[Haskell-cafe] lifting restrictions on defining instances

[Tillmann Rendel]

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?

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.

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).

   Tillmann