Haskell, lambda calculus for Evaluation

Question

(Figure 1)

A part of the simply typed lambda calculus (Figure 1), it is implemented in Haskell as given below.

 evaluate expression = do
        case expression of
        (Application (Lambda x ltype term) value) | isValue value = True -> substitute term x value
        (Application value e2) | isValue value = True  -> let e22 = evaluate e2 in Application value e22
        (Application  e1 e2) -> let e11 = evaluate e1 in Application e11 e2

However, this doesn't work for these test cases,

1) print (evaluate (Application (Var "x") (Var "y")))

2) print (evaluate (Application (Constant 3) (Var "y")) "(Constant 3) is a value"

But, for the first test case, I know it's because (Var "x") as e1 is terminal so it cannot transition. Does it mean I should add a Stuck case? But I want to return an output suggesting the success of the transitions, if that's possible.

Thank you in advance...

Answer 1

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.

Answer 2

But, how substitute works then (i.e. what is the implementation of the substitute function in haskell).