Dependent if expressions without dependent types

This post showcases a folklore trick for implementing code that seems like it should require dependent types without actually requiring dependent types. In fact, this trick works in any language with simple Hindley-Milner type inference. To prove that, by the end of this post I'm going to show how you can make this Haskell code type-check and work:

example bool = if bool then 5 else "hi!"

main = do
    print (example false)            -- "hi!"
    print (example true )            -- 5
    print (example (false && true))  -- "hi!"
    print (example (false || true))  -- 5
    print (example (not true))       -- "hi!"

… and it will only require one language extension: RebindableSyntax.

I picked up this trick from studying various Haskell packages, most notably the formatting package. Here I'm adapting the trick to modeling dependent if expressions which can return different types based on their input.

I'll build up to the trick in two steps: first I'll explain a related trick (Church-encoded booleans) and then generalize that trick to implement our dependent if expressions.

Church encoding

"Church encoding" is a technique for encoding data structures and operations on those data structures using pure functions and nothing else.

For example, we can Church-encode boolean values as functions that accept two arguments and return one of the two arguments as their result:

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (Bool(..), not, (&&), (||))

type Bool = forall a . a -> a -> a

true :: Bool
true thenBranch elseBranch = thenBranch

false :: Bool
false thenBranch elseBranch = elseBranch

The reason I name the function arguments thenBranch and elseBranch is because you can think of these Church-encoded boolean values as "pre-formed if expressions", meaning that the two function arguments (thenBranch and elseBranch) represent the then and else branches of an if expression and the boolean value selects which branch to return as the result. In fact, we can define an ifThenElse function that behaves just like an if expression except that it expects the condition to be a Church-encoded boolean value:

…

ifThenElse :: Bool -> a -> a -> a
ifThenElse condition thenBranch elseBranch =
    condition thenBranch elseBranch

… and it works just like an if expression would:

>>> ifThenElse true "then branch" "else branch"
"then branch"
>>> ifThenElse false "then branch" "else branch"
"else branch"

NOTE: If you want to follow along and/or run any of these examples you can find the complete code in the Appendix.

To see why the above code works, let's reason through what happens if we invoke our ifThenElse function on true:

ifThenElse true thenBranch elseBranch

-- According to the definition of `ifThenElse`:
= true thenBranch elseBranch

-- According to the definition of `true`:
= thenBranch

The above expression returns the thenBranch, just like a traditional if expression would when given true. Similarly, if we invoke ifThenElse on false then we get the elseBranch:

ifThenElse false thenBranch elseBranch
= false thenBranch elseBranch
= elseBranch

In fact, we can go a step further and change Haskell's if/then/else syntax to use the above ifThenElse function. If we enable the RebindableSyntax language extension then all expressions of the form if condition then thenBranch else elseBranch are desugared to ifThenElse condition thenBranch elseBranch using whatever ifThenElse function happens to be in scope:

