[Haskell-cafe] Naive booleans and numbers - type-checking fails

[Ryan Ingram]

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ář <kolar at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>