## Wednesday 27 April 2016

### Descriptions

Desc.agda
```-- In this post I'll shortly introduce descriptions and describe a variant of them that I prefer.
-- If you haven't seen this form of generic programming before,
-- http://effectfully.blogspot.com/2016/02/simple-generic-programming.html

{-# OPTIONS --type-in-type --no-termination-check #-}

module Desc where

open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Unit.Base
open import Data.Bool.Base
open import Data.Nat.Base
open import Data.Product

module Computational where
-- I'll start by defining descriptions in their usual computational form.

data Desc I : Set where
ind : I -> Desc I
κ   : Set -> Desc I
σ π : ∀ A -> (A -> Desc I) -> Desc I
_⊛_ : Desc I -> Desc I -> Desc I

⟦_⟧ : ∀ {I} -> Desc I -> (I -> Set) -> Set
⟦ ind i ⟧ F = F i
⟦ κ A   ⟧ F = A
⟦ σ A B ⟧ F = Σ A λ x -> ⟦ B x ⟧ F
⟦ π A B ⟧ F = (x : A) -> ⟦ B x ⟧ F
⟦ D ⊛ E ⟧ F = ⟦ D ⟧ F × ⟦ E ⟧ F

record μ {I} (F : I -> Desc I) j : Set where
inductive
constructor node
field knot : ⟦ F j ⟧ (μ F)

-- `ind i` is an inductive position. `⟦ ind i ⟧ (μ F)` reduces to `μ F i`,
-- so that is where knot tying happens. In `μ F j` `j` is the index of a term
-- and in `ind i` `i` is the index of a subterm.

-- `κ` allows to embed any `Set` into a description.
-- `σ` allows this too, but `κ` is non-recursive and thus can finish a description.

-- `σ` serves two purposes:
--   1. It allows to split a description of a data type into descriptions of several constructors.
--      E.g. we can express the fact that a data type has two constructors by defining its
--      description as `σ Bool λ b -> if b then cons₁ else cons₂` for some `cons₁` and `cons₂`.
--   2. It encodes top-level Π-types in the type of a constructor in a target language.
--      I'll explain in a minute why we use `σ` to encode `Π`.

-- `π` is for higher-order inductive occurrences. I.e. for data types where an inductive
-- position appears to the right of the arrow. E.g. `W`:

-- data W (A : Set) (B : A -> Set) : Set where
--   sup : (x : A) -> (B x -> W A B) -> W A B

-- or `Desc` itself (the `σ` and `π`) constructors.

-- `D ⊛ E` is a first-order equivalent of `π Bool λ b -> if b then D else E`.

-- The choice operator mentioned above:

_⊕_ : ∀ {I} -> Desc I -> Desc I -> Desc I
D ⊕ E = σ Bool λ b -> if b then D else E

-- Here is an example of described data type.

list : Set -> Desc ⊤
list A = κ ⊤
⊕ σ A λ _ -> ind tt

List : Set -> Set
List A = μ (λ _ -> list A) tt

-- Lists are a non-indexed data type, hence we pass `⊤` to `Desc`, and
-- lists have two constructors: the one that doesn't contain any data
-- (which is expressed as `κ ⊤`) and the other that contains an `A` and an inductive occurrence.

-- The recovered constructors:

-- [] : ∀ {A} -> List A
pattern [] = node (true , tt)

-- _∷_ : ∀ {A} -> A -> List A -> List A
pattern _∷_ x xs = node (false , x , xs)

-- Now we can see why `σ` is used to describe the arguments to a constructor.
-- If we define `List` via the `data` keyword, then `_∷_` is a "god-given" function,
-- but internally it's just a tag "cons" stored among with an element and a sublist.
-- Here we store the element and the sublist explicitly.

-- You can read described constructors like there is `-> D` after them,
-- where `D` is the data type being described. E.g. for the usual lists `_∷_` can be defined as

-- `cons : (A × List A) -> List A`

-- which is the same as

-- `cons : (Σ A λ _ -> List A) -> List A`.

-- compare this to `_∷_` described above: `σ A λ _ -> ind tt`.

-- Described lists have the usual eliminator.

elimList : ∀ {A}
-> (P : List A -> Set)
-> (∀ {xs} x -> P xs -> P (x ∷ xs))
-> P []
-> ∀ xs
-> P xs
elimList P f z  []      = z
elimList P f z (x ∷ xs) = f x (elimList P f z xs)

-- Now let's describe something indexed.

fin : ℕ -> Desc ℕ
fin n = (σ ℕ λ m -> κ (n ≡ suc m))
⊕ (σ ℕ λ m -> σ (n ≡ suc m) λ _ -> ind m)

Fin : ℕ -> Set
Fin = μ fin

-- fzero : ∀ {n} -> Fin (suc n)
pattern fzero {n} = node (true , n , refl)

-- fsuc : ∀ {n} -> Fin n -> Fin (suc n)
pattern fsuc {n} i = node (false , n , refl , i)

-- `Fin` has two constructors and in order to describe them we must introduce explicit
-- unification constraints. `Fin n` is inhabited only when `n ≡ suc m` for some `m` --
-- that's what the description says. Since the unification constraint is the same for
-- both constructors, we could introduce it before defining actual constructors:

module Before where
fin′ : ℕ -> Desc ℕ
fin′ n = σ ℕ λ m -> σ (n ≡ suc m) λ _ -> κ ⊤ ⊕ ind m

Fin′ : ℕ -> Set
Fin′ = μ fin′

fzero′ : ∀ {n} -> Fin′ (suc n)
fzero′ {n} = node (n , refl , true , tt)

fsuc′ : ∀ {n} -> Fin′ n -> Fin′ (suc n)
fsuc′ {n} i = node (n , refl , false , i)

-- `Fin` has the usual induction principle:

elimFin : ∀ {n}
-> (P : ∀ {n} -> Fin n -> Set)
-> (∀ {n} {i : Fin n} -> P i -> P (fsuc i))
-> (∀ {n} -> P (fzero {n}))
-> (i : Fin n)
-> P i
elimFin P f x  fzero   = x
elimFin P f x (fsuc i) = f (elimFin P f x i)

-- But these explicit unification constraints are quite ugly.
-- Moreover, sometimes you want to have access to them while defining generic functions
-- over `Desc`, but constraints can appear everywhere in the definition of a description,
-- so you can't locate them by just pattern matching on a `Desc`.

module Propositional where
-- So here are propositional descriptions that solve most of the problems mentioned above.
-- I'm taking stuff directly from [1].

data Desc I : Set where
ret  : I -> Desc I
σ    : ∀ A -> (A -> Desc I) -> Desc I
ind  : I -> Desc I -> Desc I
hind : ∀ A -> (A -> I) -> Desc I -> Desc I

Extend : ∀ {I} -> Desc I -> (I -> Set) -> I -> Set
Extend (ret i)      F j = j ≡ i
Extend (σ A B)      F j = Σ A λ x -> Extend (B x) F j
Extend (ind i D)    F j = F i × Extend D F j
Extend (hind A k D) F j = ((x : A) -> F (k x)) × Extend D F j

record μ {I} (D : Desc I) j : Set where
inductive
constructor node
field knot : Extend D (μ D) j

-- Each desciption ends with `ret` that receives the index of a term.
-- `σ` is the same thing as before.
-- `ind` carries an inductive position and the rest of a description.
-- `hind` is the same thing as `ind`, but an inductive occurrence is higher-order.

-- `Extend` is straightforward and pretty linear. The only interesting case is `ret`:
-- that's where we put constraints. Now we don't need to write them down explicitly.

-- However I don't like the `(A -> I)` part in `hind`. If we want to encode something like

data Foo : Set where
foo : (ℕ -> Bool -> Foo) -> Foo

-- then `A` must be `ℕ × Bool` and this compulsory uncurrying is annoying.
-- Manual extraction of elements from a big tuple is verbose and ugly.

-- To encode this definition

data Bar : Set where
foo : (ℕ -> Bar × Bar) -> Bar

-- we have to transform it to

data Bar′ : Set where
foo : (ℕ -> Bar′) -> (ℕ -> Bar′) -> Bar′

-- Computational descriptions didn't have these problems.

module CompProp where
infixr 6 _⊛_
infixr 5 _⊕_

-- So here is a compact and convenient form of descriptions:

data Desc I : Set where
var : I -> Desc I
π   : ∀ A -> (A -> Desc I) -> Desc I
_⊛_ : Desc I -> Desc I -> Desc I

⟦_⟧ : ∀ {I} -> Desc I -> (I -> Set) -> Set
⟦ var i ⟧ F = F i
⟦ π A B ⟧ F = ∀ x -> ⟦ B x ⟧ F
⟦ D ⊛ E ⟧ F = ⟦ D ⟧ F × ⟦ E ⟧ F

Extend : ∀ {I} -> Desc I -> (I -> Set) -> I -> Set
Extend (var j) F i = j ≡ i
Extend (π A B) F i = ∃ λ x -> Extend (B x) F i
Extend (D ⊛ E) F i = ⟦ D ⟧ F × Extend E F i

record μ {I} (D : Desc I) i : Set where
inductive
constructor node
field knot : Extend D (μ D) i

-- `⟦_⟧` is taken from computational descriptions and
-- `Extend` is taken from propositional descriptions.

-- `var` serves as both `ind` and `ret`. There is `var i` at the end of each constructor,
-- where `i` is the index that a constructor returns. All other `var`s in a description
-- represent inductive positions.

-- `π` subsumes both `σ` and `π` from computation descriptions.
-- `Extend` interprets `π` as `∃` and `⟦_⟧` interprets `π` as `Π`.

-- Note that `μ` in this representation and in the propositional one receives a proper
-- first-order `Desc`, while in the computational representation `μ` receives a
-- higher-order `I -> Desc I`.

_⊕_ : ∀ {I} -> Desc I -> Desc I -> Desc I
D ⊕ E = π Bool λ b -> if b then D else E

-- Everything should become clear after looking at an example:

vec : Set -> Desc ℕ
vec A = var 0
⊕ π ℕ λ n -> π A λ _ -> var n ⊛ var (suc n)

Vec : Set -> ℕ -> Set
Vec A = μ (vec A)

-- Vectors have two constructors: the one that doesn't contain any data and
-- the other that carries an `A` and a subvector `xs : Vec A n`.
-- The former constructor returns a vector of length `0` and
-- the latter returns a vector of length `suc n`.
-- Compare this to the usual definition of vectors which has the same pattern:

module UsualVec where
data Vec′ (A : Set) : ℕ -> Set where
[]  : Vec′ A 0
_∷_ : ∀ {n} -> A -> Vec′ A n -> Vec′ A (suc n)

-- `Extend` interprets `π` as `∃`, i.e. like `⟦_⟧` in computational descriptions interprets `σ`,
-- so the recovered constructors are very similar:

-- [] : ∀ {A} -> Vec A 0
pattern [] = node (true , refl)

-- _∷_ : ∀ {n A} -> A -> Vec A n -> Vec A (suc n)
pattern _∷_ {n} x xs = node (false , n , x , xs , refl)

elimVec : ∀ {n A}
-> (P : ∀ {n} -> Vec A n -> Set)
-> (∀ {n} {xs : Vec A n} x -> P xs -> P (x ∷ xs))
-> P []
-> (xs : Vec A n)
-> P xs
elimVec P f z  []      = z
elimVec P f z (x ∷ xs) = f x (elimVec P f z xs)

-- Let's now encode `W`:

w : ∀ A -> (A -> Set) -> Desc ⊤
w A B = π A λ x -> (π (B x) λ _ -> var tt) ⊛ var tt

W : ∀ A -> (A -> Set) -> Set
W A B = μ (w A B) tt

-- sup : ∀ {A B} -> (x : A) -> (B x -> W A B) -> W A B
pattern sup x g = node (x , g , refl)

-- The key thing here is that `Extend` interprets `D` and `E` in `D ⊛ E` differently.
-- In `D` `π` encodes actual `Π` and `var i` is an inductive position.
-- In `E` `π` encodes `∃` and `var i` (if it's not to the left of another `_⊛_`)
-- represents the index that a constructor returns.

-- Compare this to the usual definion of `W`:

module UsualW where
data W′ A (B : A -> Set) : Set where
sup′ : (x : A) -> (B x -> W′ A B) -> W′ A B

-- They are quite the same except that `_⊛_` is replaced by `_->_`.

-- As the final example we can encode `Desc` itself:

data Codes : Set where
varᶜ πᶜ ⊛ᶜ : Codes

desc : Set -> Desc ⊤
desc I = π Codes λ
{ varᶜ -> π I λ _ -> var tt
; πᶜ   -> π Set λ A -> (π A λ _ -> var tt) ⊛ var tt
; ⊛ᶜ   -> var tt ⊛ var tt ⊛ var tt
}

Desc′ : Set -> Set
Desc′ I = μ (desc I) tt

-- var′ : ∀ {I} -> I -> Desc′ I
pattern var′ i = node (varᶜ , i , refl)

-- π′ : ∀ {I} A -> (A -> Desc′ I) -> Desc′ I
pattern π′ A B = node (πᶜ , A , B , refl)

-- _⊛′_ : ∀ {I} -> Desc′ I -> Desc′ I -> Desc′ I
pattern _⊛′_ D E = node (⊛ᶜ , D , E , refl)

-- `Desc` and `Desc′` are clearly isomorphic:

fromDesc : ∀ {I} -> Desc I -> Desc′ I
fromDesc (var i) = var′ i
fromDesc (π A B) = π′ A λ x -> fromDesc (B x)
fromDesc (D ⊛ E) = fromDesc D ⊛′ fromDesc E

toDesc : ∀ {I} -> Desc′ I -> Desc I
toDesc (var′ i) = var i
toDesc (π′ A B) = π A λ x -> toDesc (B x)
toDesc (D ⊛′ E) = toDesc D ⊛ toDesc E

module References where
-- [1] "Modeling Elimination of Described Types"
-- Larry Diehl
-- http://spire-lang.org/blog/2014/01/15/modeling-elimination-of-described-types/
```