https://plfa.github.io/DeBruijn in Idris

LambdaCalculus.idr

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

Tests.idr

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