Type synonym for lambda-based/church booleans

Question

Assume that true (t) and false (f) are defined as follows:

> let t = \x -> \_ -> x
t :: t1 -> t -> t1
> let f = \_ -> \y -> y
f :: t1 -> t -> t

Is there a way to define a type synonym that can capture the type of both boolean values?

The type of the Church-encoded booleans would be forall a. a -> a -> a. It cannot be specialised to either the type of your t or f but that's not surprising: their type leaks information about the boolean they represent. — gallais

Zeta Zeta · Accepted Answer · 2017-02-02T09:12:07

Given that Church Booleans basically either choose the first or the second parameter, and you want to use them in something like

if' :: Boolean -> a -> a -> a
if' b tval fval = b tval fval

such that

if' t 1 0 == 1
if' f 1 0 == 0

you have to restrict the type to a single type variable a:

{-# LANGUAGE RankNTypes #-}

type Boolean = forall a. a -> a -> a