Implementing Lambda Calculus true and false in Haskell

Question

Perhaps this is a trivial question and I'm just not thinking about it correctly. If so, my apologies.

I would like to implement the lambda calculus true and false functions in Haskell and then use those to implement if-then-else. Here's what I did.

true :: t1 -> t2 -> t1
true x y =  x

false :: t1 -> t2 -> t2
false x y = y

-- ifThenElse :: (t2 -> t1 -> t) -> t2 -> t1 -> t
ifThenElse cond thenPart elsePart =  cond thenPart elsePart

The commented-out ifThenElse type is what GHC generates. My concern is that t in that type should be constrained to be either t1 or t2. Can I write a type for ifThenElse that accomplishes this?

Answer 1

You want these:

{-# LANGUAGE RankNTypes #-}
-- These are the only two values of this type...
true  :: l -> r -> Either l r
false :: l -> r -> Either l r
true  l _ = Left  l
false _ r = Right r

-- ...and they are the only possible arguments here.
ifThenElse :: (forall l r. l -> r -> Either l r) -> l -> r -> Either l r
ifThenElse = id

There's no way around Either if you want differing left and right types.