From df84bb5c89773d380ec72b81a46d4776cff38534 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 5 Aug 2024 16:49:25 +0100 Subject: Define nominal, painless binding. --- inky.ipkg | 2 +- src/Inky.idr | 1 - src/Inky/Binding.idr | 220 +++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 221 insertions(+), 2 deletions(-) delete mode 100644 src/Inky.idr create mode 100644 src/Inky/Binding.idr diff --git a/inky.ipkg b/inky.ipkg index 313b667..5225ed9 100644 --- a/inky.ipkg +++ b/inky.ipkg @@ -5,4 +5,4 @@ sourcedir = "src" options = "--total" modules - = Inky + = Inky.Binding diff --git a/src/Inky.idr b/src/Inky.idr deleted file mode 100644 index c501caf..0000000 --- a/src/Inky.idr +++ /dev/null @@ -1 +0,0 @@ -module Inky diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr new file mode 100644 index 0000000..7562f27 --- /dev/null +++ b/src/Inky/Binding.idr @@ -0,0 +1,220 @@ +module Inky.Binding + +import Control.Relation +import Control.Order +import Data.DPair +import Data.List +import Data.Nat +import Data.So +import Decidable.Equality + +-- Types ----------------------------------------------------------------------- + +data WorldRepr : Nat -> List Bool -> Type where + Done : 0 `WorldRepr` [] + True : w `WorldRepr` bs -> 1 + 2 * w `WorldRepr` True :: bs + False : w `WorldRepr` bs -> 2 * w `WorldRepr` False :: bs + +export +World : Type +World = List Bool + +export +Binder : Type +Binder = Nat + +Member : Binder -> World -> Type +n `Member` [] = Void +Z `Member` b :: bs = So b +S n `Member` b :: bs = n `Member` bs + +export +(:<) : World -> Binder -> World +[] :< Z = True :: [] +[] :< (S n) = False :: [] :< n +(_ :: bs) :< Z = True :: bs +(b :: bs) :< (S n) = b :: bs :< n + +snocSem : (bs : World) -> (k, n : Binder) -> n `Member` bs :< k <=> Either (n = k) (n `Member` bs) +snocSem [] Z Z = MkEquivalence (const $ Left Refl) (const Oh) +snocSem [] Z (S n) = MkEquivalence absurd absurd +snocSem [] (S k) 0 = MkEquivalence absurd absurd +snocSem [] (S k) (S n) = + let equiv = snocSem [] k n in + MkEquivalence + (mapFst (\prf => cong S prf) . equiv.leftToRight) + (equiv.rightToLeft . mapFst injective) +snocSem (b :: bs) Z Z = + MkEquivalence (const $ Left Refl) (const Oh) +snocSem (b :: bs) Z (S n) = MkEquivalence Right (\case (Right x) => x) +snocSem (b :: bs) (S k) Z = MkEquivalence Right (\case (Right x) => x) +snocSem (b :: bs) (S k) (S n) = + let equiv = snocSem bs k n in + MkEquivalence + (mapFst (\prf => cong S prf) . equiv.leftToRight) + (equiv.rightToLeft . mapFst injective) + +export +Name : World -> Type +Name w = Subset Binder (`Member` w) + +-- Countable binders ----------------------------------------------------------- + +export +BZ : Binder +BZ = Z + +export +BS : Binder -> Binder +BS = S + +-- Binders to names ------------------------------------------------------------ + +export +name : forall w. (b : Binder) -> Name (w :< b) +name b = Element b ((snocSem w b b).rightToLeft (Left Refl)) + +export +binder : Name w -> Binder +binder = fst + +export +binderName : binder {w = w :< b} (name {w} b) = b +binderName = Refl + +-- Empty world ----------------------------------------------------------------- + +export +Empty : World +Empty = [] + +export +Uninhabited (Name Empty) where + uninhabited n = void n.snd + +-- Names are comparable and stripable ------------------------------------------ + +export +Eq (Name w) where + n == k = n == k + +soEq : (n : Nat) -> So (n == n) +soEq Z = Oh +soEq (S k) = soEq k + +export +strip : {b : Binder} -> Name (w :< b) -> Maybe (Name w) +strip (Element n member) = + case decSo (b == n) of + Yes _ => Nothing + No neq => + Just + (Element n + (either + (\eq => void $ neq $ rewrite eq in soEq b) + id $ + (snocSem w b n).leftToRight member)) + +-- Freshness ------------------------------------------------------------------- + +export +FreshIn : Binder -> World -> Type +FreshIn k bs = So (k `gte` length bs) + +export +freshInEmpty : b `FreshIn` Empty +freshInEmpty = Oh + +snocLength : (w : World) -> (k : Binder) -> So (k `gte` length w) -> So (S k `gte` length (w :< k)) +snocLength [] 0 prf = Oh +snocLength [] (S k) prf = snocLength [] k prf +snocLength (b :: bs) (S k) prf = snocLength bs k prf + +%inline +soRecomputable : (0 s : So b) -> So b +soRecomputable Oh = Oh + +export +sucFresh : b `FreshIn` w -> S b `FreshIn` w :< b +sucFresh prf = soRecomputable (snocLength w b prf) + +-- World inclusion ------------------------------------------------------------- + +export +(<=) : World -> World -> Type +w <= v = {n : Binder} -> n `Member` w -> n `Member` v + +export +coerce : (0 prf : w <= v) -> Name w -> Name v +coerce lte n = Element n.fst (lte n.snd) + +export +Reflexive World (<=) where + reflexive = id + +export +Transitive World (<=) where + transitive f g = g . f + +export +Preorder World (<=) where + +export +emptyMin : Empty <= w +emptyMin n impossible + +export +snocMono : {w, v : World} -> (b : Binder) -> w <= v -> w :< b <= v :< b +snocMono b lte {n} = (snocSem v b n).rightToLeft . mapSnd lte . (snocSem w b n).leftToRight + +export +freshLte : {b : Binder} -> {w : World} -> (0 fresh : b `FreshIn` w) -> w <= w :< b +freshLte _ {n} = (snocSem w b n).rightToLeft . Right + +-- DeBruijn Worlds ------------------------------------------------------------- + +export +WS : World -> World +WS = (False ::) + +public export +shift : World -> World +shift w = WS w :< BZ + +export +sucMono : w <= v -> WS w <= WS v +sucMono lte {n = (S n)} member = lte member + +public export +shiftMono : {w, v : World} -> w <= v -> shift w <= shift v +shiftMono lte = snocMono BZ (sucMono lte) + +export +sucLteShift : WS w <= shift w +sucLteShift {n = (S n)} member = member + +export +sucInjective : WS w <= WS v -> w <= v +sucInjective lte {n} member = lte {n = (S n)} member + +export +shiftInjective : shift w <= shift v -> w <= v +shiftInjective lte {n} member = lte {n = (S n)} member + +export +sucLteShiftInjective : WS w <= shift v -> w <= v +sucLteShiftInjective lte {n} member = lte {n = (S n)} member + +export +sucEmpty : WS Empty <= Empty +sucEmpty {n = (S n)} member impossible + +-- Suc and snoc ---------------------------------------------------------------- + +export +sucDistributesOverSnocLte : WS (w :< b) <= WS w :< BS b +sucDistributesOverSnocLte {n = (S n)} member = member + +export +sucDistributesOverSnocGte : WS w :< BS b <= WS (w :< b) +sucDistributesOverSnocGte {n = (S n)} member = member -- cgit v1.2.3