As other people have said, you need higher rank types for this. Lets start with just pairs to get you headed in the right direction:
{-# LANGUAGE RankNTypes #-}
(As an aside, almost all of my "real" programs require at least rank-2 types, so I usually turn on RankNTypes on principle)
mpair :: a -> b -> (a -> b -> c) -> c mpair f s k = k f s
mfst p = p (\x y -> x) msnd p = p (\x y -> y)
Here is where it gets tricky. GHC infers these types: mfst :: ((a -> b -> a) -> c) -> c msnd :: ((a -> b -> b) -> c) -> c But these aren't the right types; if you try to use both mfst and msnd on the same pair, you will unify "a" and "b" which is almost certainly wrong; it says the first and second element of the pair are the same type. Now, lets look at the type signature for the partially-applied mpair; given x :: A, and y :: B, we have mpair x y :: (A -> B -> c) -> c Notice this: a pair is a polymorphic function! Lets make functions that take pairs specify that explicitly:
mfst :: (forall c. (a -> b -> c) -> c) -> a msnd :: (forall c. (a -> b -> c) -> c) -> b
Here we tell the typechecker that mfst and msnd are required to be
passed polymorphic functions; this makes us free to determine the
result type when we call "p", and the same pair can be passed to both
of these functions successfully. The placement of the parentheses
around the "forall" is very important, because that's how we specify
where the polymorphism is required.
Similar tricks generally need to be used when defining church
numerals, if you are headed in that direction. These sort of objects
which work in untyped lambda calculus are just not expressible in the
simply typed lambda calculus, even with rank-1 polymorphism. Once you
move to full System F, a lot more becomes possible.
-- ryan
2010/1/24 Dušan Kolář
Dear cafe,
I'm trying to prepare a naive definition of booleans, numbers and some helper functions such a way, so that definition in lambda-calculus can be used in a straightforward way in Haskell. I was caught in trouble quite soon during change of lambda-expressions to Haskell - defining prefn as a helper for prev. When using Haskell-ish if-then-else then there is no problem (the code commented out), while using defined if-then-else (mif), the type-checking fails, but just for this case! Other simple tests are OK for the mif. Do I need some extra option for type-checker, or is it a principal failure (infinite type is reported) - I'm running ghci 6.10.4.
mtrue x y = x mfalse x y = y
m0 f n = n m1 f n = f n m2 f n = f (f n)
msucc x g m = x g (g m) iszero m = m (\_ -> mfalse) mtrue
mif c t f = c t f mpair f s = \e -> e f s mfst p = p mtrue msnd p = p mfalse
-- mprefn f p = if mex True False then mth else mel mprefn f p = mif mex mth mel where mex = mfst p mth = mpair mfalse (msnd p) mel = mpair mfalse (f (msnd p))
Please, change of definitions is not a solution, I'm trying to follow available resources, so using something else is not an option. :-(
Thanks for any help
Dusan
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe