? for Help ⟫
With a bit of reflection, we can obtain
mechanically obtain data structures from theories
| ‘theory’ τ | ‘data structure’ termtype τ |
|---|---|
| pointed set | 𝟙 |
| dynamic system | ℕ |
| monoid | tree skeletons |
| collections | lists |
| graphs | (homogeneous) pairs |
| actions | infinite streams |
Carrier,_⨾_Id.record MonoidOn (Carrier : Set) : Set
where
field
_⨾_ : Carrier → Carrier → Carrier
Id : Carrier
leftId : ∀ x → Id ⨾ x ≡ x
rightId : ∀ x → x ⨾ Id ≡ x
assoc : ∀ x y z → (x ⨾ y) ⨾ z
≡ x ⨾ (y ⨾ z)
open MonoidOn {{...}}
instance
ℕ₊ : MonoidOn ℕ
ℕ₊ = record { _⨾_ = _+_
; Id = 0
; leftId = +-identityˡ
; rightId = +-identityʳ
; assoc = +-assoc }
ex : ∀ (m n : ℕ) → m ⨾ n ≡ n ⨾ m
ex = +-comm
⇨ __⨾__ is determined to be _+_by instance search ⇦
likewise : ∀ (m : ℕ) → m ⨾ Id ≡ m
likewise = rightId
instance
ℕₓ : MonoidOn ℕ
ℕₓ = record { _⨾_ = _*_
; Id = 1
; leftId = *-identityˡ
; rightId = *-identityʳ
; assoc = *-assoc }
whoops : ∀ {m : ℕ} → m ⨾ Id ≡ m
whoops = {!!}
⇨ ℕ₊ and ℕₓ are both candidates! No unique solution! ⇦
Make two isomorphic copies of numbers …
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 α ≅ α
For Num α they have different monoid instances.
Start with fully bundled Monoid
then expose fields as parameters on the fly.
Reflection!
record-s directly.Instead of the nice syntactic sugar
record R (ε¹ : τ¹) ⋯ (εʷ : τʷ) : Set
where
field
εʷ⁺¹ : τʷ⁺¹
⋮
εʷ⁺ᵏ : τʷ⁺ᵏ
Use a more raw form ---eek!
R ≅ Π ε¹ : τ¹ • ⋯ • Π εʷ : τʷ
• Σ εʷ⁺¹ : τʷ⁺¹ • ⋯ • Σ εʷ⁺ᵏ : τʷ⁺ᵏ
• 𝟙
R ≅ Π ε¹ : τ¹ • ⋯ • Π εʷ : τʷ
• Σ εʷ⁺¹ : τʷ⁺¹ • ⋯ • Σ εʷ⁺ᵏ : τʷ⁺ᵏ
• 𝟙
⇨ “R is a ΠʷΣ type” —a (partitioned) context
⇨ It has parameters ε⁰, …, εʷ and fields εʷ⁺¹, …, εʷ⁺ᵏ
⇨ \(w\) is the “waist”
E.g., MonoidOn is a Π¹Σ type
If we encode a record as a ΠʷΣ type, what if we want to instantiate, fix, a field —instead of a parameter?
We thus need a way to lift parameters to fields!
( Teaser: Π→λ ! )
Instead of Set, use (waist : ℕ) → Set
“Contexts” are exposure-indexed types
Context = λ ℓ → ℕ → Set ℓ
The “empty context” is the unit type
End : ∀ {ℓ} → Context ℓ
End {ℓ} = ‵ 𝟙 {ℓ}
do-notation!
_>>=_ : ∀ {a b}
→ (Γ : Context a)
→ (∀ {n} → Γ n → Context b)
→ Context (a ⊍ b)
(Γ >>= f) zero = Σ γ ∶ Γ 0 • f γ 0
(Γ >>= f) (suc n) = Π γ ∶ Γ n • f γ n
>>=, permitting Σ, Π, 𝒲, let, … !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 {ℓ}
ℕ₊′ : (Monoid ℓ₀ :waist 1) ℕ
ℕ₊′ = ⟨ _+_ -- _⨾_
, 0 -- Id
, +-identityˡ
, +-identityʳ
, +-assoc
⟩
Notice…
(Monoid ℓ₀ :waist 1) ℕ ≅ MonoidOn ℕ
Π→λ —or _:waist_recordContext
If C : Context ℓ₀ then C w : Πʷ ⋯ • Set, but we want to apply C w to w-many parameters?
(Πʷ x • τ) is w-many Π's binding variables to be used in
type τ.
So we need a combinator…
Π→λ “Πʷ x • τ” = “λʷ x • τ”
with an infix form for contexts in particular …
C :waist w = Π→λ (C w)
Monoid : Context
Monoid = do C ← Set; _⨾_ : C → C → C; Id ← C; …
With no parameters, we have a Π⁰Σ-type
Monoid :waist 0 : Set₁
Monoid :waist 0 ≡ Σ C : Set • Σ _⨾_ : C → C → C • Σ Id : C • …
With one parameter, we regain MonoidOn
Monoid :waist 1 : Π C : Set • Set
Monoid :waist 1 = λ C : Set • Σ _⨾_ : C → C → C • Σ Id : C • …
With two parameters, we have a ‘solution’ to the additive-or-multiplicative-monoid-problem!
Monoid :waist 2 : Π C : Set) • Π _⨾_ : C → C → C • Set
Monoid :waist 2 = λ C : Set • λ _⨾_ : C → C → C • Σ Id : C • …
Monoid : Context -- i.e., (w : ℕ) → Set
Monoid :waist 𝓌 : Πʷ ⋯ • Set
Monoid :waist 𝓌 = λʷ “parameters” • “fields”
-- Π a : A • B a ↦ λ a : A • B a
Π→λ-helper : Term → Term
Π→λ-helper (pi a (abs x b))
= lam visible (abs x (Π→λ-helper b))
Π→λ-helper x
= x
Term denotes untyped λ-terms,
so let's keep track of the types when we convert Πs to λs.
Π→λ-type : Term → Term
Π→λ-type (pi a (abs x b))
= pi a (abs x (Π→λ-type b))
Π→λ-type x
= unknown
macro
Π→λ : Term → Term → TC Unit.⊤
Π→λ τ goal
= normalise τ
>>=ₜₑᵣₘ λ τ′ → checkType goal (Π→λ-type τ′)
>>=ₜₑᵣₘ λ _ → unify goal (Π→λ-helper τ′)
On-the-fly unbundling can be implemented as an in-language library in a dependently-typed language with sufficient reflection capabilities (•̀ᴗ•́)و
Monoiddo 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 ⊍ 𝟙termtype : UnaryFunctor → Type termtype τ = Fix (Σ→⊎ (sources τ))
macro
termtype : Term → Term → TC Unit.⊤
termtype tm goal =
normalise tm
>>=ₜₑᵣₘ λ tm′ → unify goal (def (quote Fix) ((vArg (Σ→⊎₀ (sourcesₜₑᵣₘ tm′))) ∷ []))
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))))
termtype Monoid ≅ TreeSkeleton 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)
DynamicSystem : Context ℓ₁
DynamicSystem = do State ← Set
start ← State
next ← (State → State)
End {ℓ₀}
𝔻 = termtype (DynamicSystem :waist 1)
Pattern synonyms for more compact presentation
-- : 𝔻
pattern startD
= μ (inj₁ tt)
-- : 𝔻 → 𝔻
pattern nextD e = μ (inj₂ (inj₁ e))
termtype 𝔻 ≅ ℕ to : 𝔻 → ℕ
to startD = 0
to (nextD x) = suc (to x)
from : ℕ → 𝔻
from zero = startD
from (suc n) = nextD (from n)
PSet : Context (ℓsuc ℓ₀)
PSet = do Carrier ← Set ℓ₀
point ← Carrier
End {ℓ₀}
ℙ𝕊𝕖𝕥 : Set
ℙ𝕊𝕖𝕥 = termtype (PSet :waist 1)
to : ℙ𝕊𝕖𝕥 → 𝟙 {ℓ₀}
to emptyM = tt
from : 𝟙 {ℓ₀} → ℙ𝕊𝕖𝕥
from _ = μ (inj₁ tt)
Graph : Context (ℓsuc ℓ₀)
Graph = do Node ← Set
Edge ← Set
adjacency ← (Node → Node → Edge)
End {ℓ₀}
𝔾𝕣𝕒𝕡𝕙 : Set → Set
𝔾𝕣𝕒𝕡𝕙 X = termtype ((Graph :waist 2) X)
pattern _⇌_ x y = μ (inj₁ (x , y , tt))
view : ∀ {X} → 𝔾𝕣𝕒𝕡𝕙 X → X × X
view (x ⇌ y) = x , y
Action : Context ℓ₁
Action = do Value ← Set
Program ← Set
run ← (Program → Value → Value)
End {ℓ₀}
𝔸𝕔𝕥𝕚𝕠𝕟 : Set → Set
𝔸𝕔𝕥𝕚𝕠𝕟 X = termtype ((Action :waist 2) X)
-- : X → 𝔸𝕔𝕥𝕚𝕠𝕟 X → 𝔸𝕔𝕥𝕚𝕠𝕟 X
pattern _∷_ head tail
= μ (inj₁ (tail , head , tt))
record Stream (X : Set) : Set where
coinductive
field
hd : X
tl : Stream X
open Stream
view : ∀ {I} → 𝔸𝕔𝕥𝕚𝕠𝕟 I → Stream I
hd (view (h ∷ t)) = h
tl (view (h ∷ t)) = view t
Collection : ∀ ℓ → Context (ℓsuc ℓ)
Collection ℓ = do Elem ← Set ℓ
Container ← Set ℓ
insert ← (Elem → Container → Container)
∅ ← Container
End {ℓ}
ℂ : Set → Set
ℂ Elem = termtype ((Collection ℓ₀ :waist 2) Elem)
-- : X → ℂ X → ℂ X
pattern _::_ x xs
= μ (inj₁ (x , xs , tt))
-- : ℂ X
pattern ∅
= μ (inj₂ (inj₁ tt))
| ‘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!
Thanks for listening in!
The Context Library:
https://alhassy.github.io/next-700-module-systems/diy/Context.agda
Examples to play with:
https://alhassy.github.io/next-700-module-systems/diy/Examples.agda
These slides:
https://alhassy.github.io/next-700-module-systems/diy/agda-implementors-meeting-2020