[Haskell-cafe] lifting restrictions on defining instances

[wren ng thornton]

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