Dependent if expressions without dependent types

# Dependent if expressions without dependent types Source: [https://haskellforall.com/2026/09/dependent-if-expressions](https://haskellforall.com/2026/09/dependent-if-expressions) 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](https://hackage.haskell.org/package/formatting)\. 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](https://haskellforall.com/2021/02/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](https://haskellforall.com/2021/01/the-visitor-pattern-is-essentially-same) 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!" ```