[Haskell-cafe] lifting restrictions on defining instances
wren ng thornton
wren at freegeek.org
Tue Jul 28 19:44:01 EDT 2009
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
More information about the Haskell-Cafe
mailing list