[Haskell-cafe] Re: explicit big lambdas

[oleg at okmij.org]

Paul Brauner wrote:
> is there a way in some haskell extension to explicit (system F's) big
> lambdas and (term Type) applications in order to help type inference?

Actually, yes: newtype constructor introductions may act as a big
lambda, with constructor elimination acting as type applications:
	http://okmij.org/ftp/Haskell/types.html#some-impredicativity


Newtypes are also handy for turning type functions (defined by type
families) into real lambdas. For example, given the following code

> {-# LANGUAGE NoMonomorphismRestriction #-}
> {-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
> {-# LANGUAGE ScopedTypeVariables #-}
>
> module S where
>
> data Z
> data S a 
>
> class Nat a where nat :: a -> Int
> instance Nat Z where nat _ = 0
> instance Nat n => Nat (S n) where nat _ = succ (nat (undefined::n))
>
> type family Add a b
> type instance Add Z b = b
> type instance Add (S a) b = S (Add a b)


we would like to compose the type function Add (S (S Z)) twice.

We may first try

*> newtype F2 f x = F2{unF2 :: f (f x)}
*> tf1 :: F2 (Add (S (S Z))) (S Z)
*> tf1 = undefined

alas, without success:
    Type synonym `Add' should have 2 arguments, but has been given 1
    In the type signature for `tf1':
      tf1 :: F2 (Add (S (S Z))) (S Z)

Indeed, type functions defined via type families can't be turned into
closures. Newtypes help, introducing the needed Lambda behind the
scenes:

> newtype A2 a = A2{unA2 :: Add (S (S Z)) a}
>
> appA2 :: x -> A2 x
> appA2 = undefined
>
> -- Now we can compose the type function, many times
> tc = unA2 . appA2 . unA2 . appA2
> -- Inferred type:
> -- tc :: a -> Add (S (S Z)) (Add (S (S Z)) a)
>
> tcrun = nat $ tc (undefined::S Z)
> -- 5

One can see from the inferred type of tc that the type-checker has
composed the partially applied Add function. I'll show a bit more
elaborate example next week.