[Haskell-cafe] lifting restrictions on defining instances

[Tillmann Rendel]

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.


In other words, the following is not legal Haskell, and not how forall 
works in any polymorphic lambda calculus:

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

Note that (forall a . a) has kind *, so (forall a . a) Int is not even 
well-kinded, as ghci correctly determines:

   > ghci -XRankNTypes
   > :k (forall a. a)
   (forall a. a) :: *

   > :k (forall a . a) Int
   <interactive>:1:0:
       Kind error: `forall a. a' is applied to too many type arguments

About syntax:
>>   (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)
> 
> 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 ->).

I agree that this makes as much sense as my view.

However, I still argue that the existing type/kind symmetry for -> 
should be reflected in a term/type symmetry for \. We already have:

   id x = x
   type Id x = x

   :t id
   id :: a -> a

   :k Id
   Id :: * -> *

And I think anonymous type-level abstraction should look like this:

   id' = \x -> x
   type Id' = \x -> x

   :t id'
   id' :: a -> a

   :k Id'
   Id' :: * -> *

I would use the upper-case lambda for kind-polymorphism on the type level.

   type Id'' = /\k -> \t :: k -> t
   :k Id'' :: forall k . k -> k

   :k Id'' [*] :: * -> *
   :k Id'' [*] Int = Int
   :k Id'' [forall k . k -> k] Id'' [*] Int = Int

Tillmann