module DeducteamTalk where
open import Level renaming (zero to zeroL ; suc to sucL)
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Product
open import Data.Sum
open import Data.List
open import Data.Fin hiding (lift ; _+_)
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Enum
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- * Part I: Inductive types
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- ** Signature functors
-- Signature functors are implemented with a Martin-Löf *universe*,
-- consisting of a code and its interpretation. The code gives an
-- intensional characterisation of the functors of interest, while the
-- interpretation builds extensional objects, ie. strictly-positive
-- endofunctors over Set.
-- Code:
data Desc {ℓ} : Set (sucL ℓ) where
`K : (S : Set ℓ) → Desc
`X : Desc
_`×_ _`+_ : (D₁ D₂ : Desc) → Desc
`σ : (E : Enum)(D : EnumT E → Desc) → Desc
`Σ `Π : (S : Set ℓ)(D : S → Desc) → Desc
-- Interpretation:
⟦_⟧ : ∀{ℓ} → Desc {ℓ} → Set ℓ → Set ℓ
⟦ `K S ⟧ X = S
⟦ `X ⟧ X = X
⟦ D₁ `× D₂ ⟧ X = ⟦ D₁ ⟧ X × ⟦ D₂ ⟧ X
⟦ D₁ `+ D₂ ⟧ X = ⟦ D₁ ⟧ X ⊎ ⟦ D₂ ⟧ X
⟦ `σ E D ⟧ X = σ E (λ e → ⟦ D e ⟧ X)
⟦ `Σ S D ⟧ X = Σ[ s ∈ S ] ⟦ D s ⟧ X
⟦ `Π S D ⟧ X = (s : S) → ⟦ D s ⟧ X
infixr 30 _`×_
infixr 20 _`+_
-- *** Example: Nat
pattern `ze` = zero
pattern `su` = suc zero
NatD : Desc {zeroL}
NatD = `σ 2 (λ { `ze` → `K ⊤
; `su` → `X
; (suc (suc ())) } )
-- *** Example: List
pattern `nil` = zero
pattern `cons` = suc zero
ListD : Set → Desc {zeroL}
ListD A = `σ 2 (λ { `nil` → `K ⊤
; `cons` → `Σ A (λ _ → `X)
; (suc (suc ())) })
-- *** Example: Tree
pattern `leaf` = zero
pattern `node` = suc zero
TreeD : Set → Set → Desc {zeroL}
TreeD A B = `σ 2 λ { `leaf` → `K A
; `node` → `K B `× `X `× `X
; (suc (suc ())) }
-- ** Fixpoint
-- We obtain the least fixpoint by simply tying the knot:
data μ {ℓ}(D : Desc {ℓ}) : Set ℓ where
⟨_⟩ : (xs : ⟦ D ⟧ (μ D)) → μ D
-- From which we can derive a (generic) catamorphism. We write a
-- mutual definition of 'fold' and 'mapFold' because Agda
-- termination's checker would accept the naive definition otherwise.
module Fold {ℓ}(D : Desc {ℓ}){X : Set ℓ}
(α : ⟦ D ⟧ X → X) where
mutual
foldD : μ D → X
foldD ⟨ xs ⟩ = α (mapFoldD D xs)
mapFoldD : (D' : Desc) → ⟦ D' ⟧ (μ D) → ⟦ D' ⟧ X
mapFoldD (`K S) s = s
mapFoldD `X xs = foldD xs
mapFoldD (D₁ `× D₂) (xs₁ , xs₂) = mapFoldD D₁ xs₁ , mapFoldD D₂ xs₂
mapFoldD (D₁ `+ D₂) (inj₁ xs₁) = inj₁ (mapFoldD D₁ xs₁)
mapFoldD (D₁ `+ D₂) (inj₂ xs₂) = inj₂ (mapFoldD D₂ xs₂)
mapFoldD (`σ E D') (k , xs) = k , mapFoldD (D' k) xs
mapFoldD (`Σ S D') (s , xs) = s , mapFoldD (D' s) xs
mapFoldD (`Π S D') xs s = mapFoldD (D' s) (xs s)
open Fold
-- In Type Theory, the catamorphism is of little interest: we want to
-- obtain an induction principle. The construction, for a similar
-- universe, can be found in
-- [http://gallium.inria.fr/~pdagand/stuffs/thesis-2011-phd/model/html/Chapter5.IDesc.Induction.html].
-- Here, we simply postulate it:
postulate
□ : ∀{ℓ k}{X : Set ℓ} → (D : Desc {ℓ}) →
(P : X → Set k) → ⟦ D ⟧ X → Set k
induction : ∀{ℓ}{D : Desc {ℓ}}{P : μ D → Set} →
(α : ∀ xs → □ D P xs → P ⟨ xs ⟩) →
(xs : μ D) → P xs
-- *** Example: Nat
Nat' : Set
Nat' = μ NatD
ze' : Nat'
ze' = ⟨ `ze` , tt ⟩
su' : Nat' → Nat'
su' n = ⟨ `su` , n ⟩
-- Exercise:
-- * using 'fold', define addition of natural numbers
-- * prove that 2 + 2 = 4
-- *** Example: List
List' : Set → Set
List' A = μ (ListD A)
nil' : ∀{A} → List' A
nil' = ⟨ `nil` , tt ⟩
cons' : ∀{A} → A → List' A → List' A
cons' a xs = ⟨ `cons` , a , xs ⟩
-- *** Example: Tree
Tree' : Set → Set → Set
Tree' A B = μ (TreeD A B)
leaf' : ∀{A B} → A → Tree' A B
leaf' a = ⟨ `leaf` , a ⟩
node' : ∀{A B} → B → Tree' A B → Tree' A B → Tree' A B
node' b l r = ⟨ `node` , b , l , r ⟩
-- ** Bootstrap
-- This is an inductive type:
-- data Desc : Set₁ where
-- `K : (S : Set) → Desc
-- `X : Desc
-- _`×_ _`+_ : (D₁ D₂ : Desc) → Desc
-- `σ : (E : Enum)(D : EnumT E → Desc) → Desc
-- `Σ `Π : (S : Set)(D : S → Desc) → Desc
-- So we can describe it within our universe of datatypes!
pattern `K` = zero
pattern `X` = suc zero
pattern `×` = suc (suc zero)
pattern `+` = suc (suc (suc zero))
pattern `σ` = suc (suc (suc (suc zero)))
pattern `Σ` = suc (suc (suc (suc (suc zero))))
pattern `Π` = suc (suc (suc (suc (suc (suc zero)))))
DescD : ∀{ℓ} → Desc {sucL ℓ}
DescD {ℓ} = `σ 7 (λ { `K` → `K (Set ℓ)
; `X` → `K (Lift ⊤)
; `×` → `X `× `X
; `+` → `X `× `X
; `σ` → `Σ (Lift Enum) λ { (lift E) →
`Π (Lift (EnumT E)) (λ _ →
`X) }
; `Σ` → `Σ (Set ℓ) λ S →
`Π (Lift S) (λ _ →
`X)
; `Π` → `Σ (Set ℓ) λ S →
`Π (Lift S) (λ _ →
`X)
; (suc (suc (suc (suc (suc (suc (suc ()))))))) })
Desc' : ∀{ℓ} → Set (sucL ℓ)
Desc' = μ DescD
`K' : ∀{ℓ} → Set ℓ → Desc' {ℓ}
`K' S = ⟨ `K` , S ⟩
`X' : ∀{ℓ} → Desc' {ℓ}
`X' = ⟨ `X` , lift tt ⟩
_`×'_ : ∀{ℓ} → Desc' {ℓ} → Desc' {ℓ} → Desc' {ℓ}
D₁ `×' D₂ = ⟨ `×` , D₁ , D₂ ⟩
_`+'_ : ∀{ℓ} → Desc' {ℓ} → Desc' {ℓ} → Desc' {ℓ}
D₁ `+' D₂ = ⟨ `+` , D₁ , D₂ ⟩
`σ' : ∀{ℓ} → (E : Enum)(T : EnumT E → Desc' {ℓ}) → Desc' {ℓ}
`σ' E T = ⟨ `σ` , lift E , T ∘ lower ⟩
`Σ' : ∀{ℓ} → (S : Set ℓ) → (S → Desc' {ℓ}) → Desc' {ℓ}
`Σ' S D = ⟨ `Σ` , S , D ∘ lower ⟩
`Π' : ∀{ℓ} → (S : Set ℓ) → (S → Desc' {ℓ}) → Desc' {ℓ}
`Π' S D = ⟨ `Π` , S , D ∘ lower ⟩
-- We could prove (assuming extensionality) that both presentations
-- are isomorphic to each other:
postulate
fromDescD : ∀{ℓ} → Desc {ℓ} → Desc' {ℓ}
toDescD : ∀{ℓ} → Desc' {ℓ} → Desc {ℓ}
iso-from-to : ∀{ℓ} → ∀ (D : Desc' {ℓ}) →
fromDescD (toDescD D) ≡ D
iso-to-from : ∀{ℓ} → ∀ (D : Desc {ℓ}) →
toDescD (fromDescD D) ≡ D
-- In an implementation, we could collapse this isomorphism and define
-- Desc directly from itself. There is a technical subltety that I
-- have eluded here, so be careful if you try this at home.
-- This bootstrap is described in more detail in Chapter 6 of my
-- thesis
-- [http://gallium.inria.fr/~pdagand/stuffs/thesis-2011-phd/thesis.pdf]
-- and in "The Gentle Art of Levitation"
-- [http://gallium.inria.fr/~pdagand/papers/levitation.pdf].
-- ** Extensions and improvements
-- *** Internal fixpoints
-- We would like to write the type of rose trees without encoding:
data RTree (A : Set) : Set where
node : A → List (RTree A) → RTree A
-- *** Explicit treatment of parameters
-- Because parameters have a parametric behavior, we would like to
-- single them out in the code of the datatype, to enable more precise
-- optimisations and transformations.
-- *** Inductive famillies
-- This is a rather simple extension, described in my thesis
-- [http://gallium.inria.fr/~pdagand/stuffs/thesis-2011-phd/thesis.pdf]
-- and modelled in
-- [http://gallium.inria.fr/~pdagand/stuffs/thesis-2011-phd/model/html/Chapter5.IDesc.html]
-- *** Elaboration of high-level definitions to codes
-- The benefit of this presentation is its tight connection with
-- semantics. To the user, we must then provide an high-level language
-- for inductive definitions and translate that language to
-- descriptions: by construction, we would obtain a translation
-- semantics for our inductive definitions.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- * Part II: Programming with 1st class citizens
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- ** Functoriality
-- The ⟦ D ⟧ function defines the object part of a functor. We can
-- also define its morphism part, as a generic program over
-- descriptions:
⟦_⟧map : ∀ {ℓ}(D : Desc) → {X Y : Set ℓ} →
(f : X → Y) → ⟦ D ⟧ X → ⟦ D ⟧ Y
⟦ `K S ⟧map f s = s
⟦ `X ⟧map f x = f x
⟦ D₁ `× D₂ ⟧map f xs = Data.Product.map (⟦ D₁ ⟧map f) (⟦ D₂ ⟧map f) xs
⟦ D₁ `+ D₂ ⟧map f xs = Data.Sum.map (⟦ D₁ ⟧map f) (⟦ D₂ ⟧map f) xs
⟦ `σ E D ⟧map f xs = σmap (λ e xs → ⟦ D e ⟧map f xs) xs
⟦ `Σ S D ⟧map f xs = Data.Product.map id (λ {s} → ⟦ D s ⟧map f) xs
⟦ `Π S D ⟧map f xs s = ⟦ D s ⟧map f (xs s)
-- ** Free monad
-- *** Tagged descriptions
-- To define the free monad, we ask for a slightly more structured
-- version of descriptions: tagged descriptions. In effect, we require
-- the description to start with a finite list of constructors (E ∈
-- Enum) and, then, for each constructor, we give its code.
-- This presentation enforces a 'constructor-headed normal form',
-- where our inductive definition necessarily provides a finite list
-- of constructors.
tDesc : Set₁
tDesc = Σ[ E ∈ Enum ] (EnumT E → Desc)
⌊_⌋ : tDesc → Desc {zeroL}
⌊ (E , D) ⌋ = `σ E D
μ⌊_⌋ : tDesc → Set
μ⌊_⌋ = μ ∘ ⌊_⌋
-- *** Free monad construction
-- Informally, the free monad of a functor F is defined by:
--
-- F * : Set → Set
-- F * X = μ Z. X + F(Z)
-- We can describe the free monad from the description of a functor F
-- by simply inserting a new constructor, 'var X'.
pattern `var` = zero
[_]D* : tDesc → Set → tDesc
[ (E , D) ]D* X = (suc E) , (λ { `var` → `K X
; (suc k) → D k })
-- Taking the least fixpoint of the resulting description, we have
-- built the free monad:
[_]* : tDesc → Set → Set
[ D ]* X = μ⌊ [ D ]D* X ⌋
-- *** Structure
-- Having built a monad, we can now equip it with its monadic
-- structure: a 'return', a functorial action 'fmap', a 'join', from
-- which we derive the Kleisli's 'bind'.
module Structure {D : tDesc} where
return : ∀ {X} → X → [ D ]* X
return x = ⟨ `var` , x ⟩
fmap : ∀{X Y} → (X → Y) → [ D ]* X → [ D ]* Y
fmap {X}{Y} f xs = foldD ⌊ [ D ]D* X ⌋ apply xs
where apply : ⟦ ⌊ [ D ]D* X ⌋ ⟧ ([ D ]* Y) → [ D ]* Y
apply (zero , x) = return (f x)
apply (suc k , ys) = ⟨ suc k , ys ⟩
join : ∀{X} → [ D ]* ([ D ]* X) → [ D ]* X
join {X} xs = foldD ⌊ [ D ]D* ([ D ]* X) ⌋ help xs
where help : ⟦ ⌊ [ D ]D* ([ D ]* X) ⌋ ⟧ ([ D ]* X) → [ D ]* X
help (zero , x) = x
help (suc k , xs) = ⟨ suc k , xs ⟩
bind : ∀{X Y} → [ D ]* X → (X → [ D ]* Y) → [ D ]* Y
bind {X}{Y} dxs f = join (fmap f dxs)
open Structure
-- *** Example: arithmetic expressions with variables
module AExpr where
-- To illustrate this machinery, we build the type of arithmetic
-- expressions with variables (note: no binding here). The 'var'
-- constructor corresponds exactly to the 'var' introduced by the
-- free monad construction, whilst substitution of variables
-- corresponds exactly to the bind of the free monad.
-- AExp V = {
-- var : V → AExp V
-- val : ℕ → AExp V
-- plus : AExp V → AExp V → AExp V
-- times : AExp V → AExp V → AExp V }
pattern `val` = zero
pattern `plus` = suc zero
pattern `times` = suc (suc zero)
-- We code the signature for 'val', 'plus' and 'times':
AExpD : tDesc
AExpD = 3 ,
λ { `val` → `K ℕ
; `plus` → `X `× `X
; `times` → `X `× `X
; (suc (suc (suc ()))) }
-- And obtain the AExp by free monad construction:
AExp : Set → Set
AExp V = [ AExpD ]* V
-- **** Operations
var : ∀{V} → V → AExp V
var = return
val : ∀{V} → ℕ → AExp V
val n = ⟨ suc `val` , n ⟩
plus : ∀{V} → AExp V → AExp V → AExp V
plus e₁ e₂ = ⟨ suc `plus` , e₁ , e₂ ⟩
times : ∀{V} → AExp V → AExp V → AExp V
times e₁ e₂ = ⟨ suc `times` , e₁ , e₂ ⟩
-- **** Substitution
substAExpr : ∀{V W} → AExp V → (V → AExp W) → AExp W
substAExpr = bind
-- **** Open term semantics
-- Here is an example of programming with that structure: we define
-- the open term semantics. Provided a valuation of variables, we
-- first subtitute the variables by their values. And we then simply
-- compute through.
evalAExpr : ∀{V} → (V → ℕ) → AExp V → ℕ
evalAExpr ρ tm = help (substAExpr tm (val ∘ ρ))
where α : ⟦ ⌊ [ AExpD ]D* ⊥ ⌋ ⟧ ℕ → ℕ
α (`var` , ())
α (suc `val` , n) = n
α (suc `plus` , m , n) = m + n
α (suc `times` , m , n) = m * n
α (suc (suc (suc (suc ()))) , _)
help : AExp ⊥ → ℕ
help = foldD ⌊ [ AExpD ]D* ⊥ ⌋ α
-- *** Example: syntax for effects
module Eff where
-- We can use the same machinery to build a (modular) syntax for
-- effectful programs. (Note: we are only dealing with syntax here,
-- not semantics). For example, we can build a monad for stateful
-- computations by defining a signature 'StateSig' with two
-- operations, 'get' and 'set':
-- State(S):
-- get : ⊤ → S
-- set : S → ⊤
pattern `get` = zero
pattern `set` = suc zero
StateSig : Set → tDesc
StateSig S = 2 , λ { `get` → `Π S λ _ → `X
; `set` → `Σ S λ _ → `X
; (suc (suc ())) }
State : Set → Set → Set
State S A = [ StateSig S ]* A
-- **** Operations
-- In the 'State' monad, we have the usual 'pure' ('return') and
-- bind of the monad, but also the stateful operations 'get' and
-- 'set':
pure : ∀{S A} → A → State S A
pure = return
_>>=_ : ∀{S A B} → State S A → (A → State S B) → State S B
_>>=_ = bind
get : ∀{S} → ⊤ → State S S
get tt = ⟨ suc `get` , (λ s → return s) ⟩
set : ∀{S} → S → State S ⊤
set s = ⟨ suc `set` , s , return tt ⟩
example : State ℕ ℕ
example =
get tt >>= λ n₁ →
set (n₁ + 3) >>= λ tt →
pure n₁
-- Again, this is just the syntax: to interpret these programs, one
-- has to give its semantics (in the usual State monad).
-- ** Derivative
-- We define here the Zipper from a derivation operator. However, not
-- every polynomial is differentiable: here, we only consider
-- 'finitary' polynomials. They are defined as follows:
∂Desc : Desc {zeroL} → Set
∂Desc (`K S) = ⊤
∂Desc `X = ⊤
∂Desc (D₁ `× D₂) = ∂Desc D₁ × ∂Desc D₂
∂Desc (D₁ `+ D₂) = ∂Desc D₁ × ∂Desc D₂
∂Desc (`σ E D) = π E (λ e → ∂Desc (D e))
∂Desc _ = ⊥
-- Provided that a description 'D' is differentiable, we compute its
-- derivative:
∂ : (D : Desc) → ∂Desc D → Desc {zeroL}
∂ (`K S) ∂D = `K (Lift ⊥)
∂ `X ∂D = `K ⊤
∂ (D₁ `+ D₂) (∂D₁ , ∂D₂) = ∂ D₁ ∂D₁ `+ ∂ D₂ ∂D₂
∂ (D₁ `× D₂) (∂D₁ , ∂D₂) = (∂ D₁ ∂D₁ `× D₂) `+ (D₁ `× ∂ D₂ ∂D₂)
∂ (`σ E D) ∂D = `Σ (EnumT E) (λ e → ∂ (D e) (appπ ∂D e))
∂ (`Σ S D) ()
∂ (`Π S D) ()
-- The zipper is then a pair of a context and a tree-in-context:
data Context (D : Desc){q : ∂Desc D} : Set where
root : Context D
layer : ⟦ ∂ D q ⟧ (μ D) → Context D {q} → Context D
Zipper : (D : Desc){q : ∂Desc D} → Set
Zipper D {q} = Context D {q} × μ D
-- There is then a bunch of operations on Zipper. Here is one,
-- 'plug'ging a tree back into a context:
plug : (D : Desc){q : ∂Desc D} → Context D {q} → μ D → μ D
plug D root t = t
plug D {q} (layer x ctxt) t = plug D {_} ctxt ⟨ plugF D {q} x t ⟩
where plugF : ∀{X} → (D : Desc){q : ∂Desc D} → ⟦ ∂ D q ⟧ X → X → ⟦ D ⟧ X
plugF (`K S) (lift ())
plugF `X tt x = x
plugF (D₁ `+ D₂) {∂D₁ , ∂D₂} (inj₁ xs₁) x = inj₁ (plugF D₁ {∂D₁} xs₁ x)
plugF (D₁ `+ D₂) {∂D₁ , ∂D₂} (inj₂ xs₂) x = inj₂ (plugF D₂ {∂D₂} xs₂ x)
plugF (D₁ `× D₂) {∂D₁ , ∂D₂} (inj₁ (∂xs₁ , xs₂)) x = plugF D₁ {∂D₁} ∂xs₁ x , xs₂
plugF (D₁ `× D₂) {∂D₁ , ∂D₂} (inj₂ (xs₁ , ∂xs₂)) x = xs₁ , plugF D₂ {∂D₂} ∂xs₂ x
plugF (`σ E D) {∂D} (e , xs) x = e , (plugF (D e) {appπ ∂D e} xs x)
plugF (`Σ S D) {()} _ _
plugF (`Π S D) {()} _ _
-- *** Example: binary tree
module ZipperTree {A B : Set} where
CTree' : (A B : Set) → Set
CTree' A B = Context (TreeD A B)
nodeL' : B → Tree' A B → CTree' A B → CTree' A B
nodeL' b l r = layer (`node` , inj₂ (b , (inj₁ (tt , l)))) r
nodeR' : B → CTree' A B → Tree' A B → CTree' A B
nodeR' b l r = layer (`node` , inj₂ (b , (inj₂ (r , tt)))) l
module Example where
open ZipperTree
-- Here is a tree:
example : Tree' ⊤ ℕ
example =
node' 1
(node' 2
(leaf' tt)
(leaf' tt))
(node' 5
(node' 6
(node' 7
(leaf' tt)
(leaf' tt))
(leaf' tt))
(node' 3
(leaf' tt)
(leaf' tt)))
-- Here is that same tree zipped:
exampleZ : Zipper (TreeD ⊤ ℕ)
exampleZ = ( nodeL' 5
(node' 3
(leaf' tt)
(leaf' tt))
(nodeR' 1
root
(node' 2
(leaf' tt)
(leaf' tt))),
node' 6
(node' 7
(leaf' tt)
(leaf' tt))
(leaf' tt))
example' : Tree' ⊤ ℕ
example' = plug (TreeD ⊤ ℕ) (proj₁ exampleZ) (proj₂ exampleZ)
-- After plugging, they are indeed definitionally equal:
test : example ≡ example'
test = refl
-- ** Left aside
-- *** Zipper navigation
-- There is an entire toolbox of Zipper operations. See Huet's Zipper
-- [http://yquem.inria.fr/~huet/PUBLIC/zip.pdf], McBride's "The
-- Derivative of a Regular Type is its Type of One-Hole Context"
-- [strictlypositive.org/diff.pdf].
-- *** Constructions on constructors (generic proofs)
-- When one define a new datatype in, say, Coq, the system introduces
-- a few generic lemmas, besides the standard induction
-- principle. These transformations have been described by McBride &
-- McKinna in a "A Few Constructions on Constructors"
-- [http://strictlypositive.org/concon.ps.gz] and they can be directly
-- implemented in type theory now (see "Elaborating Inductive
-- Definitions"
-- [http://gallium.inria.fr/~pdagand/stuffs/paper-2012-data-jfla/paper.pdf]
-- for a few examples)
-- *** Ornaments!
-- Because we have access to the definition of datatypes, we can
-- single out classes of transformation over datatypes. Ornaments are
-- such an object: they corresponds to structure-preserving
-- transformations, allowing us to transport functions across
-- datatypes. This is treated in McBride's "Ornamental Algebras,
-- Algebraic Ornaments"
-- [https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf],
-- "Transporting Functions across Ornaments"
-- [http://gallium.inria.fr/~pdagand/stuffs/paper-2012-patch-icfp/paper.pdf]
-- and "A Categorical Treatment of Ornaments"
-- [http://gallium.inria.fr/~pdagand/stuffs/paper-2012-catorn-lics/paper.pdf].
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
-- Part III: Structures & Equality
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
open import IProp
-- ** Functor laws
-- The functorial action of descriptions satisfy the following
-- equations:
postulate
map-id : ∀ {ℓ}{X : Set ℓ} → (D : Desc {ℓ}) →
(xs : ⟦ D ⟧ X) →
⊢ ⟦ D ⟧map id xs ≡ xs
map-∘ : ∀{ℓ}{X Y Z : Set ℓ} → (D : Desc {ℓ}) →
(xs : ⟦ D ⟧ X) → (f : Y → Z)(g : X → Y) →
⊢ ⟦ D ⟧map (f ∘ g) xs ≡ (⟦ D ⟧map f ∘ ⟦ D ⟧map g) xs
-- In "New equations for neutral terms"
-- [http://arxiv.org/abs/1304.0809], Allais et al. craft an NbE model
-- in which these laws hold definitionally for the map operation over
-- lists.
-- ** Monad laws
-- The monadic operations associated with the free monad satisfy the
-- following equations:
postulate
bind-left-id : {X Y : Set} → (D : tDesc)
(x : X)(f : X → [ D ]* Y) →
⊢ bind (return x) f ≡ f x
bind-right-id : {X : Set} → (D : tDesc)
(xs : [ D ]* X) →
⊢ bind xs return ≡ xs
bind-∘ : {X Y Z : Set} → (D : tDesc)
(xs : [ D ]* X)(g : X → [ D ]* Y)(f : Y → [ D ]* Z) →
⊢ bind (bind xs g) f ≡ bind xs ((λ xs → bind xs f) ∘ g)
-- In a prototype of Epigram 2, the NbE algorithm was customized to
-- use these equations as left-to-right rewrite rules (see
-- [substMonadOpSimp] in
-- [https://github.com/brixen/Epigram/blob/master/src/Features/FreeMonad.lhs]).
-- A similar trick was also described by Bob Atkey in "A Type Checker
-- that knows its Monad from its Elbow"
-- [http://bentnib.org/posts/2011-12-14-type-checker.html].
-- ** Binding laws
-- Another instance of an interesting algebraic structure is syntax
-- with binding. For simplicity, I focus here on untyped binders
-- (meaning, over ℕ) but one can easily generalise to typed bindings.
-- The machinery deployed here is strongly inspired by Hirschowitz &
-- Maggesi's "Modules over monads and initial semantics"
-- [http://web.math.unifi.it/users/maggesi/syn.pdf] and Ahrens &
-- Zsidó's "Initial Semantics for higher-order typed syntax in Coq"
-- [http://jfr.cib.unibo.it/article/view/2066]. I've just adapted
-- their presentation to a relative monad, but not as abstractly as
-- Ahrens' "Modules over relative monads for syntax and semantics"
-- [http://arxiv.org/abs/1107.5252].
-- *** Signature
-- For convenience, I give here an extensional presentation, some sort
-- of W-types with bindings:
record BSig : Set₁ where
field
-- Operations:
Op : Set
-- Aritites:
Ar : Op → Set
-- Bindings:
Bi : ∀ {sh} → Ar sh → ℕ
-- *** Free term algebra
module Terms (Σ : BSig) where
open BSig Σ
-- We can then build the terms and scopes corresponding the
-- signature Σ :
mutual
-- Term:
data Tm (n : ℕ) : Set where
`var : Fin n → Tm n
`op : (sh : Op)(Xs : (pos : Ar sh) → Scope[ Bi pos ] n) → Tm n
-- Binder of k-variables :
data Scope[_] (k : ℕ)(n : ℕ) : Set where
sc : Tm (k + n) → Scope[ k ] n
-- A relative strength over Tm (provided that Tm is a functor, which
-- we will define) is defined as:
Strength : Set
Strength = {l m : ℕ} → (∀{l m} → (Fin l → Fin m) → Tm l → Tm m) →
Tm l ⊎ Fin m → Tm (m + l)
-- *** Substitution structure
module Subst (Σ : BSig)
(str : Terms.Strength Σ) where
open BSig Σ
open Terms Σ
-- We then implement a generic substitution and weakening operation:
mutual
-- Scope[ k ] : ℕ → Set is a functor
-- ie. for f ∈ ℕ(m, n)
-- we have a functorial map
-- mapSc f ∈ Set(Scope m, Scope n)
mapSc : ∀{k l m} →
(Fin l → Fin m) → Scope[ k ] l → Scope[ k ] m
mapSc {k} ρ (sc tm) = sc (mapTm (Data.Fin.lift k ρ) tm)
-- Tm : ℕ → Set is a functor
-- ie. for f ∈ W(m, n),
-- we have a functorial map
-- mapTm f ∈ Set(Tm m, Tm n)
mapTm : ∀{l m} →
(Fin l → Fin m) → Tm l → Tm m
mapTm ρ (`var x) = `var (ρ x)
mapTm ρ (`op sh Xs) = `op sh λ pos → mapSc {Bi pos} ρ (Xs pos)
-- Tm Σ : ℕ → Set is a relative monad over Fin : ℕ → Set
-- ie.
-- 1. we have a natural transformation
-- return : ∀ m. Set(Fin m, Tm m)
var : ∀{m} → Fin m → Tm m
var = `var
mutual
-- 2. we have a natural transformation
-- bind : ∀ m n. Set(Fin m, Tm n) → Set(Tm m, Tm n)
sub : ∀{m n} → (Fin m → Tm n) → Tm m → Tm n
sub ρ (`var x) = ρ x
sub ρ (`op sh Xs) = `op sh (λ pos → weaken {Bi pos} ρ (Xs pos))
-- Scope[ k ] : ℕ → Set is a Tm-module
-- ie. we have a natural transformation
-- weaken : ∀ m n. Set(Fin m, Tm n) → Set(Scope[ k ] m, Scope[ k ] n)
weaken : ∀{k m n} → (Fin m → Tm n) → Scope[ k ] m → Scope[ k ] n
weaken {k}{m}{n} ρ (sc tm) = sc (sub (λ v → str {n}{k} mapTm (Data.Sum.map ρ id (monFin v))) tm)
where monFin : ∀{n m} → Fin (n + m) → Fin m ⊎ Fin n
monFin {zero} xs = inj₁ xs
monFin {suc m} zero = inj₂ zero
monFin {suc m} (suc xs) with monFin {m} xs
monFin {suc m} (suc xs) | inj₁ x = inj₁ x
monFin {suc m} (suc xs) | inj₂ y = inj₂ (suc y)
-- *** Example: Well-scoped, untyped lambda-calculus
module LC where
Σλam : BSig
Σλam = record { Op = Bool
; Ar = λ { true → ⊤
; false → Bool }
; Bi = λ { {true} tt → 1
; {false} b → 0 } }
open Terms Σλam
λam : ℕ → Set
λam n = Tm n
app : ∀{n} → λam n → λam n → λam n
app f s = `op false (λ { true → sc f
; false → sc s })
abs : ∀{n} → λam (suc n) → λam n
abs b = `op true (λ { tt → sc b })
-- **** Substitution
str : Terms.Strength Σλam
str {m = n} fmap (inj₁ tm) = fmap (raise n) tm
str fmap (inj₂ k) = `var (inject+ _ k)
open Subst Σλam str
substλ : ∀{m n} → λam m → (Fin m → λam n) → λam n
substλ tm ρ = sub ρ tm
-- **** Application
tm1 : λam 0
tm1 = abs (var zero)
tm2 : λam 1
tm2 = abs (app (var (suc zero)) (var zero))
tm3 : λam 0
tm3 = substλ tm2 ρ
where ρ : Fin 1 → λam 0
ρ zero = tm1
ρ (suc ())
-- *** Equations
module Equation (Σ : BSig)(str : Terms.Strength Σ) where
open Terms Σ
open Subst Σ str
-- More interestingly, these substitution operations have a
-- well-behaved equationnal theory. We have the usual monadic
-- identities:
postulate
sub-left-id : {m n : ℕ} →
(x : Fin m)(f : Fin m → Tm n) →
⊢ sub f (var x) ≡ f x
sub-right-id : {m : ℕ} →
(xs : Tm m) →
⊢ sub var xs ≡ xs
sub-∘ : {l m n : ℕ} →
(xs : Tm l)(g : Fin l → Tm m)(f : Fin m → Tm n) →
⊢ sub f (sub g xs) ≡ sub ((sub f) ∘ g) xs
-- To which we add the identities associated with the Tm-module:
weaken-id : {k l : ℕ} →
(xs : Scope[ k ] l) →
⊢ weaken var xs ≡ xs
weaken-∘ : {k l m n : ℕ} →
(xs : Scope[ k ] l)(g : Fin l → Tm m)(f : Fin m → Tm n) →
⊢ weaken f (weaken g xs) ≡ weaken (sub f ∘ g) xs
-- * EOF
-- Local Variables:
-- mode: outline-minor
-- outline-regexp: "-- [*\f]+"
-- outline-level: outline-level
-- End: