Int > Int > Bool
Solving the halting problem
Soon after teaching Turing machines, educators often explain why the halting problem is undecidable. But then they seem to leave the story unfinished. Have we just learned we can never trust software? How can we rely on a program to control spacecraft or medical equipment if it can unpredictably loop forever?
One might claim extensive testing is the answer. We check a variety of cases work as intended, then hope for the best. But though helpful, testing alone rarely suffices. Dijkstra said: “Program testing can be used to show the presence of bugs, but never to show their absence!” In the worst case, a malicious user can examine our tests, learn what is untested, then quickly find ways to deliberately sabotage our program.
The only true fix is to rein in those unruly Turing machines. Constraining our code, might make it behave. We might try banning GOTO statements for example.
But how do we know if our restrictions are effective? Also, halting is but one concern: even if we’re sure our program halts, it should still do the right thing.
We’ll see that reasoning about our programs is easiest if we replace Turing machines with an equally powerful model of computation: lambda calculus. Only then can we introduce types, and draw on mathematics to prove correctness.
Unfortunately, some restrictions appear to have been invented without paying any heed to theory. Could this be caused by the relative obscurity of lambda calculus?
Simply typed lambda calculus
We can easily modify lambda calculus so that all programs halt while retaining some power. We’ll walk through the solution that was first discovered, the aptly named simply typed lambda calculus.
Simply typed lambda calculus is also known as \(\lambda^{\rightarrow}\).
We start with base types, say Int
and Bool
, from which we
build other types with the (→)
type constructor, such as:
Int → (Int → Bool)
. Conventionally, (→)
is right associative, so we
write this as:
This type describes a function that takes an integer, and returns a function mapping an integer to a boolean.
We can view this as a function that takes two Int
parameters and returns
a single Bool
. For example, the lessthan function might have this type.
Representing functions that take multiple arguments as a series of functions
that each take one argument is known as currying.
We populate the base types with constants, such as 0
, 1
, … for Int
,
and True
and False
for Bool
.
This seems quotidian so far. Typical highlevel languages do this sort of thing. The fun part is seeing how easily it can be tacked on to lambda calculus. There are only two changes:

We add a new kind of leaf node, which holds a constant.

