Navigation Menu

Skip to content

Instantly share code, notes, and snippets.

@sjoerdvisscher
Created August 25, 2021 12:20
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save sjoerdvisscher/d3c6e9717a5e1f843acc91d4049830ea to your computer and use it in GitHub Desktop.
Save sjoerdvisscher/d3c6e9717a5e1f843acc91d4049830ea to your computer and use it in GitHub Desktop.
Calculating Dependently-Typed Compilers
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment