Doesn't the simply typed lambda calculus introduce if-then-else as a primitive precisely so that it can be typed? Its not an illuminating answer to your question and I'd welcome clarification for my own understanding, but I don't think you can solve the problem without appealing to Haskell's built-in if-then-else. Best wishes Stephen

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