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.