#
#
The initial goal of this work was to explore how investigations into packaging-up-data —and language extension in general— could benefit from mechanising tedious patterns, thereby reinvigorating the position of universal algebra within computing. Towards that goal, we have decided to create an editor extension that can be used, for instance, to quickly introduce universal algebra constructions for the purposes of “getting things done” in a way that does not force users of an interface to depend on features they do not care about —the so-called Interface Segregation Principle. Moreover, we have repositioned the prototype from being an auxiliary editor extension to instead being an in-language library and have presented its key insights so that it can be implemented in other dependently-typed settings besides Agda.[…]
In dependently-typed settings (DTS), it is common practice to operate on packages —by renaming them, hiding parts, adding new parts, etc.— and the frameworks presented in this thesis show that it is indeed possible to treat packages nearly as first-class citizens “after the fact” even when a language does not assign them such a status. The techniques presented show that this approach is feasible as an in-language library for DTS as well as for any highly customisable and extensible text editor.
#
#
#
#
With a bit of reflection, we can obtain
- a uniform, and practical, syntax for both records (semantics) and termtypes (syntax)
- on-the-fly unbundling; and,
- mechanically obtain data structures from theories
\pause
‘theory’ τ ‘data structure’ termtype τpointed set 𝟙 dynamic system ℕ monoid tree skeletons collections lists graphs (homogeneous) pairs actions infinite streams
record Monoid₂
(Carrier : Set)
(_⨾_ : Carrier → Carrier → Carrier) : Set where
field
Id : Carrier
lid : ∀ {x} → Id ⨾ x ≡ x
rid : ∀ {x} → x ⨾ Id ≡ x
assoc : ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)\vspace{1em}
Monoids model unityped composition: Sticking words on a page, sequencing programs, following instructions.
People work with monoids at various levels of exposure …
\pause
- “Let 𝑴 be a monoid, …” \vspace{1em}\pause
- “Given a monoid over ℕ, …” \vspace{1em}\pause
- “Consider /the/ monoid (ℕ, +), …”
- (Unique viz proof irrelevance.) \vspace{1em}\pause
- “Consider /the/ monoid (ℕ, +, 0), …”
record Monoid₀ : Set₁ where
field Carrier : Set
_⨾_ : Carrier → Carrier → Carrier
Id : Carrier
lid : ∀ {x} → Id ⨾ x ≡ x
rid : ∀ {x} → x ⨾ Id ≡ x
assoc : ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)| Use-case: The category of monoids. |
“A monoid over a given collection Carrier and operation _⨾_ is given by ensuring there is a selected point …”?
record Monoid₁
(Carrier : Set) : Set where
field -- ⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵ Change here
_⨾_ : Carrier → Carrier → Carrier
Id : Carrier
lid : ∀ {x} → Id ⨾ x ≡ x
rid : ∀ {x} → x ⨾ Id ≡ x
assoc : ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)| Use-case: Sharing the carrier type |
record Monoid₂
(Carrier : Set)
(_⨾_ : Carrier → Carrier → Carrier) : Set where
field -- ⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵ Change here
Id : Carrier
lid : ∀ {x} → Id ⨾ x ≡ x
rid : ∀ {x} → x ⨾ Id ≡ x
assoc : ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)| Use-case: The additive monoid on the ℕatural numbers |
record Monoid₃
(Carrier : Set)
(_⨾_ : Carrier → Carrier → Carrier)
(Id : Carrier) : Set where
field -- ⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵⟵ Change here
lid : ∀ {x} → Id ⨾ x ≡ x
rid : ∀ {x} → x ⨾ Id ≡ x
assoc : ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)Structures are meaninglessly parameterized from a mathematical perspective. […] That is, what is bundled cannot be later opened up as a parameter. […] This means that library designers are forced to take a conservative approach and expose as a parameter anything that any user might reasonably want exposed, because once it is bundled, it is not coming back.
\hfill —A Review of the Lean Theorem Prover, 2018-09-18
- Agda’s Standard Library,
- RATH-Agda,
- agda-categories
- Haskell’s Standard Library
\alert{Maintenance of relationships} …
\pause
Monoid₀ ≅ Σ C : Set • Monoid₁ C\pause
Monoid₁ C ≅ Σ 𝑴 : Monoid₀ • Monoid₀.Carrier 𝑴 ≡ C\pause
- Termtypes?
- Extensions?
- Exclusions?
- Pushouts: Name-relevant unions?
- The src_emacs-lisp[:exports code]{PackageFormer} Prototype: A useful experimentation tool
- The src_haskell[:exports code]{Context} Library: Unbundling in Agda
- Algebraic data types as a semantics for contexts
Prototype with an editor extension then incorporate lessons learned into a DTL library!
| Generated code displayed on hover |
PackageFormer MonoidP : Set₁ where
Carrier : Set
_⨾_ : Carrier → Carrier → Carrier
Id : Carrier
assoc : ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
leftId : ∀ {x} → Id ⨾ x ≡ x
rightId : ∀ {x} → x ⨾ Id ≡ x\pause
\pause
Tree = MonoidP termtype-with-variables "Carrier"
≅
data Tree (Var : Set) : Set where
inj : Var → Tree Var
_⨾_ : Tree Var → Tree Var → Tree Var
Id : Tree Var\pause
| _Linear_ effort in number of variations |
\pause
record : PackageFormer → PackageFormerrecord = :kind record
:alter-elements (λ es → (--map (map-qualifier (-const "field") it) es))(𝒱 union pf (renaming₁ "") (renaming₂ "")
(adjoin-retract₁ t) (adjoin-retract₂ t)
= :alter-elements (λ es →
(let* ((p (symbol-name 'pf))
(es₁ (alter-elements es renaming renaming₁ :adjoin-retract nil))
(es₂ (alter-elements ($𝑒𝑙𝑒𝑚𝑒𝑛𝑡𝑠-𝑜𝑓 p) renaming renaming₂ :adjoin-retract nil))
(es′ (-concat es₁ es₂)))
(-concat ;; return value
es′
(when adjoin-retract₁ (list (element-retract $𝑝𝑎𝑟𝑒𝑛𝑡 es :new es₁ :name adjoin-retract₁)))
(when adjoin-retract₂ (list (element-retract p ($𝑒𝑙𝑒𝑚𝑒𝑛𝑡𝑠-𝑜𝑓 p) :new es₂ :name adjoin-retract₂)))))))AdditiveMagma = Magma renaming′ "_*_ to _+_"
LeftDivisionMagma = Magma renaming′ "_*_ to _╲_"
RightDivisionMagma = Magma renaming′ "_*_ to _╱_"
LeftOperation = MultiCarrier extended-by′ "_⟫_ : U → S → S"
RightOperation = MultiCarrier extended-by′ "_⟪_ : S → U → S"
IdempotentMagma = Magma extended-by′ "*-idempotent : ∀ (x : U) → (x * x) ≡ x"
IdempotentAdditiveMagma = IdempotentMagma renaming′ "_*_ to _+_"
SelectiveMagma = Magma extended-by′ "*-selective : ∀ (x y : U) → (x * y ≡ x) ⊎ (x * y ≡ y)"
SelectiveAdditiveMagma = SelectiveMagma renaming′ "_*_ to _+_"
PointedMagma = Magma union′ PointedCarrier
Pointed𝟘Magma = PointedMagma renaming′ "e to 𝟘"
AdditivePointed1Magma = PointedMagma renaming′ "_*_ to _+_; e to 𝟙"
LeftPointAction = PointedMagma extended-by "pointactLeft : U → U; pointactLeft x = e * x"
RightPointAction = PointedMagma extended-by "pointactRight : U → U; pointactRight x = x * e"
CommutativeMagma = Magma extended-by′ "*-commutative : ∀ (x y : U) → (x * y) ≡ (y * x)"
CommutativeAdditiveMagma = CommutativeMagma renaming′ "_*_ to _+_"
PointedCommutativeMagma = PointedMagma union′ CommutativeMagma ⟴ :remark "over Magma"
AntiAbsorbent = Magma extended-by′ "*-anti-self-absorbent : ∀ (x y : U) → (x * (x * y)) ≡ y"
SteinerMagma = CommutativeMagma union′ AntiAbsorbent ⟴ :remark "over Magma"
Squag = SteinerMagma union′ IdempotentMagma ⟴ :remark "over Magma"
PointedSteinerMagma = PointedMagma union′ SteinerMagma ⟴ :remark "over Magma"
UnipotentPointedMagma = PointedMagma extended-by′ "unipotent : ∀ (x : U) → (x * x) ≡ e"
Sloop = PointedSteinerMagma union′ UnipotentPointedMagma- Waist
- Termtypes
- Pragmatic
User-defined variational: Drop definitions when lifting fields into parameters.
(𝒱 unbundling n
= "Turn the first N elements into parameters to the PackageFormer.
Any elements above the waist line have their equations dropped."
:waist n
:alter-elements (λ es →
(-let [i 0]
(--graph-map (progn (incf i) (<= i n))
(map-equations (-const nil) it)
es))))Some types can be viewed as a monoid in more than one way, e.g. both addition and multiplication on numbers. In such cases we often define newtypes and make those instances of Monoid, e.g. Sum and Product. —Hackage Data.Monoid
Sum α ≅ α {- and -} Product α ≅ α
Start with fully bundled src_haskell[:exports code]{Monoid} then expose fields as parameters on the fly.
\pause Reflection!
- Unfortunately, current mechanism cannot touch src_haskell[:exports code]{record}-s directly.
- But every record is a Σ-type…
- Instead of the nice syntactic sugar
record R (ε¹ : τ¹) ⋯ (εʷ : τʷ) : Set where field εʷ⁺¹ : τʷ⁺¹ ⋮ εʷ⁺ᵏ : τʷ⁺ᵏ
\pause
- Use a rawer form —/eek!/
R : Π ε¹ : τ¹ • ⋯ • Π εʷ : τʷ • Set R ≅ λ ε¹ : τ¹ • ⋯ • λ εʷ : τʷ • Σ εʷ⁺¹ : τʷ⁺¹ • ⋯ • Σ εʷ⁺ᵏ : τʷ⁺ᵏ • 𝟙
#
Monoid : Context ℓ₁
Monoid = do Carrier ← Set
_⨾_ ← (Carrier → Carrier → Carrier)
Id ← Carrier
leftId ← ∀ (x : Carrier) → x ⨾ Id ≡ x
rightId ← ∀ (x : Carrier) → Id ⨾ x ≡ x
assoc ← ∀ (x y z) → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
End {ℓ}- “Contexts” are exposure-indexed types
Context = λ ℓ → (waist : ℕ) → Set ℓ
- The “empty context” is the unit type
End : ∀ {ℓ} → Context ℓ End {ℓ} = λ _ → 𝟙 {ℓ}
- src_haskell[:exports code]{do}-notation!
_>>=_ : ∀ {a b} → (Γ : Context a) → (∀ {n} → Γ n → Context b) → Context (a ⊍ b) (Γ >>= f) zero = Σ γ ∶ Γ 0 • f γ 0 (Γ >>= f) (suc n) = Π γ ∶ Γ n • f γ n
Monoid : Context
Monoid = do C ← Set; _⨾_ : C → C → C; Id ← C; …\vspace{1em} \pause
Π→λ “Πʷ x • τ” = “λʷ x • τ”
\vspace{1em}\pause
C :waist w = Π→λ (C w)
Monoid : Context
Monoid = do C ← Set; _⨾_ : C → C → C; Id ← C; …\pause
Monoid :waist 0 : Set₁
Monoid :waist 0 ≡ Σ C : Set • Σ _⨾_ : C → C → C • Σ Id : C • …\pause
Monoid :waist 1 : Π C : Set • Set
Monoid :waist 1 = λ C : Set • Σ _⨾_ : C → C → C • Σ Id : C • …\pause
Monoid :waist 2 : Π C : Set • Π _⨾_ : C → C → C • Set
Monoid :waist 2 = λ C : Set • λ _⨾_ : C → C → C • Σ Id : C • …ℕ₊ : (Monoid ℓ₀ :waist 1) ℕ
ℕ₊ = ⟨ _+_ -- _⨾_
, 0 -- Id
, +-identityˡ
, +-identityʳ
, +-assoc
⟩‘Unbundle’ module fields as if they were parameters ‘on the fly’
\pause \vspace{-1.2em}
\pause
𝒩⁰ : DynamicSystem :waist 0
𝒩⁰ = ⟨ ℕ , 0 , suc ⟩
𝒩¹ : (DynamicSystem :waist 1) ℕ
𝒩¹ = ⟨ 0 , suc ⟩
𝒩² : (DynamicSystem :waist 2) ℕ 0
𝒩² = ⟨ suc ⟩
𝒩³ : (DynamicSystem :waist 3) ℕ 0 suc
𝒩³ = ⟨⟩Without redefining src_haskell[:exports code]{DynamicSystem}, we are able to fix some of its fields by making them into parameters!
src_haskell[:exports code]{Monoid}
⟿
do C ← Set; _⨾_ : C → C → C; Id : C; …⟿
λ C : Set • Σ _⨾_ : C → C → C • Σ Id : C • …⟿
λ C : Set • Σ _⨾_ : C → C → C • Σ Id : C • 𝟙⟿
λ C : Set • C × C ⊍ C ⊍ 𝟙⟿
μ C : Set • C × C ⊍ C ⊍ 𝟙\pause
Monoid : ∀ ℓ → Context (ℓsuc ℓ)
Monoid ℓ = do Carrier ← Set ℓ
_⨾_ ← (Carrier → Carrier → Carrier)
Id ← Carrier
leftId ← ∀ {x : Carrier} → Id ⨾ x ≡ x
rightId ← ∀ {x : Carrier} → x ⨾ Id ≡ x
assoc ← ∀ {x y z} → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
End {ℓ}𝕄 : Set
𝕄 = termtype (Monoid ℓ₀ :waist 1)that-is : 𝕄
≡ Fix (λ X →
-- _⊕_, branch
X × X × 𝟙
-- Id, nil leaf
⊎ 𝟙
-- invariant leftId
⊎ 𝟘
-- invariant rightId
⊎ 𝟘
-- invariant assoc
⊎ 𝟘
-- the “End {ℓ}”
⊎ 𝟘)
that-is = refl-- : 𝕄
pattern emptyM
= μ (inj₂ (inj₁ tt))
-- : 𝕄 → 𝕄 → 𝕄
pattern branchM l r
= μ (inj₁ (l , r , tt))-- absurd 𝟘-values
pattern absurdM a
= μ (inj₂ (inj₂ (inj₂ (inj₂ a))))data TreeSkeleton : Set where
empty : TreeSkeleton
branch : TreeSkeleton → TreeSkeleton → TreeSkeleton- “doing nothing”
to : 𝕄 → TreeSkeleton to emptyM = empty to (branchM l r) = branch (to l) (to r) to (absurdM (inj₁ ())) to (absurdM (inj₂ ()))
- “doing nothing”
from : TreeSkeleton → 𝕄 from empty = emptyM from (branch l r) = branchM (from l) (from r)
Bring \alert{algebraic data types} under the umbrella of grouping mechanisms:
\pause
\vspace{-0.5em}
\pause
data 𝔻 : Set where
startD : 𝔻
nextD : 𝔻 → 𝔻\pause \vspace{-1.3em}
\vspace{-2em}
𝔻 = termtype (DynamicSystem :waist 1)
-- Pattern synonyms for more compact presentation
pattern startD = μ (inj₁ tt) -- : 𝔻
pattern nextD e = μ (inj₂ (inj₁ e)) -- : 𝔻 → 𝔻
trivial : 𝔻 ≅ ℕ| ‘theory’ τ | ‘data structure’ termtype τ |
|---|---|
| pointed set | 𝟙 |
| dynamic system | ℕ |
| monoid | tree skeletons |
| collections | lists |
| graphs | (homogeneous) pairs |
| actions | infinite streams |
Many more theories τ to explore and see what data structures arise!
\pause \vspace{0.5em}
- Context: “name-type pairs”
do S ← Set; s ← S; n ← (S → S); End
- Record Type: “bundled-up data”
Σ S ∶ Set • Σ s ∶ S • Σ n ∶ S → S • 𝟙
\vspace{0.5em}
- Function Type: “a type of functions”
Π S • Σ s ∶ S • Σ n ∶ S → S • 𝟙
\vspace{0.5em}
- Type constructor: “a function on types”
λ S • Σ s ∶ S • Σ n ∶ S → S • 𝟙
\vspace{0.5em}
- Algebraic datatype: “a descriptive syntax”
data 𝔻 : Set where s : 𝔻; n : 𝔻 → 𝔻
- Identify the \alert{module design patterns} used by DTL practitioners
- Demonstrate that there is an expressive yet minimal set of primitives which allow common module constructions to be defined
- Bring \alert{algebraic data types} under the umbrella of grouping mechanisms
- The ability to ‘unbundle’ module fields as if they were parameters ‘on the fly’
- Show that common data-structures are \alert{mechanically the (free) termtypes} of common modules
- Demonstrate that there is a \alert{practical implementation} of such a framework
- Finally, the resulting framework is mostly \alert{type-theory agnostic}.