[Haskell-cafe] lifting restrictions on defining instances

[wren ng thornton]

Tillmann Rendel wrote:
> wren ng thornton wrote:
>> [1] In System F the capital-lambda binder is used for the term-level 
>> abstraction of passing type representations. So for example we have,
>>
>>     id :: forall a. a -> a
>>     id = /\a. \(x::a). x
>>
>> Thus, the forall keyword is serving as the type-level abstraction. 
>> Perhaps this is suboptimal syntax, but it is the standard. We could, 
>> of course, have both a term-level /\ and a type-level /\ where the 
>> latter is the type of the former (since the namespaces are separate) 
>> though that's also dubious. Capital-pi is the canonical type-level 
>> abstraction, though that evokes the idea of dependent types which are 
>> much more complex.
> 
> 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.


> In a language with type functions and polymorphism, we need three 
> different lambda binders:
> 
>   (1) abstraction over terms in terms (to construct functions)
>   (2) abstraction over types in terms (to construct polymorphic values)
>   (3) abstraction over types in types (to construct type functions)
> 
> I think only (2) should be written as upper-case lambdas, while (1) and 
> (3) should both be written as lower-case lambdas. Since (1) and (3) 
> belong to different syntactic categories, they can not be confused, and 
> we can reuse the lower-case lambda at the type-level.

I'm sure that's fine. I was merely pointing out precedent.

The syntax of #3 could also be conflated with the syntax of #2, for the 
same reason: they are in different syntactic categories. I pointed this 
out because the capital-lambda was the syntax others in the thread were 
using. Also, it makes sense to me to have #2 and #3 ("abstraction over 
types in _") paired together, rather than #1 and #3 ("abstraction over X 
in X"). Pairing #2/#3 also gives term/type symmetry as we have for other 
built-ins like [], (,), and -> (though the symmetry is imperfect for ->).


> Furthermore, we need three function types / kinds to describe the three 
> lambdas one level higher:
> 
>   (4) the type of functions
>   (5) the type of polymorphic values
>   (6) the kind of type functions
> 
> In ghc, we already have "forall" for (5), and arrows for (4) and (6).
> 
> I would say that (3) is the "type-level abstraction", not (5).

I'm not sure I follow what you mean. Given the relationship between /\ 
and forall as demonstrated in the definition of id above, I don't see 
such a difference between #3 and #5. That is, given the need for #2 the 
need for #5 follows; from there #3 follows by extending the wording of 
#5. (Though #6 is desirable from a theoretical perspective I'm not sure 
whether the language needs to be able to express it. There's much else 
at the kind-layer we cannot express.)

In other words, just because forall is the type of /\ doesn't mean that 
that's all it is. All of these are effectively identical:

     -- Just a type-level lambda
     five :: (forall a. a) Int
     five = 5

     -- Making the term-level match the type exactly
     five :: (forall a. a) Int
     five = (/\a. 5::a) @Int

     -- Hiding a CAF behind a constant type
     -- (somewhat like how numeric constants really work)
     five :: Int
     five = (/\a. 5::a) @Int

     -- Boring
     five :: Int
     five = 5

-- 
Live well,
~wren