Skip to content

Instantly share code, notes, and snippets.

@AndrasKovacs
Last active January 7, 2023 17:22
Show Gist options
  • Save AndrasKovacs/c7d385aa117929503feb to your computer and use it in GitHub Desktop.
Save AndrasKovacs/c7d385aa117929503feb to your computer and use it in GitHub Desktop.
Lambda calculus on the type level with GHC 7.11.20151212.
{-# LANGUAGE
TypeInType, UndecidableInstances, TypeOperators, GADTs, TypeFamilies #-}
import Data.Kind
import GHC.Prim
import Data.Proxy
data Fun a b
type a ~> b = Fun a b -> Type
infixr 0 ~>
infixl 9 @@
type family (@@) (f :: a ~> b) (x :: a) :: b
data Con1 :: (a -> b) -> (a ~> b)
data Con2 :: (a -> b -> c) -> (a ~> b ~> c)
data Con3 :: (a -> b -> c -> d) -> (a ~> b ~> c ~> d)
type instance Con1 c @@ a = c a
type instance Con2 c @@ a = Con1 (c a)
type instance Con3 c @@ a = Con2 (c a)
infixr 0 $
type ($) f x = f x
data Var :: [Type] -> Type -> Type where
VZ :: Var (t ': ts) t
VS :: Var ts t -> Var (t' ': ts) t
data Term :: [Type] -> Type -> Type where
T :: t -> Term ts t
V :: Var ts t -> Term ts t
L :: Term (t ': ts) t' -> Term ts (t ~> t')
Fix :: Term (Delay t ': ts) t -> Term ts t
(:$) :: Term ts (a ~> b) -> Term ts a -> Term ts b
Let :: Term ts t -> Term (t ': ts) t' -> Term ts t' -- only sugar
Case :: Term ts t -> [(Term ts t, Term ts t')] -> Term ts t'
infixl 9 :$
data Env :: [Type] -> Type where
ENil :: Env '[]
ECons :: t -> Env cxt -> Env (t ': cxt)
type family LookupVar (v :: Var cxt t) (env :: Env cxt) :: t where
LookupVar VZ (ECons x env) = x
LookupVar (VS v) (ECons x env) = LookupVar v env
type family Eval (term :: Term '[] t) :: t where
Eval term = Eval_ term ENil
type family Eval_ (term :: Term cxt t) (env :: Env cxt) :: t where
Eval_ (T x) env = x
Eval_ (V v) env = LookupVar v env
Eval_ (f :$ x) env = Eval_ f env @@ Eval_ x env
Eval_ (L e) env = LamS e env
Eval_ (Fix e) env = Fix_ e env
Eval_ (Let x e) env = Eval_ (L e :$ x) env
Eval_ (Case e cs) env = Eval_ (Lookup (Eval_ e env) (EvalCases env cs)) env
type family Lookup k xs where
Lookup k ('(k , v) ': xs) = v
Lookup k ('(k', v) ': xs) = Lookup k xs
type family EvalCases
(env :: Env ts) (cs :: [(Term ts t, Term ts t')]) :: [(t, Term ts t')] where
EvalCases env '[] = '[]
EvalCases env ('(c, e) ': cs) = '(Eval_ c env , e) ': EvalCases env cs
type family Fix_ (e :: Term (Delay t ': cxt) t) (env :: Env cxt) :: t where
Fix_ e env = Eval_ e (ECons ('Delay (FixS e) env) env)
data FixS :: Term (Delay t ': cxt) t -> Env cxt ~> t
type instance FixS e @@ env = Fix_ e env
data LamS :: Term (a ': cxt) b -> Env cxt -> a ~> b
type instance LamS e env @@ x = Eval_ e (ECons x env)
data Delay b where
Delay :: (a ~> b) -> a -> Delay b
type family Force (x :: Delay t) :: t where
Force ('Delay f a) = f @@ a
data ForceS :: Delay t ~> t
type instance ForceS @@ dt = Force dt
-- examples
type V0 = VZ
type V1 = VS V0
type V2 = VS V1
type V3 = VS V2
type V4 = VS V3
type V5 = VS V4
type Flip = L $ L $ L $ V V2 :$ V V0 :$ V V1
type Id = L $ V V0
type Const = L $ L $ V V1
data Nat = Z | S Nat
type family Pred n where
Pred (S n) = n
data PredS :: Nat ~> Nat
type instance PredS @@ n = Pred n
-- Add = fix $ \add a b -> case a of 0 -> b; a -> S (add (pred a) b)
type Add =
Fix $ L $ L $
Case (V V1) '[
'(T Z , V V0),
'(V V1, T (Con1 S) :$ (T ForceS :$ V V2 :$ (T PredS :$ V V1) :$ V V0))
]
-- Mul = fix $ \mul a b -> case a of 0 -> a; a -> add b (mul (pred a) b)
type Mul =
Fix $ L $ L $
Case (V V1) '[
'(T Z , T Z),
'(V V1, Add :$ V V0 :$ (T ForceS :$ V V2 :$ (T PredS :$ V V1) :$ V V0))
]
-- Non de-Bruijn version, doesn't work because of buggy stuck reduction
{.
{-# language UndecidableInstances #-}
import Data.Kind
import GHC.Prim
import Data.Proxy
import GHC.TypeLits
import Data.Type.Equality
import Data.Type.Bool
data Fun a b
type a ~> b = Fun a b -> Type
infixr 0 ~>
infixl 9 @@
type family (@@) (f :: a ~> b) (x :: a) :: b
infixr 0 $
type ($) f x = f x
type Cxt = [(Symbol, Type)]
type family Lookup (x :: a) (xs :: [(a, b)]) :: b where
Lookup x ('(y, b) ': xs) = If (x == y) b (Lookup x xs)
type family If' b (x :: t) (y :: f) :: If b t f where
If' True t f = t
If' False t f = f
data Term :: Cxt -> Type -> Type where
V_ :: Proxy v -> Lookup v cxt :~: a -> Term cxt a
L_ :: Proxy v -> Term ('(v, a) ': cxt) b -> Term cxt (a ~> b)
(:$) :: Term ts (a ~> b) -> Term ts a -> Term ts b
type V v = V_ ('Proxy :: Proxy v) Refl
type Lam v t = L_ ('Proxy :: Proxy v) t
data Env :: Cxt -> Type where
ENil :: Env '[]
ECons :: t -> Env cxt -> Env ('(s, t) ': cxt)
type family EvalVar (p :: Proxy (v :: Symbol)) (env :: Env cxt) :: Lookup v cxt where
EvalVar (p :: Proxy v) (ECons x xs :: Env ('(v', t) ': cxt)) = If' (v == v') x (EvalVar p xs)
type family Coe (eq :: a :~: b) (x :: a) :: b where
Coe Refl x = x
type Eval t = Eval_ t ENil
type family Eval_ (t :: Term cxt a) (env :: Env cxt) :: a where
Eval_ (V_ p eq) env = Coe eq (EvalVar p env)
Eval_ (f :$ x) env = Eval_ f env @@ Eval_ x env
Eval_ (L_ p t) env = LamS t env
data LamS :: Term ('(v, a) ': cxt) b -> Env cxt -> a ~> b
type instance LamS t env @@ x = Eval_ t (ECons x env)
type Foo = Eval (Lam "x" (V "x"))
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment