Eval.hs

module Eval (run) where

import Type
import Infer

import Control.Arrow

import Debug.Trace
ti a b = trace (a ++ show b) b
t' a b = trace (a ++ show b)

deBruijn :: TTerm -> TTerm
deBruijn = deBruijn' []

deBruijn' :: [(String, Int)] -> TTerm -> TTerm
deBruijn' ctx (VarT s ty      ) = case lookup s ctx of
                                    Just m -> VarIT m s ty
                                    _      -> undefined    -- s is a free variable
deBruijn' ctx (AbsT s ty1 t ty2)
                        = AbsT s ty1 (deBruijn' ((s,0):map (second succ) ctx) t) ty2
deBruijn' ctx (AppT  t1 t2 ty ) = AppT (deBruijn' ctx t1) (deBruijn' ctx t2) ty
deBruijn' ctx (PairT t1 t2 ty ) = PairT (deBruijn' ctx t1) (deBruijn' ctx t2) ty
deBruijn' ctx (Prj1T  t ty    ) = Prj1T (deBruijn' ctx t) ty
deBruijn' ctx (Prj2T  t ty    ) = Prj2T (deBruijn' ctx t) ty
deBruijn' ctx (IfT t1 t2 t3 ty) = IfT (deBruijn' ctx t1) (deBruijn' ctx t2) (deBruijn' ctx t3) ty
deBruijn' ctx (ST  t  ty      ) = ST (deBruijn' ctx t) ty
deBruijn' ctx (PT  t  ty      ) = PT (deBruijn' ctx t) ty
deBruijn' ctx t         = t

-- evaluation
shift :: Int -> Int -> TTerm -> TTerm
shift c d (VarIT k str ty)     = VarIT (if k < c then k else k+d) str ty
shift c d (AbsT str ty1 t ty2) = AbsT str ty1 (shift (c+1) d t) ty2
shift c d (AppT t1 t2 ty)      = AppT (shift c d t1) (shift c d t2) ty
shift c d t             = t

subst :: TTerm -> Int -> TTerm -> TTerm 
subst s j (VarIT k str ty     ) = if k == j then s else (VarIT k str ty)
subst s j (AbsT str ty1 tt ty2) = AbsT str ty1 (subst (shift 0 1 s) (j+1) tt) ty2
subst s j (AppT  t1 t2 ty     ) = AppT (subst s j t1) (subst s j t2) ty
subst s j (IfT   t1 t2 t3 ty  ) = IfT (subst s j t1) (subst s j t2) (subst s j t3) ty
subst s j (PairT t1 t2 ty     ) = PairT (subst s j t1) (subst s j t2) ty
subst s j (Prj1T t  ty        ) = Prj1T (subst s j t) ty
subst s j (Prj2T t  ty        ) = Prj2T (subst s j t) ty
subst s j (ST    t  ty        ) = ST (subst s j t) ty
subst s j (PT    t  ty        ) = PT (subst s j t) ty
subst s j t             = t

beta :: TTerm -> TTerm -> TTerm
beta s t = shift 0 (-1) $ subst (shift 0 1 s) 0 t 

