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?

No, because Haskell does not know that cond should be either true or false. For Haskell cond is a generic function. — Willem Van Onsem
You could write ifThenElse :: (t -> t -> t) -> t -> t -> t. — melpomene
I know that Haskell doesn't know that cond must be either true or false. I'm asking how to require that it be that.. — RussAbbott
Switch on RankNTypes and demand ifThenElse take a condition of type forall t. t -> t -> t. — pigworker

HTNW HTNW · Accepted Answer · 2017-09-09T18:08:26

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.

Implementing Lambda Calculus true and false in Haskell

1 Answers