Dependent if expressions without dependent types

The post discusses a technique for implementing code that seems to require dependent types, but actually does not need dependent types. This technique works in any language that supports simple Hindley-Milner type inference. The author learned this trick from studying Haskell packages, particularly the formatting package. The technique is adapted to model dependent if expressions that can return different types based on their input.

Church encoding is introduced as a method for encoding data structures and operations on those structures using pure functions. In the context of boolean values, Church encoding represents true and false as functions that accept two arguments and return one of the two arguments based on the condition. The author defines an `ifThenElse` function that behaves like a traditional if expression but expects the condition to be a Church-encoded boolean value.

The author demonstrates how the code using Church-encoded booleans works by reasoning through the evaluation of `ifThenElse` on true and false. The author then shows how to replace traditional if/then/else syntax with the `ifThenElse` function by enabling the `RebindableSyntax` language extension. This allows expressions of the form `if condition then thenBranch else elseBranch` to be desugared to `ifThenElse condition thenBranch elseBranch`.

The post goes on to show how to implement other boolean operations on Church-encoded booleans and how to remove type declarations and the `RankNTypes` extension to make dependent if expressions work with only one language extension, `RebindableSyntax`. The author explains that by removing type signatures, the compiler infers more general types for the code, allowing it to support dependent if expressions. The author demonstrates this by showing how the type checker infers different types based on the input boolean value.