Church encoding of boolean and STLC

Question

It is often said that

tru t f = t
fls t f = f

represent True and False in the sense that "we can use those terms to perform the operation on testing the truth of a boolean value".

But that hides an important caveat in that it seems only true in the untyped lambda calculus. If I just plug those values in haskell, I can write a function :

tryMeOnFalse ∷  (∀ t f. t → f → t) → String
tryMeOnFalse tr = "Hi"
a' = tryMeOnFalse tru
b' = tryMeOnFalse fls  -- type error !

which distinguishes tru and fls at the type level. How wrong/true would it be to say that :

in STLC tru and fls are value level witness of some promoted 'Boolean kind, which has types 'True and 'False
in STLC the (coerced) typed values (tru :: ∀ t . t → t → t) and (fls :: ∀ t . t → t → t) represent True and False (and in untyped, well the usual)

Edit : I now realize thanks to @Daniel Wagner's answer I was thinking of Second Order Lambda Calculus and not STLC in my question.

Daniel Wagner Daniel Wagner · Accepted Answer · 2016-06-05T18:06:20

It is not only true in the untyped lambda calculus; but in typed calculi, one does need to be a bit careful with typing, as usual. We should define:

type Boolean = forall r. r -> r -> r

We certainly have tru, fls :: Boolean, and should annotate them as such. But we do not have tryMeOnFalse :: Boolean -> String! So there is no real contradiction here.

Your comments about STLC are a bit weird, since STLC has a very different typing system. We would need separate boolean types for each result type there, since there is no polymorphism.

In Haskell, one can certainly define types which are inhabited only by tru or only by fls (well, each type is also inhabited by undefined, of course); but this is generally not very useful.

Church encoding of boolean and STLC

1 Answers