Skip to content

Instantly share code, notes, and snippets.

@rntz
Last active August 7, 2023 04:18
Show Gist options
  • Save rntz/45abb309e1cde70b579405748f9c4163 to your computer and use it in GitHub Desktop.
Save rntz/45abb309e1cde70b579405748f9c4163 to your computer and use it in GitHub Desktop.
{-# LANGUAGE GADTs, TypeFamilies #-}
data Type a where
TNat :: Type Int
TFun :: Type a -> Type b -> Type (a -> b)
type Var a = (Type a, String)
data Expr a where
ENat :: Int -> Expr Int
EVar :: Var a -> Expr a
ELam :: Var a -> Expr b -> Expr (a -> b)
EApp :: Expr (a -> b) -> Expr a -> Expr b
EFix :: Var a -> Expr a -> Expr a
EVal :: Val a -> Expr a -- escape hatch for primitives
type Stream a = [a] -- monotonically increasing infinite streams
type family Val a where
Val Int = Stream Int
Val (a -> b) = Val a -> Val b
-- Are two types the same?
data Same a b where Refl :: Same a a
same :: Type a -> Type b -> Maybe (Same a b)
same TNat TNat = Just Refl
same (TFun a b) (TFun a' b') | (Just Refl, Just Refl) <- (same a a', same b b') = Just Refl
same _ _ = Nothing
data Binding where Bind :: Var a -> Val a -> Binding
type Env = [Binding]
binding :: Var a -> Env -> Val a
binding (_, xname) [] = error ("unbound variable: " ++ xname)
binding x@(xtp, xname) (Bind (ytp, yname) val : env)
| xname == yname, Just Refl <- same xtp ytp = val
| otherwise = binding x env
eval :: Env -> Expr a -> Val a
eval env (EVal v) = v
eval env (ENat x) = xs where xs = x : xs
eval env (EVar x) = binding x env
eval env (ELam x body) = \v -> eval (Bind x v : env) body
eval env (EApp func arg) = eval env func $ eval env arg
-- The magic trick.
eval env (EFix x@(xtp, xname) body) = result
where result = eval (Bind x (delay xtp result) : env) body
delay :: Type a -> Val a -> Val a
delay TNat xs = 0 : xs
delay (TFun a b) f = \x -> delay b (f x)
{-# LANGUAGE GADTs #-}
data Type a where
TNat :: Type Int
TFun :: Type a -> Type b -> Type (a -> b)
type Var a = (Type a, String)
data Expr a where
ENat :: Int -> Expr Int
EVar :: Var a -> Expr a
ELam :: Var a -> Expr b -> Expr (a -> b)
EApp :: Expr (a -> b) -> Expr a -> Expr b
EFix :: Var a -> Expr a -> Expr a
type S a = [a] -- monotonically increasing infinite streams
data Val a where
VNat :: S Int -> Val Int
VFun :: (Val a -> Val b) -> Val (a -> b)
-- Are two types the same?
data Same a b where Refl :: Same a a
same :: Type a -> Type b -> Maybe (Same a b)
same TNat TNat = Just Refl
same (TFun a b) (TFun a' b') | (Just Refl, Just Refl) <- (same a a', same b b') = Just Refl
same _ _ = Nothing
data Binding where Bind :: Var a -> Val a -> Binding
type Env = [Binding]
binding :: Var a -> Env -> Val a
binding (_, xname) [] = error ("unbound variable: " ++ xname)
binding x@(xtp, xname) (Bind (ytp, yname) val : env)
| xname == yname, Just Refl <- same xtp ytp = val
| otherwise = binding x env
app :: Val (a -> b) -> Val a -> Val b
app (VFun f) = f
-- the rope trick
delay :: Type a -> Val a -> Val a
delay TNat val = VNat (0 : (case val of VNat s -> s))
delay (TFun a b) val = VFun (\x -> delay b (app val x))
eval :: Env -> Expr a -> Val a
eval env (ENat x) = VNat xs where xs = x : xs
eval env (EVar x) = binding x env
eval env (ELam x body) = VFun (\v -> eval (Bind x v : env) body)
eval env (EApp func arg) = eval env func `app` eval env arg
eval env (EFix x@(xtp, xname) body) = result
where result = eval (Bind x (delay xtp result) : env) body
-- BUT WHAT DOES IT __DO__???
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment