Skip to content

Instantly share code, notes, and snippets.

@timsueberkrueb
Last active October 19, 2020 07:58
Show Gist options
  • Save timsueberkrueb/5275cb940258f833800fd7c864f81759 to your computer and use it in GitHub Desktop.
Save timsueberkrueb/5275cb940258f833800fd7c864f81759 to your computer and use it in GitHub Desktop.
import Data.Vect
import Data.Fin
%default total
%access public export
-- Shortcut operator for application
infixl 7 $$
data Typ : Type where
TLam : Typ -> Typ -> Typ
TNat : Typ
||| Typing Context
||| A typing context is a vector of types. The index of a type
||| is the de-Bruijn index of the corresponding variable.
||| The variable of the last binder comes first.
Ctx : {len : Nat} -> Type
Ctx {len} = Vect len Typ
||| Terms with intrinsic typing judgement
data Term : Typ -> Ctx -> Type where
Var : Elem a ctx -> Term a ctx
Lam : Term b (a :: ctx) -> Term (TLam a b) ctx
App : Term (TLam a b) ctx -> Term a ctx -> Term b ctx
Zero : Term TNat ctx
Suc : Term TNat ctx -> Term TNat ctx
Case : Term TNat ctx
-> Term a ctx
-> Term a (TNat :: ctx)
-> Term a ctx
Fix : Term a (a :: ctx) -> Term a ctx
($$) : Term (TLam a b) ctx -> Term a ctx -> Term b ctx
($$) = App
lookup : Ctx {len} -> Fin len -> Typ
lookup (a :: ctx) FZ = a
lookup (_ :: ctx) (FS n) = lookup ctx n
count : {ctx : Ctx {len}} -> (n : Fin len) -> Elem (lookup ctx n) ctx
count {ctx = _ :: ctx} FZ = Here
count {ctx = _ :: ctx} (FS n) = There (count n)
var : {ctx : Ctx {len}} -> (n : Fin len) -> Term (lookup ctx n) ctx
var n = Var (count n)
||| Extension lemma
||| This is used in rename. It is needed in terms that extend the context
||| with bound variables (e.g. Lam, Fix, Case)
ext : (Elem a ctx1 -> Elem a ctx2)
-> (Elem a (b :: ctx1) -> Elem a (b :: ctx2))
ext p Here = Here
ext p (There x) = There (p x)
||| Renaming of variables
||| rename takes a function which maps a de Bruijn index from ctx1
||| to another de Bruijn index in ctx2
||| For example, `rename There t` shifts the index of free variables
||| in `t` up by one, bound variables are untouched.
rename : ({a : _} -> Elem a ctx1 -> Elem a ctx2)
-> ({a : _} -> Term a ctx1 -> Term a ctx2)
rename p (Var x) = Var (p x)
rename p (Lam x) = Lam (rename (ext p) x)
rename p (App x y) = (App (rename p x) (rename p y))
rename p Zero = Zero
rename p (Suc x) = Suc (rename p x)
rename p (Case c x y) = (Case (rename p c) (rename p x) (rename (ext p) y))
rename p (Fix x) = Fix (rename (ext p) x)
exts : (Elem a ctx1 -> Term a ctx2)
-> (Elem a (b :: ctx1) -> Term a (b :: ctx2))
exts f Here = Var Here
exts f (There x) = rename There (f x)
||| Substitutes variables in a context using a
||| function mapping variables to the terms they
||| should be substituted by
subst : ({a : _} -> Elem a ctx1 -> Term a ctx2)
-> ({a : _} -> Term a ctx1 -> Term a ctx2)
subst f (Var x) = f x
subst f (Lam x) = Lam (subst (exts f) x)
subst f (App x y) = Main.App (subst f x) (subst f y)
subst f Zero = Zero
subst f (Suc x) = Suc (subst f x)
subst f (Case c x y) = Case (subst f c) (subst f x) (subst (exts f) y)
subst f (Fix x) = Fix (subst (exts f) x)
||| Substitute the last free variable
substLast : {ctx, a, b : _}
-> Term a (b :: ctx)
-> Term b ctx
-> Term a ctx
substLast {ctx} {a} {b} t s = subst f t
where
||| Maps the last variable to the substituted term
||| and all other variables to themselves
f : {a : _} -> Elem a (b :: ctx) -> Term a ctx
f Here = s
f (There x) = Var x
data Value : Term a ctx -> Type where
VLam : Value (Lam b)
VZero : Value Zero
VSuc : Value x -> Value (Suc x)
||| Single-step reduction rules
data Reduce : Term a ctx -> Term a ctx -> Type where
-- Compatibility (ξ) rules
RCompAppLHS : Reduce t t' -> Reduce (App t x) (App t' x)
RCompAppRHS : Value v -> Reduce x x' -> Reduce (App v x) (App v x')
RCompSuc : Reduce x x' -> Reduce (Suc x) (Suc x')
RCompCase : Reduce c c' -> Reduce (Case c a b) (Case c' a b)
-- Beta (β) rules
RBetaLam : Value v -> Reduce (App (Lam b) v) (substLast b v)
RBetaZero : Reduce (Case Zero a b) a
RBetaSuc : Value v -> Reduce (Case (Suc v) a b) (substLast b v)
RBetaFix : Reduce (Fix b) (substLast b (Fix b))
||| Multi-step reduction rules (reflexive and transitive closure of small step relation)
data Normalize : Term a ctx -> Term a ctx -> Type where
NRefl : Normalize t t
NTrans : Reduce a b -> Normalize b c -> Normalize a c
Uninhabited (Reduce (Lam _) _) where
uninhabited _ impossible
Uninhabited (Reduce Zero _) where
uninhabited _ impossible
Uninhabited (Reduce (Suc _) (Var _)) where
uninhabited _ impossible
Uninhabited (Reduce (Suc _) (App _ _)) where
uninhabited _ impossible
Uninhabited (Reduce (Suc _) Zero) where
uninhabited _ impossible
Uninhabited (Reduce (Suc _) (Case _ _ _)) where
uninhabited _ impossible
Uninhabited (Reduce (Suc _) (Fix _)) where
uninhabited _ impossible
valuesDontReduce : {t' : _} -> Value t -> Not (Reduce t t')
valuesDontReduce VLam = uninhabited
valuesDontReduce VZero = uninhabited
valuesDontReduce {t' = (Suc innerTerm)} (VSuc innerVal) = \assumeItReduces =>
let innerDoesntReduce = valuesDontReduce {t' = innerTerm} innerVal in
case assumeItReduces of
(RCompSuc innerReduces) => innerDoesntReduce innerReduces
-- TODO: Is there a way to shorten this?
valuesDontReduce {t' = (Var x)} (VSuc inner) = uninhabited
valuesDontReduce {t' = (App x y)} (VSuc inner) = uninhabited
valuesDontReduce {t' = Zero} (VSuc inner) = uninhabited
valuesDontReduce {t' = (Case x y z)} (VSuc inner) = uninhabited
valuesDontReduce {t' = (Fix x)} (VSuc inner) = uninhabited
reducingTermsArentValues : Reduce t t' -> Not (Value t)
reducingTermsArentValues r = \v => (valuesDontReduce v) r
data Progress : Term a [] -> Type where
Done : Value v -> Progress v
Step : Reduce t t' -> Progress t
progress : {ty : _} -> (t : Term ty []) -> Progress t
progress (Var x) impossible
progress {ty = TLam a b} (Lam x) = Done VLam
progress (App x y) with (progress x)
progress (App x y) | (Done vx) with (progress y)
progress (App (Lam b) y) | (Done vx) | (Done vy) = Step (RBetaLam vy)
progress (App x y) | (Done vx) | (Step ry) = Step (RCompAppRHS vx ry)
progress (App x y) | (Step rx) = Step (RCompAppLHS rx)
progress {ty = TNat} Zero = Done VZero
progress {ty = TNat} (Suc x) with (progress x)
progress {ty = TNat} (Suc x) | (Done vx) = Done (VSuc vx)
progress {ty = TNat} (Suc x) | (Step rx) = Step (RCompSuc rx)
progress (Case x y z) with (progress x)
progress (Case Zero y z) | (Done VZero) = Step RBetaZero
progress (Case (Suc _) y z) | (Done (VSuc vs)) = Step (RBetaSuc vs)
progress (Case x y z) | (Step rx) = Step (RCompCase rx)
progress (Fix _) = Step RBetaFix
Fuel : Type
Fuel = Nat
data Finished : Term a ctx -> Type where
Normalized : Value v -> Finished v
OutOfFuel : Finished t
data Steps : Term a [] -> Type where
MkSteps : Normalize t t' -> Finished t' -> Steps t
eval : Fuel -> (t : Term a []) -> Steps t
eval Z t = MkSteps NRefl OutOfFuel
eval (S k) t with (progress t)
eval (S k) t | (Done vt) = MkSteps NRefl (Normalized vt)
eval (S k) t | (Step rt) {t'} with (eval k t')
eval (S k) t | (Step rt) {t'} | (MkSteps rt' fin) = MkSteps (NTrans rt rt') fin
import Data.Vect
import LambdaCalculus
test1 : Ctx {len = 2}
test1 = [TNat, TLam TNat TNat]
test2 : Elem TNat [TNat, TLam TNat TNat]
test2 = Here
test3 : Elem (TLam TNat TNat) [TNat, TLam TNat TNat]
test3 = There Here
test4 : Term TNat [TNat, TLam TNat TNat]
test4 = var 0
test5 : Term (TLam TNat TNat) [TNat, TLam TNat TNat]
test5 = var 1
test6 : Term TNat [TNat, TLam TNat TNat]
test6 = App (var 1) (var 0)
test7 : Term TNat [TNat, TLam TNat TNat]
test7 = App (var 1) (App (var 1) (var 0))
test8 : Term (TLam TNat TNat) [TLam TNat TNat]
test8 = Lam (var 1 $$ (var 1 $$ var 0))
two : Term TNat ctx
two = Suc (Suc Zero)
plus : Term (TLam TNat (TLam TNat TNat)) ctx
plus = Fix
(Lam (Lam
(Case (var 1)
(var 0)
(Suc ((var 3) $$ (var 0) $$ (var 1)))
)
))
twoPlusTwo : Term TNat ctx
twoPlusTwo = plus $$ two $$ two
mul : Term (TLam TNat (TLam TNat TNat)) ctx
mul = Fix
(Lam (Lam
(Case (var 1)
(Zero)
(plus $$ (var 1) $$ ((var 3) $$ (var 0) $$ (var 1)))
)
))
twoMulTwo : Term TNat ctx
twoMulTwo = mul $$ two $$ two
test9 : Term (TLam TNat TNat) [TLam TNat TNat]
test9 = Lam (var 1 $$ (var 1 $$ var 0))
test10 : Term (TLam TNat TNat) [TNat, TLam TNat TNat]
test10 = Lam (var 2 $$ (var 2 $$ var 0))
test11 : rename There Tests.test9 = Tests.test10
test11 = Refl
test12 : Term (TLam TNat TNat) [TLam TNat TNat]
test12 = Lam (var 1 $$ (var 1 $$ var 0))
test13 : Term (TLam TNat TNat) []
test13 = Lam (Suc (var 0))
test14 : Term (TLam TNat TNat) []
test14 = Lam ( (Lam (Suc (var 0))) $$ ((Lam (Suc (var 0))) $$ (var 0)))
test15 : substLast Tests.test12 Tests.test13 = Tests.test14
test15 = Refl
test16 : Term (TLam (TLam TNat TNat) TNat) [TNat, TLam TNat TNat]
test16 = Lam ((var 0) $$ (var 1))
test17 : Term TNat [TLam TNat TNat]
test17 = (var 0) $$ Zero
test18 : Term (TLam (TLam TNat TNat) TNat) [TLam TNat TNat]
test18 = Lam ((var 0) $$ ((var 1) $$ Zero))
test19 : substLast Tests.test16 Tests.test17 = Tests.test18
test19 = Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment