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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
