# Dependent if expressions without dependent types

**URL:** <https://discuss.ocaml.org/t/dependent-if-expressions-without-dependent-types/18506>\
**Category:** Learning\
**Created:** [September 3, 2026, 9:58am UTC](https://discuss.ocaml.org/t/dependent-if-expressions-without-dependent-types/18506 "2026-09-03T09:58:40Z")\
**Posts on this page:** 1\
**Showing post:** 1

<div class="post-metadata">

**Author:** ![didier-wenzek](https://avatars.discourse-cdn.com/v4/letter/d/9de0a6/32.png) [@didier-wenzek](https://discuss.ocaml.org/u/didier-wenzek)\
**Post date:** [September 3, 2026, 9:58am UTC](https://discuss.ocaml.org/t/dependent-if-expressions-without-dependent-types/18506/1 "2026-09-03T09:58:40Z")

</div>

This [post on Haskell for all](https://haskellforall.com/2026/09/dependent-if-expressions)  
shows an insighful use of Church encoding to implement dependent if expressions without dependent types.

The following OCaml code type checks and works:

```auto
# 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):

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

```

Dependent if expressions require a liberal definition:

```auto
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):

```auto
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.

---

_[View the full topic](https://discuss.ocaml.org/t/dependent-if-expressions-without-dependent-types/18506)._