If you're implementing your lambda calculus AST as something like
data Exp = Var String
| Constant Int
| App Exp Exp
| Lam String Exp
then the interpreter evaluate :: Exp -> Out
can produce a number of values, some the result of poorly typed input. For instance
evaluate (Lam "f" (Lam "x" (App (Var "f") (Var "x")))
-- type like (a -> b) -> a -> b
evaluate (Var "x")
-- open term, evaluation gets stuck
evaluate (App (Lam "x" (Constant 4)) (Constant 3))
-- term results in a constant
We'll need to represent all of these types in the return type. A typical way to do that is to use a universal type like
data Out
= Stuck
| I Int
| F (Out -> Out)
which again emphasizes the need for the stuck case. If we examine the App
branch of evaluate
evaluate (App e1 e2) = case evaluate e1 of
Stuck -> Stuck
I i -> Stuck
F f -> f (evaluate e2)
show's how Stuck
cases both rise to the top and can arise from poorly typed terms.
There are many ways to write a well-typed simply-typed lambda calculus type in Haskell. I'm quite fond of the Higher-Order Abstract Syntax Final Encoding. It's wonderfully symmetric.
class STLC rep where
lam :: (rep a -> rep b) -> rep (a -> b)
app :: rep (a -> b) -> (rep a -> rep b)
int :: Int -> rep Int
newtype Interpreter a = Reify { interpret :: a } -- just the identity monad
instance STLC Interpreter where
lam f = Reify $ interpret . f . Reify
app f a = Reify $ interpret f $ interpret a
int = Reify
In this formulation, it's not possible at all to write a type of STLC rep => rep a
which isn't well-typed and never-sticking. The type of interpret
indicates this as well
interpret :: Interpreter a -> a
No Out
-type in sight.