Context.hs

module Untyped.Context where

type Context = [String]

mkContext :: Context
mkContext = []

bindVarName :: Context -> String -> Context
bindVarName ctx x = x : ctx

getVarName :: Context -> Int -> String
getVarName ctx n =
  if length ctx > n
     then ctx !! n
     else error $ ("Requested index " ++ show n
                   ++ " of Context of length " ++ show (length ctx))
                   
freshVarName :: Context -> String -> (Context, String)
freshVarName ctx x =
  let x' = getFreshName ctx x
  in  (bindVarName ctx x', x')
  
getFreshName :: Context -> String -> String
getFreshName [] x = x
getFreshName ctx@(b:bs) x
  | x == b    = getFreshName ctx (x ++ "'")
  | otherwise = getFreshName bs x

Evaluator.hs

module Untyped.Evaluator where

import Untyped.Context
import Untyped.Syntax

-- Variable Shifting and Substitution
--

shiftTerm :: Int -> Term -> Term
shiftTerm d t = walk 0 t
  where walk c t =
          case t of
            TermVar x n   -> 
              if x >= c
                then TermVar (x+d) (n+d)
                else TermVar x     (n+d)
            TermAbs x t1  ->
              TermAbs x (walk (c+1) t1)
            TermApp t1 t2 ->
              TermApp (walk c t1) (walk c t2)

substTerm :: Int -> Term -> Term -> Term
substTerm j s t = walk 0 t
  where walk c t =
          case t of
            TermVar x n -> 
              if x == j+c
                 then shiftTerm c s
                 else TermVar x n
            TermAbs x t1 ->
              TermAbs x (walk (c+1) t1)
            TermApp t1 t2 ->
              TermApp (walk c t1) (walk c t2)

substTopTerm :: Term -> Term -> Term
substTopTerm s t = shiftTerm (-1) (substTerm 0 (shiftTerm 1 s) t)

-- Evaluation
--

isValue :: Context -> Term -> Bool
isValue _ (TermAbs _ _) = True
isValue _ _             = False

eval1 :: Context -> Term -> Maybe Term
eval1 ctx t =
  case t of
    TermApp (TermAbs _ t12) v2 -> 
      if isValue ctx v2
        then Just $ substTopTerm v2 t12
        else Nothing
    TermApp t1 t2              ->
      if isValue ctx t1
         then let t2' = eval1 ctx t2
              in  case t2' of
                    Just t2'' -> Just $ TermApp t1 t2''
                    Nothing   -> Nothing
         else let t1' = eval1 ctx t1
              in  case t1' of
                    Just t1'' -> Just $ TermApp t1'' t2
                    Nothing   -> Nothing
    _ -> Nothing

eval :: Context -> Term -> Term
eval ctx t =
  case eval1 ctx t of
    Just t' -> eval ctx t'
    Nothing -> t

Syntax.hs

module Untyped.Syntax where

import Untyped.Context

data Term = TermVar Int Int
          | TermAbs String Term
          | TermApp Term Term
          deriving (Show)

showTerm :: Context -> Term -> String
showTerm ctx t =
  case t of
    TermVar _ n   -> 
      getVarName ctx n
    TermAbs x t1  -> 
      let (ctx', x') = freshVarName ctx x
      in  "(lambda " ++ x' ++ "." ++ showTerm ctx' t1 ++ ")"
    TermApp t1 t2 -> 
      "(" ++ showTerm ctx t1 ++ " " ++ showTerm ctx t2 ++ ")"