Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Typed Interpreter in Haskell
{-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NPlusKPatterns #-}
module Main where
import Prelude hiding (lookup, id)
data Ty = TyBool | TyNat | Ty :~> Ty
type family InterpTy (t :: Ty) :: * where
InterpTy TyBool = Bool
InterpTy TyNat = Int
InterpTy (s :~> t) = InterpTy s -> InterpTy t
data Env (ts :: [Ty]) :: * where
Nil :: Env '[]
Cons :: InterpTy t -> Env ts -> Env (t ': ts)
data DeBruijn (ts :: [Ty]) (t :: Ty) :: * where
Stop :: DeBruijn (t ': ts) t
Pop :: DeBruijn ts t -> DeBruijn (s ': ts) t
lookup :: DeBruijn ts t -> Env ts -> InterpTy t
lookup Stop (Cons t _) = t
lookup (Pop i) (Cons _ ts) = lookup i ts
data Expr (ts :: [Ty]) (t :: Ty) :: * where
Var :: DeBruijn ts t -> Expr ts t
T :: Expr ts TyBool
F :: Expr ts TyBool
If :: Expr ts TyBool -> Expr ts a -> Expr ts a -> Expr ts a
Lam :: Expr (s ': ts) t -> Expr ts (s :~> t)
App :: Expr ts (s :~> t) -> Expr ts s -> Expr ts t
Z :: Expr ts TyNat
S :: Expr ts TyNat -> Expr ts TyNat
Rec :: Expr ts TyNat
-> Expr ts a
-> Expr ts (TyNat :~> (a :~> a))
-> Expr ts a
eval :: Env ts -> Expr ts t -> InterpTy t
eval env (Var i) = lookup i env
eval env (S n) = 1 + eval env n
eval _ Z = 0
eval _ T = True
eval _ F = False
eval env (Lam sc) = \e -> eval (Cons e env) sc
eval env (App f x) = eval env f $ eval env x
eval env (If c t f) =
case eval env c of
True -> eval env t
False -> eval env f
eval env (Rec n x f) =
case eval env n of
0 -> eval env x
n' + 1 -> eval env f n' (eval env x)
id :: Expr ts (a :~> a)
id = Lam (Var Stop)
inc :: Expr ts (TyNat :~> TyNat)
inc = Lam (S (Var Stop))
plus :: Expr ts (TyNat :~> (TyNat :~> TyNat))
plus =
Lam (
Lam (
Rec (Var (Pop Stop)) (Var Stop) (
Lam (
Lam (
App inc (App (App plus (Var (Pop Stop))) (Var Stop))
)
)
)
)
)
main :: IO ()
main = print $ eval Nil (App (App plus (S (S (S Z)))) (S (S Z)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.