{-# LANGUAGE RebindableSyntax #-}

…

toString :: Bool -> String
toString bool = if bool then "true" else "false"

main :: IO ()
main = do
    print (toString false)  -- "false"
    print (toString true )  -- "true"

We can reason through why this works the same way as before:

toString false

-- According to the definition of `toString`:
= if false then "true" else "false"

-- `if`/`then`/`else` desugars to `ifThenElse`
= ifThenElse false "true" "false"

-- According to the definition of `ifThenElse`:
= false "true" "false"

-- According to the definition of `false`:
= "false"

We can keep going, though, and implement all the usual boolean operations to work on these Church-encoded boolean values:

not :: Bool -> Bool
not bool thenBranch elseBranch =
    bool elseBranch thenBranch

(&&) :: Bool -> Bool -> Bool
(x && y) thenBranch elseBranch =
    x (y thenBranch elseBranch) elseBranch

(||) :: Bool -> Bool -> Bool
(x || y) thenBranch elseBranch =
    x thenBranch (y thenBranch elseBranch)

… and they work exactly the way we expect:

main :: IO ()
main = do
    …
    print (toString (not true))       -- "false"
    print (toString (false && true))  -- "false"
    print (toString (false || true))  -- "true"

… and we can reason through that last example like this:

toString (false || true)
= if false || true then "true" else "false"
= ifThenElse (false || true) "true" "false"
= (false || true) "true" "false"
= false "true" (true "true" "false")
= true "true" "false"
= "true"

However, the original motivating example function still does not type-check with these Church-encoded booleans. If we try to type-check it we get:

ghci> example bool = if bool then 5 else "hi!"
<interactive>:2:29: error: [GHC-39999]
    • No instance for ‘Num String’ arising from the literal ‘5’
    • In the expression: 5
      In the expression: if bool then 5 else "hi!"
      In an equation for ‘example’:
          example bool = if bool then 5 else "hi!"

So how are we going to make this work?

The trick

So far we had to enable two language extensions to make these Church-encoded booleans work:

• RankNTypes
• RebindableSyntax

… but earlier I said that we were going to make dependent if expressions work with only one extension: RebindableSyntax. So does this mean that we're going to somehow make our Church-encoded booleans more powerful with fewer language extensions?

Yes! In fact, all we have to do is delete all of the type declarations, type signatures, and the RankNTypes extension, like this:

{-# LANGUAGE RebindableSyntax #-}

import Prelude hiding (Bool(..), not, (&&), (||))

true thenBranch elseBranch = thenBranch

false thenBranch elseBranch = elseBranch

ifThenElse condition thenBranch elseBranch =
    condition thenBranch elseBranch

not bool thenBranch elseBranch =
    bool elseBranch thenBranch

(x && y) thenBranch elseBranch =
    x (y thenBranch elseBranch) elseBranch

(x || y) thenBranch elseBranch =
    x thenBranch (y thenBranch elseBranch)

toString bool = if bool then "true" else "false"

main = do
    print (toString false)            -- "false"
    print (toString true )            -- "true"
    print (toString (false && true))  -- "false"
    print (toString (false || true))  -- "true"
    print (toString (not true))       -- "false"

… and not only does our code still type check but now it supports dependent if expressions! The code I showed earlier at the beginning of the post Just Works™️:

example bool = if bool then 5 else "hi!"

main = do
    print (example false)            -- "hi!"
    print (example true )            -- 5
    print (example (false && true))  -- "hi!"
    print (example (false || true))  -- 5
    print (example (not true))       -- "hi!"

Wild, right? How does that even work?

The explanation

The above example function would not type check with the old type signatures in place because those type signatures were actually too restrictive. When we remove those type signatures the compiler infers more general types for the same code.

To illustrate this I'll add back the types the compiler infers, starting with the types for true and false:

true :: a -> b -> a
true thenBranch elseBranch = thenBranch

false :: a -> b -> b
false thenBranch elseBranch = elseBranch

The most general type for true is a function that takes two arguments that can be different types (a and b) and the type of the result is the type of the first argument. Similarly, false also accepts arguments of different types, except that the type of the result is the type of the second argument.

However, for this post I want to avoid using type variable names like a and b so I will instead propose renaming a to thenBranch and b to elseBranch like this:

true :: thenBranch -> elseBranch -> thenBranch
true thenBranch elseBranch = thenBranch

false :: thenBranch -> elseBranch -> elseBranch
false thenBranch elseBranch = elseBranch

I'll also introduce and use a new Bool type which is just a glorified synonym for a function of two arguments:

type Bool thenBranch elseBranch result =
    thenBranch -> elseBranch -> result

true :: Bool thenBranch elseBranch thenBranch
true thenBranch elseBranch = thenBranch

false :: Bool thenBranch elseBranch elseBranch
false thenBranch elseBranch = elseBranch

This new Bool type synonym shares one thing in common with our old Bool type synonym, which is that they're both functions of two arguments:

type Bool = forall a . a -> a -> a

However, now the two function arguments and the result can all have different types; they no longer need to be the same type.

Now we can annotate the type of ifThenElse:

ifThenElse
    :: Bool thenBranch elseBranch result
    -> thenBranch
    -> elseBranch
    -> result
ifThenElse condition thenBranch elseBranch =
    condition thenBranch elseBranch

This new type signature preserves more information and indicates that the type of the result changes depending on which Bool we pass into the function.

To see how this works, suppose we were to pass in true as the first argument to ifThenElse. The type checker would line up the type of the first argument with the type of true, like this:

ifThenElse :: Bool thenBranch elseBranch result     -> … -> … -> …
                                         ↕↕↕↕↕↕
true       :: Bool thenBranch elseBranch thenBranch

… and then the type-checker would infer that the result type variable must match the thenBranch type variable. The type-checker then goes through the type of ifThenElse and fixes the mismatch by replacing every occurrence of thenBranch with result:

ifThenElse
    :: Bool result elseBranch result
    -> result
    -> elseBranch
    -> result

… which means that if we apply ifThenElse to true we should get this type:

ifThenElse true :: result -> elseBranch -> result

… and now we can see from the type that it will return the first argument and ignore the second argument.

We can also confirm that we got the type right by asking the REPL to infer the type:

ghci> :type ifThenElse true
ifThenElse true :: result -> elseBranch -> result

Vice versa, if we pass in false then the type checker unifies the result type variable with the elseBranch type variable, giving us this type:

ghci> :type ifThenElse false
ifThenElse false :: thenBranch -> result -> result

… so depending on which Bool we pass in as the first argument we get a different type!

The reason this all works is because our new Bool type tracks information flow at the type-level. For example, if we spell out the generalized type of our not function:

not :: Bool thenBranch elseBranch result
    -> Bool elseBranch thenBranch result
not bool thenBranch elseBranch =
    bool elseBranch thenBranch

… the type signature now indicates that the not swaps the "then" and "else" branches. Before we would know that from looking at the implementation of the not function but now that same information is being tracked at the type level.

However, the types of our generalized logical operators might be a bit harder to follow along:

(&&)
    :: Bool intermediateResult elseBranch result
    -> Bool thenBranch         elseBranch intermediateResult
    -> Bool thenBranch         elseBranch result
(x && y) thenBranch elseBranch =
    x (y thenBranch elseBranch) elseBranch

(||)
    :: Bool thenBranch intermediateResult result
    -> Bool thenBranch elseBranch         intermediateResult
    -> Bool thenBranch elseBranch         result
(x || y) thenBranch elseBranch =
    x thenBranch (y thenBranch elseBranch)

… but (in my opinion) they make more sense if you slightly refactor the implementation to more closely match the inferred types:

(&&)
    :: Bool intermediateResult elseBranch result
    -> Bool thenBranch         elseBranch intermediateResult
    -> Bool thenBranch         elseBranch result
(x && y) thenBranch elseBranch = x intermediateResult elseBranch
  where
    intermediateResult = y thenBranch elseBranch

(||)
    :: Bool thenBranch intermediateResult result
    -> Bool thenBranch elseBranch         intermediateResult
    -> Bool thenBranch elseBranch         result
(x || y) thenBranch elseBranch = x thenBranch intermediateResult
  where
    intermediateResult = y thenBranch elseBranch

With that slight refactor the information flow at the type level exactly corresponds to the information flow at the implementation level:

• the thenBranch type tracks the flow of the thenBranch variable
• the elseBranch type tracks the flow of the elseBranch variable
• the intermediateResult type tracks the flow of the intermediateResult variable

Finally, let's check out the generalized types of our boolean functions:

toString :: Bool String String result -> result
toString bool = if bool then "true" else "false"

example :: Bool Int String result -> result
example bool = if bool then 5 else "hi!"

These functions now document in the types which type they'll return based on which Bool we provide. In a dependently typed language the types would have been something like:

example :: (bool :: Bool) -> if bool then Int else String

… but we can express something similar without dependent types by instead adding more type arguments to our Bool type. This is all possible with ≈20 lines of ordinary functional code making use of vanilla type system features.

Mixing bools

Another cool feature of this approach is that if you mix true and false together the inferred type degrades gracefully to an "unrefined" bool.

For example, if you stick true and false together in a list, then the inferred type is:

bools :: [Bool result result result]
bools = [true, false]

… which means that any function (or if expression) processing the list has to return the same type for the thenBranch and elseBranch.

That means that the compiler won't complain if we call toString on this list because toString returns the same result type for both branches:

ghci> map toString [true, false]
["true","false"]

… but if we call our dependent example function on the same list we'll get a type error because we can't mix two branches which have different types:

ghci> map example [true, false]
<interactive>:3:21: error: [GHC-83865]
    • Couldn't match type ‘[Char]’ with ‘Int’
      Expected: Bool Int String Int
        Actual: Bool Int String String
    • In the expression: false
      In the second argument of ‘map’, namely ‘[true, false]’
      In the expression: map example [true, false]

Assertions

If you're willing to enable a couple more extensions you can even implement primitive assertions on boolean expressions to enforce that they must be true, like this:

{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE TypeFamilies     #-}

import Data.Kind (Constraint)
import GHC.TypeLits (TypeError, ErrorMessage(..))

data AssertionFailed = AssertionFailed

type family Successful result :: Constraint where
    Successful AssertionFailed =
        Unsatisfiable ('Text "Assertion failed")
    Successful _ =
        ()

assert
    :: Successful result
    => Bool result AssertionFailed result -> result -> result
assert condition expression =
    if condition then expression else AssertionFailed

If the condition is true then assert just returns the second argument:

ghci> assert true 1
1
ghci> assert (true || false) 1
1
ghci> [ assert b 1 | b <- [true, true] ]
[1,1]

… but if it's false then you'll get a type error.

ghci> assert false 1
<interactive>:1:1: error: [GHC-22250]
    • Assertion failed
    • In the expression: assert false 1
      In an equation for ‘it’: it = assert false 1

ghci> assert (true && false) 1
<interactive>:2:1: error: [GHC-22250]
    • Assertion failed
    • In the expression: assert (true && false) 1
      In an equation for ‘it’: it = assert (true && false) 1

ghci> [ assert b 1 | b <- [true, false] ]
<interactive>:3:3: error: [GHC-22250]
    • Assertion failed
    • In the expression: assert b 1
      In the expression: [assert b 1 | b <- [true, false]]
      In an equation for ‘it’: it = [assert b 1 | b <- [true, false]]

Conclusion

If you liked this post you might also like these two other posts of mine, both of which are related to Church encoding:

• Folds are constructor substitution

  That post doesn't actually use the term "Church encoding" but it is describing the same thing as Church encoding. Every type's Church encoding is its "pre-formed" fold (just like how the Bool type's Church-encoding is a "pre-formed" if expression).

• The visitor pattern is essentially the same thing as Church encoding

  This post explains Church encoding through the lens of the visitor pattern, which can sometimes be helpful for people coming from an object-oriented programming background.

Appendix - Church-encoded booleans

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE RankNTypes       #-}

import Prelude hiding (Bool(..), not, (&&), (||))

type Bool = forall a . a -> a -> a

true :: Bool
true thenBranch elseBranch = thenBranch

false :: Bool
false thenBranch elseBranch = elseBranch

ifThenElse :: Bool -> a -> a -> a
ifThenElse condition thenBranch elseBranch =
    condition thenBranch elseBranch

not :: Bool -> Bool
not bool thenBranch elseBranch =
    bool elseBranch thenBranch

(&&) :: Bool -> Bool -> Bool
(x && y) thenBranch elseBranch =
    x (y thenBranch elseBranch) elseBranch

(||) :: Bool -> Bool -> Bool
(x || y) thenBranch elseBranch =
    x thenBranch (y thenBranch elseBranch)

toString :: Bool -> String
toString bool = if bool then "true" else "false"

main :: IO ()
main = do
    print (toString false)            -- "false"
    print (toString true )            -- "true"
    print (toString (false && true))  -- "false"
    print (toString (false || true))  -- "true"
    print (toString (not true))       -- "false"

Appendix - Generalized Church-encoded booleans

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE TypeFamilies     #-}

import Data.Kind (Constraint)
import GHC.TypeLits (TypeError, ErrorMessage(..))
import Prelude hiding (Bool(..), not, (&&), (||))

type Bool thenBranch elseBranch result =
    thenBranch -> elseBranch -> result

true :: Bool thenBranch elseBranch thenBranch
true thenBranch elseBranch = thenBranch

false :: Bool thenBranch elseBranch elseBranch
false thenBranch elseBranch = elseBranch

ifThenElse
    :: Bool thenBranch elseBranch result
    -> thenBranch
    -> elseBranch
    -> result
ifThenElse condition thenBranch elseBranch =
    condition thenBranch elseBranch

not :: Bool thenBranch elseBranch result
    -> Bool elseBranch thenBranch result
not bool thenBranch elseBranch =
    bool elseBranch thenBranch

(&&)
    :: Bool intermediateResult elseBranch result
    -> Bool thenBranch         elseBranch intermediateResult
    -> Bool thenBranch         elseBranch result
(x && y) thenBranch elseBranch =
    x (y thenBranch elseBranch) elseBranch

(||)
    :: Bool thenBranch intermediateResult result
    -> Bool thenBranch elseBranch         intermediateResult
    -> Bool thenBranch elseBranch         result
(x || y) thenBranch elseBranch =
    x thenBranch (y thenBranch elseBranch)

data AssertionFailed = AssertionFailed

type family Successful result :: Constraint where
    Successful AssertionFailed =
        Unsatisfiable ('Text "Assertion failed")
    Successful _ =
        ()

assert
    :: Successful result
    => Bool result AssertionFailed result -> result -> result
assert condition expression =
    if condition then expression else AssertionFailed

toString :: Bool String String result -> result
toString bool = if bool then "true" else "false"

example :: Bool Int String result -> result
example bool = if bool then 5 else "hi!"

main = do
    print (example false)            -- "hi!"
    print (example true )            -- 5
    print (example (false && true))  -- "hi!"
    print (example (false || true))  -- 5
    print (example (not true))       -- "hi!"