Small typesafe imperative embedded language

Imp.hs

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Singletons.Prelude
import GHC.Exts
import Data.List

data NotInScopeError sym

type family LookupTy sym cxt where
  LookupTy sym ( '(sym' , ty) ': cxt) =
    If (sym :== sym') ty (LookupTy sym cxt)
  LookupTy sym '[] = NotInScopeError sym
  
data St cxt where
  Assign :: Sing sym -> Exp cxt (LookupTy sym cxt) -> St cxt -> St cxt
  Decl   :: Sing sym -> Exp cxt ty -> St ('(sym,  ty) ': cxt) -> St cxt
  While  :: Exp cxt Bool -> St cxt -> St cxt -> St cxt
  End    :: St cxt

data Exp (cxt :: [(Symbol, *)]) t where
  EBool :: Bool -> Exp cxt Bool
  EInt  :: Int  -> Exp cxt Int
  EAdd  :: Exp cxt Int -> Exp cxt Int -> Exp cxt Int
  ENot  :: Exp cxt Bool -> Exp cxt Bool
  EVar  :: Sing sym -> Exp cxt (LookupTy sym cxt)
  EEq   :: Exp cxt Int -> Exp cxt Int -> Exp cxt Bool

data Env cxt where
  Nil  :: Env '[]
  (:>) :: (Sing sym, ty) -> Env cxt -> Env ('(sym, ty) ': cxt)
infixr 5 :>

lookupVar :: Sing (sym :: Symbol) -> Env cxt -> LookupTy sym cxt
lookupVar sym Nil = error "impossible"
lookupVar sym ((sym' , v) :> cxt) = case sym %:== sym' of
  STrue  -> v
  SFalse -> lookupVar sym cxt

updateEnv :: forall sym cxt. Sing sym -> Exp cxt (LookupTy sym cxt) -> Env cxt -> Env cxt
updateEnv sym e env = go e env where
  go :: forall cxt'. Exp cxt (LookupTy sym cxt') -> Env cxt' -> Env cxt'
  go e Nil = error "impossible"
  go e ((sym' , v) :> cxt) = case sym %:== sym' of
    STrue  -> (sym' , evalExp e env) :> cxt
    SFalse -> (sym' , v) :> go e cxt

evalExp :: Exp cxt t -> Env cxt -> t
evalExp (EBool b)  _   = b
evalExp (EInt  n)  _   = n
evalExp (EAdd a b) env = evalExp a env + evalExp b env
evalExp (ENot b)   env = not $ evalExp b env
evalExp (EVar s)   env = lookupVar s env
evalExp (EEq a b)  env = evalExp a env == evalExp b env

evalSt ::forall cxt. St cxt -> Env cxt -> Env cxt
evalSt (Assign sym e st) env = evalSt st (updateEnv sym e env)
evalSt (Decl sym e st)   env = case evalSt st ((sym, evalExp e env) :> env) of
  _ :> env' -> env'
evalSt (While b body st) env = go env where
  go env | evalExp b env = go (evalSt body env)
  go env = evalSt st env
evalSt End env = env

instance Show (Sing (sym :: Symbol)) where
  show = show . fromSing

type family AllCxt c (cxpt :: [(Symbol, *)]) :: Constraint where
  AllCxt c '[] = ()
  AllCxt c ( '( sym , t ) ': cxt) = (c (Sing sym, t), AllCxt c cxt)
  
instance AllCxt Show cxt => Show (Env cxt) where
  show cxt = "[" ++ intercalate ", " (toStringList cxt) ++ "]" where
    toStringList :: forall cxt. AllCxt Show cxt => Env cxt -> [String]
    toStringList Nil        = []
    toStringList (x :> cxt) = show x : toStringList cxt

-- add 10 to "foo", assign False to "bar"
test1 :: St [ '( "foo", Int), '("bar", Bool) ]
test1 =
  Assign (sing :: Sing "foo") (EAdd (EVar (sing :: Sing "foo")) (EInt 10)) $
  Assign (sing :: Sing "bar") (EBool False) $
  End

-- increment "foo" until it's 10
test2 :: St '[ '( "foo", Int) ]
test2 = 
  While (ENot (EEq (EVar (sing :: Sing "foo")) (EInt 10))) (
    Assign (sing :: Sing "foo") (EAdd (EVar (sing :: Sing "foo")) (EInt 1))
    End)    
  End