```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)

-- *** 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
μ⌊_⌋ = μ ∘ ⌊_⌋

-- 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

[_]* : 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

-- 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.

-- 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

-- 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"
-- 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:
```