Create a gist now

Instantly share code, notes, and snippets.

@gergoerdi /STLC.hs
Last active Aug 29, 2015

{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module STLC where
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Equality
data Type = Base
| Arrow Type Type
deriving (Show, Eq)
type Sym = String
-- | Untyped representation of STLC, could be not well-typed or even well-scoped
data Term = Var Sym
| Lam Sym Type Term
| App Term Term
deriving Show
-- | A (typed) variable is an index into a context of types
data TVar (ts :: [Type]) (a :: Type) where
Here :: TVar (t ': ts) t
There :: TVar ts a -> TVar (t ': ts) a
deriving instance Show (TVar ctx a)
-- | Typed representation of STLC: well-scoped and well-typed by construction
data TTerm (ctx :: [Type]) (a :: Type) where
TConst :: TTerm ctx Base
TVar :: TVar ctx a -> TTerm ctx a
TLam :: TTerm (a ': ctx) b -> TTerm ctx (Arrow a b)
TApp :: TTerm ctx (Arrow a b) -> TTerm ctx a -> TTerm ctx b
deriving instance Show (TTerm ctx a)
-- | Interpretation of types
type family Interp (t :: Type) where
Interp Base = ()
Interp (Arrow t1 t2) = Interp t1 -> Interp t2
-- | An environment gives the value of all variables in scope in a given context
data Env (ts :: [Type]) where
Nil :: Env '[]
Cons :: Interp t -> Env ts -> Env (t ': ts)
lookupVar :: TVar ts a -> Env ts -> Interp a
lookupVar Here (Cons x _) = x
lookupVar (There v) (Cons _ xs) = lookupVar v xs
-- | Evaluate a term of STLC. This function is total!
eval :: Env ctx -> TTerm ctx a -> Interp a
eval env TConst = ()
eval env (TVar v) = lookupVar v env
eval env (TLam lam) = \x -> eval (Cons x env) lam
eval env (TApp f e) = eval env f $ eval env e
$(genSingletons [''Type])
$(singDecideInstance ''Type)
-- | Existential version of 'TTerm'
data SomeTerm (ctx :: [Type]) where
TheTerm :: Sing a -> TTerm ctx a -> SomeTerm ctx
-- | Existential version of 'TVar'
data SomeVar (ctx :: [Type]) where
TheVar :: Sing a -> TVar ctx a -> SomeVar ctx
-- | A typed binder of variable names
data Binder (ctx :: [Type]) where
BNil :: Binder '[]
BCons :: Sym -> Sing t -> Binder ts -> Binder (t ': ts)
-- | Type inference for STLC
infer :: Binder ctx -> Term -> Maybe (SomeTerm ctx)
infer bs (Var v) = do
TheVar t v' <- inferVar bs v
return $ TheTerm t $ TVar v'
infer bs (App f e) = do
TheTerm (SArrow t0 t) f' <- infer bs f
TheTerm t0' e' <- infer bs e
Refl <- testEquality t0 t0'
return $ TheTerm t $ TApp f' e'
infer bs (Lam v ty e) = case toSing ty of
SomeSing t0 -> do
TheTerm t e' <- infer (BCons v t0 bs) e
return $ TheTerm (SArrow t0 t) $ TLam e'
inferVar :: Binder ctx -> Sym -> Maybe (SomeVar ctx)
inferVar (BCons u t bs) v
| v == u = return $ TheVar t Here
| otherwise = do
TheVar t' v' <- inferVar bs u
return $ TheVar t' $ There v'
inferVar _ _ = Nothing
-- | Typechecker for STLC
check :: forall ctx a. (SingI a) => Binder ctx -> Term -> Maybe (TTerm ctx a)
check bs e = do
TheTerm t' e' <- infer bs e
Refl <- testEquality t t'
return e'
where
t = singByProxy (Proxy :: Proxy a)
-- | Typechecker for closed terms of STLC
check_ :: (SingI a) => Term -> Maybe (TTerm '[] a)
check_ = check BNil
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment