Calculating Dependently-Typed Compilers

CalcComp.hs

-- https://icfp21.sigplan.org/details/icfp-2021-papers/21/Calculating-Dependently-Typed-Compilers-Functional-Pearl-
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-}
import Control.Applicative
import Data.Kind
import Data.Type.Equality

type family (a :: Bool) || (b :: Bool) :: Bool where
  'False || b = b
  'True || b = 'True

type family (a :: Bool) && (b :: Bool) :: Bool where
  'False && b = 'False
  'True && b = b

data SBool :: Bool -> Type where
  STrue :: SBool 'True
  SFalse :: SBool 'False

data Exp :: Bool -> Type where
  Val :: Integer -> Exp 'False
  Add :: SBool a -> SBool b -> Exp a -> Exp b -> Exp (a || b)
  Throw :: Exp 'True
  Catch :: SBool a -> SBool b -> Exp a -> Exp b -> Exp (a && b)

eval' :: Exp b -> Maybe Integer
eval' (Val n) = Just n
eval' (Add _ _ x y) = liftA2 (+) (eval' x) (eval' y)
eval' Throw = Nothing
eval' (Catch _ _ x h) = eval' x <|> eval' h

eval :: b :~: 'False -> Exp b -> Integer
eval Refl (Val n) = n
eval Refl (Add SFalse SFalse x y) = eval Refl x + eval Refl y
eval Refl (Catch SFalse _ x _) = eval Refl x
eval Refl (Catch STrue SFalse x h) = case eval' x of
  Just n -> n
  Nothing -> eval Refl h

data Ty :: Type where
  Nat :: Ty
  Han :: [Ty] -> [Ty] -> Ty

type family El (ty :: Ty) :: Type where
  El 'Nat = Integer
  El ('Han s s') = Code s s'

data STy :: Ty -> Type where
  SNat :: STy 'Nat
  SHan :: SList s -> SList s' -> STy ('Han s s')

class IsTy (t :: Ty) where
  sTy :: STy t
instance IsTy 'Nat where sTy = SNat
instance (IsList s, IsList s') => IsTy ('Han s s') where sTy = SHan sList sList

data SList :: [Ty] -> Type where
  SNil :: SList '[]
  SCons :: STy t -> SList ts -> SList (t ': ts)

class IsList (xs :: [Ty]) where
  sList :: SList xs
instance IsList '[] where sList = SNil
instance (IsTy t, IsList ts) => IsList (t ': ts) where sList = SCons sTy sList

sAppend :: SList xs -> SList ys -> SList (xs ++ ys)
sAppend SNil ys = ys
sAppend (SCons x xs) ys = SCons x (sAppend xs ys)

type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

data Code :: [Ty] -> [Ty] -> Type where
  PUSH :: Integer -> Code ('Nat ': s) s' -> Code s s'
  ADD :: Code ('Nat ': s) s' -> Code ('Nat ': 'Nat ': s) s'
  THROW :: SList s'' -> SList s -> Code (s'' ++ ('Han s s' ': s)) s'
  MARK :: Code s s' -> Code ('Han s s' ': s) s' -> Code s s'
  UNMARK :: Code (t ': s) s' -> Code (t ': 'Han s s' ': s) s'
  HALT :: Code s s

comp' :: forall b s s' s''. IsList s' => SList s'' -> SList s -> Exp b -> Code ('Nat ': (s'' ++ ('Han s s' ': s))) s' -> Code (s'' ++ ('Han s s' ': s)) s'
comp' _ _ (Val n) c = PUSH n c
comp' s'' s (Add _ _ x y) c = comp' s'' s x (comp' (SCons SNat s'') s y (ADD c))
comp' s'' s Throw _ = THROW s'' s
comp' s'' s (Catch _ _ x h) c = MARK (comp' s'' s h c) (comp' SNil (sAppend s'' (SCons (SHan s (sList @s')) s)) x (UNMARK c))

comp :: (IsList s, IsList s') => b :~: 'False -> Exp b -> Code ('Nat ': s) s' -> Code s s'
comp Refl (Val n) c = PUSH n c
comp Refl (Add SFalse SFalse x y) c = comp Refl x (comp Refl y (ADD c))
comp Refl (Catch SFalse _ x _) c = comp Refl x c
comp Refl (Catch STrue SFalse x h) c = MARK (comp Refl h c) (comp' SNil sList x (UNMARK c))

compile :: IsList s => b :~: 'False -> Exp b -> Code s ('Nat ': s)
compile p e = comp p e HALT

data Stack :: [Ty] -> Type where
  E :: Stack '[]
  (:>) :: El t -> Stack ts -> Stack (t ': ts)

exec :: Code s s' -> Stack s -> Stack s'
exec (PUSH x c) s = exec c (x :> s)
exec (ADD c) (m :> (n :> s)) = exec c ((m + n) :> s)
exec (THROW s'' s') s = throw s'' s' s
exec (MARK h c) s = exec c (h :> s)
exec (UNMARK c) (x :> (_ :> s)) = exec c (x :> s)
exec HALT s = s

throw :: SList s'' -> SList s -> Stack (s'' ++ ('Han s s' ': s)) -> Stack s'
throw SNil _ (h :> st) = exec h st
throw (SCons _ s'') s (_ :> st) = throw s'' s st