eval1 :: TTerm -> Either TTerm TTerm               -- reduce 1 step
eval1 (AppT (AbsT _ _ tt _) v ty) = Left $ beta (eval1' v) tt         -- E-AppAbs
eval1 (AppT  t1 t2  ty) = case eval1 t1 of
                            Left  t' -> Left $ AppT t' t2 ty          -- E-App2
                            Right t' -> Left $ AppT t' (eval1' t2) ty -- E-App1
eval1 (IfT b t2 t3  ty) = case (eval1' b) of
                            TT _ -> Left t2        -- E-IfTrue
                            FT _ -> Left t3        -- E-IfFalse
                            _    -> Right $ IfT (eval1' b) t2 t3 ty -- E-If
eval1 (PairT t1 t2  ty) = Right $ PairT (eval1' t1) (eval1' t2) ty
eval1 (Prj1T (PairT t _ _) _) = Left $ eval1' t
eval1 (Prj1T t      ty) = Right $ Prj1T (eval1' t) ty
eval1 (Prj2T (PairT _ t _) _) = Left $ eval1' t
eval1 (Prj2T t      ty) = Right $ Prj2T (eval1' t) ty
eval1 (ST    t      ty) = Right $ ST (eval1' t) ty
eval1 (PT    (OT _) ty) = Right $ OT ty 
eval1 (PT    (ST t _)      _) = Left  $ eval1' t
eval1 (PT    t      ty) = Left  $ PT (eval1' t) ty
eval1 t                 = Right t

eval1' = either id id . eval1

eval :: TTerm -> TTerm           -- reduce n steps
eval t = case eval1 t of
           Left  t' -> eval t' -- reducible
           Right t' -> t'      -- irreducible

run :: TTerm -> TTerm
run t = eval $ deBruijn t

Infer.hs

module Infer (typeInference) where

import Type

import Control.Applicative
import Control.Arrow
import Control.Lens
import Data.Maybe
import qualified Data.Map as M

-- *** debug
import Debug.Trace
t' s x p = trace (s++show x) p 
ti s x   = trace (s++show x) x
-- ***

-- check constraints
constraints :: Int -> Assump -> Term -> Maybe (Int, [TConst], TTerm)
constraints n env (Var       s) = M.lookup s env >>= (\ty -> Just (n, [], VarT s ty))
constraints n env (App  t1 t2 ) = do (n1, c1, tt1) <- constraints (n+1) env t1
                                     (n2, c2, tt2) <- constraints n1    env t2
                                     let ty1 = getType tt1
                                         ty2 = getType tt2
                                     return (n2, (ty1, ty2 ->: TVar n) : (c1 ++ c2), AppT tt1 tt2 $ TVar n)
constraints n env (Abs   i t2 ) = let nenv = M.insert i (TVar n) env
                                   in constraints (n+1) nenv t2 >>= (\(m, c, tt) -> Just (m, c, AbsT i (TVar n) tt $ TVar n ->: getType tt))
constraints n env  T            = Just (n, [], TT TBool)
constraints n env  F            = Just (n, [], FT TBool)
constraints n env (If t1 t2 t3) = do tt1 <- getTTerm n env t1
                                     tt2 <- getTTerm n env t2
                                     tt3 <- getTTerm n env t3
                                     Just (n, [], IfT tt1 tt2 tt3 $ getType $ tt2)
constraints n env  O            = Just (n, [], OT TNat)
constraints n env (S    t1    ) = do tt1 <- getTTerm n env t1
                                     Just (n, [], ST tt1 TNat)
constraints n env (P    t1    ) = do tt1 <- getTTerm n env t1
                                     Just (n, [], PT tt1 TNat)
constraints n env (Pair t1 t2 ) = do tt1 <- getTTerm n env t1
                                     tt2 <- getTTerm n env t2
                                     let ty1 = getType tt1
                                     let ty2 = getType tt2
                                     return (n, [], PairT tt1 tt2 $ TPair ty1 ty2)
constraints n env (Prj1 t    ) = do tt <- getTTerm n env t
                                    return (n, [], Prj1T tt $ getType tt)
constraints n env (Prj2 t    ) = do tt <- getTTerm n env t
                                    return (n, [], Prj2T tt $ getType tt)


getTTerm :: Int -> Assump -> Term -> Maybe TTerm
getTTerm n env t = (^._3) <$> constraints n env t 


getType :: TTerm -> Type
getType (VarT  _     ty) = ty
getType (VarIT _ _   ty) = ty
getType (AbsT  _ _ _ ty) = ty 
getType (AppT  _ _   ty) = ty
getType (PairT _ _   ty) = ty
getType (Prj1T _     ty) = ty
getType (Prj2T _     ty) = ty
getType (TT          ty) = ty
getType (FT          ty) = ty
getType (IfT   _ _ _ ty) = ty
getType (OT          ty) = ty
getType (ST    _     ty) = ty
getType (PT    _     ty) = ty
getType (PrT   _ _ _ ty) = ty

-- unification
occursCheck :: Int -> Type -> Bool
occursCheck n (TVar n')      = n == n'
occursCheck n (TArr ty1 ty2) = occursCheck n ty1 || occursCheck n ty2
occursCheck n _              = False 

unify :: Subst -> [TConst] -> Maybe Subst
unify env [] = Just env
unify env ((TVar n, TVar n'):cs) = if n == n'
                                     then unify env cs
                                     else unify' env (TVar n) n' cs
unify env ((TVar n, ty     ):cs) = unify' env ty n cs
unify env ((ty    , TVar n ):cs) = unify' env ty n cs
unify env ((TArr ty1 ty2, TArr ty3 ty4):cs) 
                                 = unify env $ (ty1, ty3) : (ty2, ty4) : cs
unify env ((TBool , TBool  ):cs) = unify env cs
unify env ((TNat  , TNat   ):cs) = unify env cs
unify env ((TPair ty1 ty2, TPair ty3 ty4):cs)
                                 = unify env $ (ty1, ty3) : (ty2, ty4) : cs

unify' :: Subst -> Type -> Int -> [TConst] -> Maybe Subst
unify' env ty n cs | occursCheck n ty = Nothing
                   | otherwise        = unify (M.insert n ty $ M.map sub env) $ map (sub *** sub) cs
  where sub = typeSubst $ M.singleton n ty 

-- type substitution
typeSubst :: Subst -> Type -> Type
typeSubst s (TVar n)        = case M.lookup n s of
                                Just t  -> t
                                Nothing -> TVar n
typeSubst s (TArr  ty1 ty2) = typeSubst s ty1 ->: typeSubst s ty2
typeSubst s (TPair ty1 ty2) = TPair (typeSubst s ty1) (typeSubst s ty2)
typeSubst s TBool           = TBool
typeSubst s TNat            = TNat

-- typed term substitution
substitute :: Subst -> TTerm -> TTerm
substitute s (VarT  str ty        ) = VarT    str $ typeSubst s ty
substitute s (VarIT i   str ty    ) = VarIT i str $ typeSubst s ty
substitute s (AbsT  str ty1 t ty2 ) = AbsT  str (typeSubst s ty1) (substitute s t) (typeSubst s ty2)
substitute s (AppT  t1 t2 ty      ) = AppT  (substitute s t1) (substitute s t2) (typeSubst s ty)
substitute s (PairT t1 t2 ty      ) = PairT (substitute s t1) (substitute s t2) (typeSubst s ty)
substitute s (Prj1T t ty) = Prj1T (substitute s t) $ typeSubst s ty
substitute s (Prj2T t ty) = Prj2T (substitute s t) $ typeSubst s ty
substitute s (TT ty  ) = TT $ typeSubst s ty
substitute s (FT ty  ) = FT $ typeSubst s ty
substitute s (IfT   t1 t2 t3 ty   ) = IfT (substitute s t1) (substitute s t2) (substitute s t3) (typeSubst s ty)
substitute s (OT ty  ) = OT $ typeSubst s ty
substitute s (ST t ty) = ST (substitute s t) $ typeSubst s ty
substitute s (PT t ty) = PT (substitute s t) $ typeSubst s ty
substitute s (PrT   t1 t2 t3 ty   ) = PrT (substitute s t1) (substitute s t2) (substitute s t3) $ typeSubst s ty

typeCheck = id

typeInference :: Term -> Maybe TTerm -- Type
typeInference t = do (_, c, u) <- constraints 0 M.empty t
                     s         <- unify M.empty c
                     return $ typeCheck $ substitute s u

Main.hs

import Type
import Parse
import Infer
import Eval

import System.Environment

main = do (code:_) <- getArgs
          case parseTerm code of
            ParseErr err -> putStrLn err
            val -> case typeInference val of
                     Just x -> print $ run x
                     _      -> putStrLn "Type Error"

Parse.hs

module Parse (parseTerm) where

import Type

import Data.Char
import Text.Parsec
import Text.Parsec.Char
import Text.Parsec.String

varLetter :: Parser Char
varLetter = satisfy isLower 

-- variables
pVar = do v <- many1 varLetter
          return $ Var v

-- lambda abstraction
pAbs = do char '\\'
          x <- many1 varLetter 
          char '.'
          y <- pExpr -- pSmallExpr
          return $ Abs x y 

{-
-- pair
pPair = do char '('
           x <- pExpr
           char ','
           y <- pExpr
           char ')'
           return $ Pair x y
-}
-- if ... then ... else ...
pIf = do string "if "
         x <- pSmallExpr
         string " then "
         y <- pSmallExpr
         string " else "
         z <- pSmallExpr
         return $ If x y z

-- truth value
pT = char 'T' >> return T
pF = char 'F' >> return F

-- natural number
pO = char '0' >> return O

pS = do string "S("
        t <- pSmallExpr
        char ')'
        return $ S t

pP = do string "P("
        t <- pSmallExpr
        char ')'
        return $ P t

-- expression
pExpr'  = do char '('
             t <- pExpr
             char ')'
             return t 

-- expressions
pExpr = do l <- many1 pSmallExpr
           return $ foldl1 App l

pSmallExpr = spaces >> (pExpr' <|> pAbs <|> pIf <|> pT <|> pF <|> pO <|> pS <|> pP <|> pVar)

parseTerm :: String -> Term
parseTerm code = case parse pExpr "" code of
                    Left  err -> ParseErr $ show err
                    Right val -> val

Type.hs

module Type 
(Type(..), (->:),
 Term(..), TTerm(..), ($:),
 Context, Binding(..),
 TConst, Assump, Subst) where

import qualified Data.Map as M

-- type (common)
data Type = TArr Type Type -- Type ->: Type
          | TVar Int       -- in a context
          | TPair Type Type
          | TBool
          | TNat
          deriving Eq

instance Show Type where
    show (TArr t1 t2) = concat ["(", show t1, " -> " ++ show t2, ")"]
    show (TVar i)     = "T_" ++ show i
    show (TPair t1 t2) = show t1 ++ " × " ++ show t2
    show  TBool       = "Bool"
    show  TNat        = "Nat"

-- alias
(->:) = TArr

-- typeless terms
data Term = Var String      -- variable
          | Abs String Term -- lambda abstraction
          | App Term   Term -- application
          | Pair Term Term | Prj1 Term | Prj2 Term
          | T | F | If Term Term Term
          | O | S Term | P Term | Pr Term Term 
          | ParseErr String 
          deriving Show

-- alias
($:) = App

-- typed terms
data TTerm = VarT  String     Type -- normal variable
           | VarIT Int String Type -- de bruijn index & normal variable
           | AbsT String Type TTerm Type -- lambda abstraction
           | AppT TTerm TTerm Type -- application
           | TT Type | FT Type | IfT TTerm TTerm TTerm Type -- boolean
           | OT Type | ST TTerm Type | PT TTerm Type | PrT TTerm TTerm TTerm Type
           | PairT TTerm TTerm Type | Prj1T TTerm Type | Prj2T TTerm Type 
           deriving Eq

instance Show TTerm where
    show (VarT    s t) = s ++ " :" ++ show t
    show (VarIT i s t) = s ++ " :" ++ show t
    show (AbsT  s ty1 t ty2) = concat ["(\\", s, " :", show ty1, ". ", show t, " :", show ty2, ")"]
    show (AppT  t1 t2 ty2)   = concat ["(", show t1, ") (", show t2, ")", " :", show ty2]
    show (PairT t1 t2 ty)    = concat ["(", show t1, ", ", show t2, ") :", show ty]
    show (TT t)  = "T :" ++ show t
    show (FT t)  = "F :" ++ show t
    show (IfT t1 t2 t3 t) = concat ["(if ", show t1, " then ", show t2, " else ", show t3, ") :", show t]
    show (OT t)  = "O :" ++ show t 
    show (ST t ty)     = "S(" ++ show t ++ ") :" ++ show ty
    show (PT t ty)     = "P(" ++ show t ++ ") :" ++ show ty
    show (PrT t1 t2 t3 ty) = "Pr" 

-- used at type checking
type Context = [(String, Binding)]        -- Γ : String |-> Binding

data Binding = NBind | TBind | VBind Type 
             deriving Show

-- used at type inference
type TConst = (Type, Type)

type Assump = M.Map String Type

type Subst  = M.Map Int    Type