The first five collapse into one uniform language within the dependently-typed language Agda.
So why not the module language?
Definition: A typed module, context, telescope, package former, record, typeclass is a sequence of tuples:
Name : Type := Optional_Definition |
Without types, we obtain essentially JSON Objects.
Purpose: Group related concepts together as single semantic units.
Packages | |
≈? | modules |
≈? | theories |
≈? | contexts |
≈? | typeclasses |
≈? | ⋯ |
≈? | dependent records |
Differences ≈?⇒ Uses & Implementations
Different ways one would encode monoid definitions in their code for different purposes
⇒ | Monoids with a dynamically known carrier |
⇒ | Monoids with a statically known carrier |
⇒ | Monoids as raw tuples |
⇒ | Monoids as telescopes |
⇄ | Derived operations |
record Monoid-Record : Set₁ where infixl 5 _⨾_ field -- Interface Carrier : Set Id : Carrier _⨾_ : Carrier → Carrier → Carrier -- Constraints lid : ∀{x} → (Id ⨾ x) ≡ x rid : ∀{x} → (x ⨾ Id) ≡ x assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z) -- derived result pop-Idᵣ : ∀ x y → x ⨾ Id ⨾ y ≡ x ⨾ y pop-Idᵣ x y = cong (_⨾ y) rid ⇨ Carrier sets, functions, and axioms all are record fields. |
record HasMonoid (Carrier : Set) : Set₁ where infixl 5 _⨾_ field Id : Carrier _⨾_ : Carrier → Carrier → Carrier lid : ∀{x} → (Id ⨾ x) ≡ x rid : ∀{x} → (x ⨾ Id) ≡ x assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z) pop-Id-tc : ∀ x y → x ⨾ Id ⨾ y ≡ x ⨾ y pop-Id-tc x y = cong (_⨾ y) rid {- We make this record type available to instance search, “typeclass”. -} open HasMonoid {{...}} using (pop-Id-tc) ⇨ Only functions and axioms are record fields —the carrier set is a parameter. |
⇨ Monoids as Agda Records
record Monoid-Record : Set₁ where field -- Interface Carrier : Set Id : Carrier _⨾_ : Carrier → Carrier → Carrier -- Constraints lid : ∀{x} → (Id ⨾ x) ≡ x rid : ∀{x} → (x ⨾ Id) ≡ x assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z) -- derived result pop-Idᵣ : ∀ x y → x ⨾ Id ⨾ y ≡ x ⨾ y pop-Idᵣ x y = cong (_⨾ y) rid {- Monoid-Record ≅ Σ C ∶ Set • HasMonoid C -}
⇨ Monoids as Typeclasses
record HasMonoid (Carrier : Set) : Set₁ where field -- Interface {- Notice that “Carrier” is a parameter. -} Id : Carrier _⨾_ : Carrier → Carrier → Carrier -- Constraints lid : ∀{x} → (Id ⨾ x) ≡ x rid : ∀{x} → (x ⨾ Id) ≡ x assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z) -- derived result pop-Id-tc : ∀ x y → x ⨾ Id ⨾ y ≡ x ⨾ y pop-Id-tc x y = cong (_⨾ y) rid {- HasMonoid ≅ λ C → Σ M ∶ Monoid-Record • M.Carrier ≡ C -}
Monoid-Σ : Set₁ Monoid-Σ = Σ Carrier ∶ Set • Σ Id ∶ Carrier • Σ _⨾_ ∶ (Carrier → Carrier → Carrier) • Σ lid ∶ (∀{x} → Id ⨾ x ≡ x) • Σ rid ∶ (∀{x} → x ⨾ Id ≡ x) • (∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) pop-Id-Σ : ∀{{M : Monoid-Σ}} (let Id = proj₁ (proj₂ M)) (let _⨾_ = proj₁ (proj₂ (proj₂ M))) → ∀ (x y : proj₁ M) → (x ⨾ Id) ⨾ y ≡ x ⨾ y pop-Id-Σ {{M}} x y = cong (_⨾ y) (rid {x}) where _⨾_ = proj₁ (proj₂ (proj₂ M)) rid = proj₁ (proj₂ (proj₂ (proj₂ (proj₂ M))))
⇨ The navigational feature of record fields is replaced by projections —i.e., it's just a different encoding.
{- Boilerplate -} Carrier′ : Monoid-Σ → Set Carrier′ = proj₁
ℕ-record : Monoid-Record ℕ-record = record { Carrier = ℕ; Id = 0; _⨾_ = _+_; ⋯ } instance ℕ-tc : HasMonoid ℕ ℕ-tc = record { Id = 0; _⨾_ = _+_; ⋯ } ℕ-Σ : Monoid-Σ ℕ-Σ = ℕ , 0 , _+_ , ⋯ ℕ-pop-0ᵣ : ∀ (x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-0ᵣ = pop-Idᵣ ℕ-record ℕ-pop-0-tc : ∀ (x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-0-tc = pop-Id-tc ℕ-pop-0-Σ : ∀ (x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-0-Σ = pop-Id-Σ
⇨ One would expect these pop-0
programs
to be instances of one polymorphic function.
⇨ Instead, we currently have three programs that are
instances of three different polymorphic functions.
module Monoid-Telescope-User (Carrier : Set ) (Id : Carrier ) (_⨾_ : Carrier → Carrier → Carrier ) (lid : ∀ {x} → Id ⨾ x ≡ x ) (rid : ∀ {x} → x ⨾ Id ≡ x ) (assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) where pop-Id-tel : ∀(x y : Carrier) → (x ⨾ Id) ⨾ y ≡ x ⨾ y pop-Id-tel x y = cong (_⨾ y) (rid {x}) open Monoid-Telescope-User ℕ 0 _+_ … ℕ-pop-tel : ∀(x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-tel = pop-Id-tel
◈ | Carrier sets, functions, and axioms all are parameters. |
◈ | This parameter listing constitutes a ‘telescope’. |
⇨ | Different notions are thus interdefinable |
⇨ | Use-cases distinguish packages |
⇨ | Distinctions ⇒ duplication of efforts |
Generalise! Use a ‘package former’, rather than a particular variation.
-- Contexts Γ ::= · -- empty context | x : T [:= T], Γ -- context with declaration, optional definition | includes X, Γ -- theory inclusion -- Terms T ::= x | T₁ T₂ | λ x : T' • T -- variables, application, lambdas | Π x : T' • T -- dependent product | [Γ] | ⟨Γ⟩ | T.x -- record “[type]” and “⟨element⟩” formers, projections | Mod X -- contravariant “theory to record” internalisation -- Theory, external grouping, level Θ ::= . -- empty theory | X := Γ, Θ -- a theory can contain named contexts | (X : (X₁ → X₂)) := Γ -- a theory can be a first-class theory morphism
A knowledge-capture mechanism ─not a programming environment.
😧 :: Coders have to copy-paste-modify packaging structures to obtain different perspectives.
😄 :: A package should be written once.
|
Which aspects of a structure should be exposed? record Semigroup0 : Set₁ where … record Semigroup1 (Carrier : Set) : Set₁ where … record Semigroup2 (Carrier : Set) (_⨾_ : Carrier → Carrier → Carrier) : Set where … record Semigroup3 (Carrier : Set) (_⨾_ : Carrier → Carrier → Carrier) (assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) : Set where -- no fields |
We want to code along Semigroup1 and use for {- Recall -} record Semigroup0 : Set₁ where … record Semigroup1 (Carrier : Set) : Set₁ where … {- Write elegantly along Semigroup1 -} translate1 : ∀{A B} → (f : A → B) → Bijection f → Semigroup1 A → Semigroup1 B {- Be able to use the previous for Semigroup0 -} translate0 : ∀{B : Set} (AS : Semigroup0) (f : Semigroup0.Carrier AS → B) → Bijection f → Semigroup0 |
Can we please just declare a Monad
without having to declare
redundant Applicative
and Functor
instances.
{- (0) -} instance Monad M where … -- (0) needs (1), which needs (2) {- (1) -} instance Applicative M where … -- (1, 2) redundant if (0) is given {- (2) -} instance Functor M where …
Accessing deeply nested fields; e.g., Monoid.Semigroup.Magma.Carrier M
.
There are none!
⇨ | Agda has a tremendously weak reflection mechanism |
⇨ | Package formers need to be introduced into the back-end |
⇨ | Unclear semantics of package formers |
⇨ | Unclear whether semantics don't break other language features |
Copy-paste-modify is almost always a mistake!
— Wolfram Kahl (•̀ᴗ•́)و
No more preprocessing for the end-user!
Questions?