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