Dependent if expressions without dependent types

Learning
1

This post on Haskell for all
shows an insighful use of Church encoding to implement dependent if expressions without dependent types.

The following OCaml code type checks and works:

# let example bool = if_then_else bool 5 "hi!";;

# example t;;
 - : int = 5
# example f;;
- : string = "hi!"
# example (f && t);;
- : string = "hi!"
# example (f || t);;
- : int = 5
# example (not t);;
- : string = "hi!"

This is simply based on Hindley-Milner type inference, with a single trick
that is to be not too restrictive on the type for Church encoded booleans.

Where the first idea to Church encode booleans would be to restrict the then and else cases to be the same
(using a record to encode the forall type):

type bool = { check : 'a. 'a -> 'a -> 'a; }

Dependent if expressions require a liberal definition:

type bool = { check : 'a 'b 'c. 'a -> 'b -> 'c; }

And this is what is inferred when no type is enforced
(ignoring the fact we get then weakly polymorphic types instead of forall types):

let t if_branch else_branch = if_branch
let f if_branch else_branch = else_branch

let if_then_else bool if_branch else_branch = bool if_branch else_branch

let (&&) a b if_branch else_branch = a (b if_branch else_branch) else_branch
let (||) a b if_branch else_branch = a if_branch (b if_branch else_branch)
let not a if_branch else_branch = a else_branch if_branch

I encourage you to read the full post, this is a really nice read.

1 Like