-
-
Save isubasinghe/67ab36d51b686686e50b821ac523a8b3 to your computer and use it in GitHub Desktop.
Well-typed interpreter from the Idris tutorial (http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf) in Haskell.
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, GADTs, TypeOperators, TypeFamilies, DataKinds #-} | |
| data Type = TInt | TBool | Type :=> Type | |
| -- Needs GHC >= 7.8 | |
| type family Interp (t :: Type) where | |
| Interp TInt = Int | |
| Interp TBool = Bool | |
| Interp (a :=> b) = Interp a -> Interp b | |
| data Var (cxt :: [Type]) (t :: Type) where | |
| ZVar :: Var (t ': ts) t | |
| SVar :: Var ts t -> Var (t2 ': ts) t | |
| data Expr (cxt :: [Type]) (t :: Type) where | |
| Val :: Int -> Expr cxt TInt | |
| Var :: Var cxt t -> Expr cxt t | |
| Lam :: Expr (a ': cxt) t -> Expr cxt (a :=> t) | |
| Op :: (Interp a -> Interp b -> Interp c) -> Expr cxt a -> Expr cxt b -> Expr cxt c | |
| App :: Expr cxt (a :=> b) -> Expr cxt a -> Expr cxt b | |
| If :: Expr cxt TBool -> Expr cxt a -> Expr cxt a -> Expr cxt a | |
| data Env (cxt :: [Type]) where | |
| ZEnv :: Env '[] | |
| SEnv :: Interp t -> Env ts -> Env (t ': ts) | |
| lookupVar :: Var cxt t -> Env cxt -> Interp t | |
| lookupVar ZVar (SEnv x xs) = x | |
| lookupVar (SVar i) (SEnv _ xs) = lookupVar i xs | |
| lookupVar _ _ = undefined | |
| eval :: Env cxt -> Expr cxt t -> Interp t | |
| eval env = \case | |
| Val i -> i | |
| Op f a b -> f (eval env a) (eval env b) | |
| Var i -> lookupVar i env | |
| Lam f -> \x -> eval (SEnv x env) f | |
| App f a -> eval env f $ eval env a | |
| If p a b -> if eval env p then eval env a else eval env b | |
| eval' :: Expr '[] t -> Interp t | |
| eval' = eval ZEnv |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment