Interpret.hs

data Expr = EApp Expr Expr
          | EAbs String Expr
          | EVar String
          | EInt Int
          deriving (Show)


-- (λx.x x) (λx.x x)
unterminating = EApp (EAbs "x" (EApp (EVar "x") (EVar "x"))) (EAbs "x" (EApp (EVar "x") (EVar "x")))

-- (λy.1) ((λx.x x) (λx.x x))
expr = EApp (EAbs "y" (EInt 1)) unterminating

{-
  The problem is: what leads to the laziness that promises the termination of above expression?
-}

interpret :: Expr -> Expr
interpret (EInt i)               = EInt i
interpret (EVar x)               = error $ "unbound " ++ x
interpret (EApp (EAbs x body) e) = subst x e body
interpret (EApp e1 e2)           = EApp (interpret e1) (interpret e2)
interpret (EAbs x body)          = EAbs x body

interpret' :: Expr -> Expr
interpret' expr =
    let expr' = interpret expr
    in  if isNormalForm expr' then expr'
        else interpret' expr'

subst :: String -> Expr -> Expr -> Expr
subst x e (EInt i) = EInt i
subst x e (EVar x')
    | x == x'   = e
    | otherwise = EVar x'
subst x e (EApp e1 e2) = EApp (subst x e e1) (subst x e e2)
subst x e (EAbs x' body)
    | x == x'   = EAbs x body
    | otherwise = EAbs x (subst x e body)

isNormalForm :: Expr -> Bool
isNormalForm (EInt _)   = True
isNormalForm (EAbs _ _) = True
isNormalForm (EVar _)   = True
isNormalForm (EApp _ _) = False

In line 21, even if we wrote subst x (interpret e) body, the expr will still terminate. But this is due to the laziness of Haskell. If we write the same thing in ML, it will not terminate.

So maybe we could say, the laziness of Haskell doesn't contribute to the laziness of target language, if we can always find a way to write the interpreter such that whether host language is Haskell or ML, the laziness of target language is the same.