[Haskell-cafe] Re: explicit big lambdas
oleg at okmij.org
oleg at okmij.org
Fri Mar 19 06:00:13 EDT 2010
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.
More information about the Haskell-Cafe
mailing list