The left child of a lambda abstraction (a variable) must be accompanied by a type.
We only need to add a few lines to our lambda calculus example to add simple types. Let’s get started:
{# LANGUAGE CPP #} #ifdef __HASTE__ import Haste.DOM import Haste.Events #else import System.Console.Haskeline #endif import Control.Monad import Data.Char import Data.List import Text.Parsec
First we need a new data structure to represent types. To avoid clashing
with predefined Haskell types, we use B
for Bool
and I
for Int.
data Type = I  B  Fun Type Type deriving Eq
By abuse of notation, Var
will hold variables and constants: when the string
it holds is True
, False
, or a string representation of an integer, then it
counts as a constant. Otherwise it is a variable.
We add a type to the left child of a lambda abstraction.
We also add an If
node, for ifthenelse expressions. This has nothing to
do with simply typed lambda calculus, but we introduce it because, firstly,
we want to demonstrate how to extend lambda calculus, and secondly, simply
typed lambda calculus turns out to be a bit weak, and can use all the help
it can get!
data Term = Var String  App Term Term  Lam (String, Type) Term  If Term Term Term instance Show Type where show I = "I" show B = "B" show (Fun t u) = showL t ++ " > " ++ show u where showL (Fun _ _) = "(" ++ show t ++ ")" showL _ = show t instance Show Term where show (Lam (x, t) y) = "\955" ++ x ++ ":" ++ show t ++ showB y where showB (Lam (x, t) y) = " " ++ x ++ ":" ++ show t ++ showB y showB expr = "." ++ show expr show (Var s) = s show (App x y) = showL x ++ showR y where showL (Lam _ _) = "(" ++ show x ++ ")" showL _ = show x showR (Var s) = ' ':s showR _ = "(" ++ show y ++ ")" show (If x y z) = "if " ++ show x ++ " then " ++ show y ++ " else " ++ show z
Parsing
Because we must attach type signatures to variable bindings, apart from adding
a parser for types, we also change our lambda calculus parser so that (→)
is
strictly a type constructor, and (.)
is strictly for lambda abstractions.
Haskell gets away with using (→)
for both cases because its grammar is
different. (For example, we can declare the type of a Haskell function
in one line, and define it in another.)
The strings "if", "then", and "else" are reserved keywords and hence invalid variable names.
data SimplyLambda = None  Let String Term  Run Term line :: Parsec String () SimplyLambda line = (<* eof) . (ws >>) $ option None $ (try $ Let <$> v <*> (str "=" >> term)) <> (Run <$> term) where term = ifthenelse <> lam <> app ifthenelse = If <$> (str "if" >> term) <*> (str "then" >> term) <*> (str "else" >> term) lam = flip (foldr Lam) <$> between lam0 lam1 (many1 vt) <*> term where lam0 = str "\\" <> str "\955" lam1 = str "." vt = (,) <$> v <*> (str ":" >> typ) typ = ((str "B" >> pure B) <> (str "I" >> pure I) <> between (str "(") (str ")") typ) `chainr1` (str ">" >> pure Fun) app = foldl1' App <$> many1 ((Var <$> v) <> between (str "(") (str ")") term) v = try $ do s < many1 alphaNum when (s `elem` ["if", "then", "else"]) $ fail $ "unexpected " ++ s ws pure s str = try . (>> ws) . string ws = spaces >> optional (try $ string "" >> many anyChar)
Typing
In a closed lambda term, every leaf node is typed because it’s either a
constant, or its type is given at its binding. Type checking works in
the obvious manner: for example, we can only apply a function of type
Int → Int → Bool
to an Int
, and we can only apply the resulting function
to an Int
, and the result will be a Bool
.
We predefine a few functions: negate
, add
, and not
, whose types are
hardcoded here.
Traditionally, an uppercase gamma denotes a set of variables and their types,
which is called a typing context or typing environment, hence our use of
gamma
for the first argument in our typeOf
function:
typeOf gamma t = case t of Var "negate" > Just (Fun I I) Var "add" > Just (Fun I (Fun I I)) Var "not" > Just (Fun B B) Var "False" > Just B Var "True" > Just B Var s  [(_, [])] < (reads s :: [(Integer, String)]) > Just I  otherwise > lookup s gamma App x y > do tx < rec x ty < rec y case tx of Fun ty' tz  ty == ty' > pure tz _ > Nothing Lam (x, t) y > do u < typeOf ((x, t):gamma) y pure $ Fun t u If x y z > if rec x /= Just B then Nothing else do ty < rec y tz < rec z if ty == tz then pure ty else Nothing where rec = typeOf gamma
Evaluation
Evaluation works the same as it does for untyped lambda calculus. In fact, we could perform type erasure and drop the type of every bound variable before evaluation: types are only needed during type checking. However, keeping types around can be useful for sanity checks. GHC has a typed intermediate language for this reason.
Otherwise, apart from handling predefined functions, our eval
function
is the same as our corresponding function of untyped lambda calculus.
We assume the input is welltyped and hence closed. This simplifies the
function fv
because let definitions are no longer permitted to contain free
variables.
eval env (If x y z) = eval env $ case eval env x of Var "True" > y Var "False" > z eval env (App m a) = let m' = eval env m in case m' of Lam (v, _) f > let beta (Var s)  s == v = a  otherwise = Var s beta (Lam (s, t) m)  s == v = Lam (s, t) m  s `elem` fvs = let s1 = newName s fvs in Lam (s1, t) $ beta $ rename s s1 m  otherwise = Lam (s, t) (beta m) beta (App m n) = App (beta m) (beta n) beta (If x y z) = If (beta x) (beta y) (beta z) fvs = fv [] a in eval env $ beta f Var "not" > case eval env a of Var "True" > Var "False" Var "False" > Var "True" Var "negate" > case eval env a of Var x > Var (show $ negate (read x :: Integer)) App (Var "add") b > Var $ show (m + n) where Var mstr = eval env a Var nstr = eval env b m = read mstr :: Integer n = read nstr :: Integer _ > App m' a eval env term@(Var v)  Just x < lookup v env = eval env x eval _ term = term fv vs (Var s)  s `elem` vs = []  otherwise = [s] fv vs (Lam (s, _) f) = fv (s:vs) f fv vs (App x y) = fv vs x `union` fv vs y fv vs (If x y z) = fv vs x `union` fv vs y `union` fv vs z newName x ys = head $ filter (`notElem` ys) $ (s ++) . show <$> [1..] where s = dropWhileEnd isDigit x rename x x1 term = case term of Var s  s == x > Var x1  otherwise > term Lam (s, t) b  s == x > term  otherwise > Lam (s, t) (rec b) App a b > App (rec a) (rec b) where rec = rename x x1
The function eval
leaves the term in
weak
head normal form. To fully normalize, we recurse:
norm env term = case eval env term of Var v > Var v Lam v m > Lam v (rec m) App m n > App (rec m) (rec n) If x y z > If (rec x) (rec y) (rec z) where rec = norm env
User interface
We check a term is welltyped before adding it to our list of let definitions or evaluating it. We print the type of terms to show off our new code.
For each let definition, we record the definition as well as its type.
Unlike our untyped lambda calculus interpreter, recursion is forbidden,
because we require the body of a let definition to be welltyped, and we
only prepopulate gamma
with the types of previous let definitions.
#ifdef __HASTE__ main = withElems ["input", "output", "evalB", "resetB", "resetP", "churchB", "churchP"] $ \[iEl, oEl, evalB, resetB, resetP, churchB, churchP] > do let reset = getProp resetP "value" >>= setProp iEl "value" >> setProp oEl "value" "" run (out, env) (Left err) = (out ++ "parse error: " ++ show err ++ "\n", env) run (out, env@(gamma, lets)) (Right m) = case m of None > (out, env) Run term > case typeOf gamma term of Nothing > (out ++ "type error: " ++ show term ++ "\n", env) Just t > (out ++ show (norm lets term) ++ "\n", env) Let s term > case typeOf gamma term of Nothing > (out ++ "type error: " ++ show term ++ "\n", env) Just t > (out ++ "[" ++ s ++ ":" ++ show t ++ "]\n", ((s, t):gamma, (s, term):lets)) reset resetB `onEvent` Click $ const reset churchB `onEvent` Click $ const $ getProp churchP "value" >>= setProp iEl "value" >> setProp oEl "value" "" evalB `onEvent` Click $ const $ do es < map (parse line "") . lines <$> getProp iEl "value" setProp oEl "value" $ fst $ foldl' run ("", ([], [])) es #else repl env@(gamma, lets) = do let redo = repl env ms < getInputLine "> " case ms of Nothing > outputStrLn "" Just s > case parse line "" s of Left err > do outputStrLn $ "parse error: " ++ show err redo Right None > redo Right (Run term) > do case typeOf gamma term of Nothing > outputStrLn "type error" Just t > do outputStrLn $ "[type = " ++ show t ++ "]" outputStrLn $ show $ norm lets term redo Right (Let s term) > case typeOf gamma term of Nothing > outputStrLn "type error" >> redo Just t > do outputStrLn $ "[type = " ++ show t ++ "]" repl ((s, t):gamma, (s, term):lets) main = runInputT defaultSettings $ repl ([], []) #endif
With induction, we can show type checking is efficient, and if a closed lambda term is welltyped, then it normalizes. (This implies the Y combinator and omega combinator cannot be expressed in this system.) Moreover, any evaluation strategy will lead to the normal form, that is, simply typed lambda calculus is strongly normalizing.
In other words, programs always halt. Try doing this with Turing machines!
Simply typed, or typically simple?
Simply typed lambda calculus has limited power, but this is fine for certain applications. In fact, it turns out some languages wind up embedding simply typed lambda calculus in the type system. But for generalpurpose programming, we need more.
There are two ways to fix this:

We boldly add features like unrestricted recursion. We lose our guarantee that all programs halt, but at least most of our language is trustworthy.

We cautiously enrich our type system, at each step checking that welltyped programs normalize. With a sufficiently advanced type system, we gain some forms of recursion.