[Haskell-cafe] Partial type family application

[mniip]

So I've been thinking of a type system extension: partial type family
application.

If we look at the type system used by modern GHC, in it, type family
application is very distinct from constructor/constraint application: it
is somewhat opaque in the sense that a type family must always appear
fully applied. As such, it doesn't make sense to talk about a type
family's kind, if we have:

	type family Id (a :: *) :: * where
		Id x = x

then saying that 'Id :: * -> *' would be wrong, because Id cannot be
used interchangeably with things that are truly of kind * -> *, such as
Maybe or [].

The reason for the "fully applied" restriction is that if we allowed
partially applied type functions, then their equality would be
undecidable.

Still, I think, in a lot of cases we could benefit from partially
applied type functions, even without extensional equality. Writing type
level list folds, filters, zips, you name it.

As stated above, we can't add the proposition 'Id :: * -> *' to our type
system, so, what if, instead, we added a different kind of arrow kind
for type families? I like the look of (~>), so 'Id :: * ~> *'.

	(~>) :: * -> * -> *

This rule of inference, similar to the usual, would supersede all the type
family kinding rules:

	f :: k ~> l, x :: k
	-------------------
	     f x :: l

As such, the juxtaposition operator would very clearly have two
different "kinds": (k -> l) --> k --> l and (k ~> l) --> k --> l, and
there is no N-ary "type family application" operator.

In order for the type checker to not fall apart, we need to have at
least intesional (structural) equality on (~>), which we can have
because it is decidable.

We could then write stuff like

	type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where
	    Foldr f z '[] = z
	    Foldr f z (x ': xs) = f x (Foldr f z xs)