Tillmann Rendel wrote:
wren ng thornton wrote:
Thus, the forall keyword is serving as the type-level abstraction.
What do you mean by "type-level abstraction" here?
I mean an abstraction, as in a lambda-abstraction (aka a lambda-expression), at the type level.
[...]
I'm not sure I follow what you mean.
I mean that the forall keyword is *not* serving as the type-level abstraction.
There is a difference between abstraction (as in lambda abstraction) and the type of abstractions (as in function types). In pure type systems, we have two different binders for these different features:
- lower-case lambda for abstraction (on all levels) - upper-case Pi for the type of abstractions (on all levels)
I find it highly confusing to say that forall denotes type-level abstraction, because it does not denote abstraction at all. It rather denotes the type of an abstraction, namely in Haskell, the type of abstracting over types in terms.
I view these as different sides of the same coin. There are two different senses of the "forall" keyword. There's the implicit Rank-1 quantifier, and then there's the Rank-N quantifier for polymorphic components. Your intuition is relying on the latter, whereas mine is relying on the former. The difference is similar to the difference between morphisms vs exponential objects in CCCs. We often find it convenient to elide the conversions between them, but they are in fact quite different. And if, at the term layer, functions can be silently lifted to/lowered from closures, then why not also at the type layer? While it is important to keep the ideas distinct, in practice we've found great utility in conflating the two faces of the coin. Why can't the type of abstractions be an abstraction of types? This is not currently the case in GHC, as you point out, but that does not demonstrate that the idea is unsound. This distributive transformation is used routinely in Conal Elliott's typeclass morphisms[1], Ralf Hinze's polyidiomatic lambda calculus[2], in HOAS (if you squint), and many other places where poly*ism spans multiple layers of the tower of interpretation. The symmetry between forall and /\ in System F is simply too great to write off without investigation. In any case, I think this discussion has veered far afield from the intent of my original footnote, which was simply to point out that the capital-lambda binder already has a canonical usage in System F (so we should not co-op it for type abstractions, without express intention). I have little invested in the current discussion, and the Cafe list doesn't really seem like the best venue to pursue it. If you have references you think would enlighten me, I'd happily pursue them. Otherwise, I think the best color for the bikeshed is purple :) [1] http://conal.net/blog/tag/type-class-morphism/ [2] http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8//26/slides/ralf.pdf -- Live well, ~wren