Haskell, lambda calculus for Evaluation

evaluate, haskell, lambda, lambda-calculus, types

Solution

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.

Problem

(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...

Original source