Created
December 29, 2020 20:52
-
-
Save lunalunaa/c061158a7d742fbd48392443bc8fc014 to your computer and use it in GitHub Desktop.
Simply Typed Lambda Calculus
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE LambdaCase #-} | |
| import Data.Maybe | |
| data Ty | |
| = Base | |
| | TyArr Ty Ty | |
| deriving (Show, Eq) | |
| data Term | |
| = TmVar Integer | |
| | TmAbs String Ty Term | |
| | TmApp Term Term | |
| deriving (Show, Eq) | |
| -- typing: use stack to represent context | |
| type Gamma = [TypeBinding] | |
| type TypeBinding = (Integer, Ty) | |
| gammaShift :: Gamma -> Gamma | |
| gammaShift [] = [] | |
| gammaShift ((i, ty) : l) = (i+1, ty) : gammaShift l | |
| gammaPush :: TypeBinding -> Gamma -> Gamma | |
| gammaPush g ctx = g : gammaShift ctx | |
| getTypeFromCtx :: Gamma -> Integer -> Ty | |
| getTypeFromCtx ctx i = fromMaybe (error "error, var not found") $ lookup i ctx | |
| typeOf :: Gamma -> Term -> Ty | |
| typeOf ctx = \case | |
| TmVar i -> getTypeFromCtx ctx i | |
| TmAbs _ tyT1 t2 -> let ctx' = gammaPush (0,tyT1) ctx in | |
| let tyT2 = typeOf ctx' t2 in | |
| TyArr tyT1 tyT2 | |
| TmApp t1 t2 -> case tyT1 of | |
| TyArr tyT11 tyT12 -> if tyT2 == tyT11 | |
| then tyT12 | |
| else error "parameter mismatch" | |
| _ -> error "arrow expected" | |
| where tyT1 = typeOf ctx t1 | |
| tyT2 = typeOf ctx t2 | |
| -- big-step evaluation | |
| termShift :: Integer -> Term -> Term | |
| termShift d = walk 0 | |
| where | |
| walk :: Integer -> Term -> Term | |
| walk c t = case t of | |
| TmVar x -> if x > c then TmVar (x + d) else t | |
| TmAbs x ty t1 -> TmAbs x ty $ walk (c+1) t1 | |
| TmApp t1 t2 -> TmApp (walk c t1) (walk c t2) | |
| termSubst :: Integer -> Term -> Term -> Term | |
| termSubst j s = walk 0 | |
| where | |
| walk :: Integer -> Term -> Term | |
| walk c t = case t of | |
| TmVar x -> if x == j + c then termShift c s else t | |
| TmAbs x ty t1 -> TmAbs x ty $ walk (c+1) t1 | |
| TmApp t1 t2 -> TmApp (walk c t1) (walk c t2) | |
| termSubstTop :: Term -> Term -> Term | |
| termSubstTop s t = termShift (-1) $ termSubst 0 (termShift 1 s) t | |
| isval :: Term -> Bool | |
| isval = \case | |
| TmAbs{} -> True | |
| _ -> False | |
| eval :: Term -> Term | |
| eval = \case | |
| TmApp t1 t2 -> case eval t1 of | |
| TmAbs _ _ t1' -> let v2' = eval t2 in | |
| if isval v2' | |
| then eval $ termSubstTop v2' t1' | |
| else TmApp t1' t2 | |
| t1'' -> TmApp t1'' t2 | |
| t -> t | |
| --- printing | |
| type Context = [(Integer, String)] | |
| contextShift :: Context -> Context | |
| contextShift [] = [] | |
| contextShift ((i, str) : l) = (i+1, str) : contextShift l | |
| contextPush :: String -> Context -> Context | |
| contextPush name ctx = (0, name) : contextShift ctx | |
| freshName :: [String] -> String -> String | |
| freshName used x | |
| | x `elem` used = freshName used $ nextName x | |
| | otherwise = x | |
| nextName :: String -> String | |
| nextName name = name ++ "'" | |
| printExp :: Context -> Term -> String | |
| printExp ctx = \case | |
| TmVar i -> fromMaybe (error "error, var not found") $ lookup i ctx | |
| TmAbs name _ t -> let name' = freshName (map snd ctx) name in | |
| let ctx' = contextPush name' ctx in | |
| "lambda: " ++ name' ++ ". " ++ printExp ctx' t | |
| TmApp t1 t2 -> printExp ctx t1 ++ " " ++ printExp ctx t2 | |
| printExpTop :: Term -> String | |
| printExpTop = printExp [] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment