-- This posts describes how to derive eliminators of described data types. {-# OPTIONS --type-in-type #-} open import Function open import Relation.Binary.PropositionalEquality open import Data.Product infixr 6 _⊛_ -- I'll be using the form of descriptions introduced in the previous post: -- http://effectfully.blogspot.com/2016/04/descriptions.html 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 ⟧ B = B i ⟦ π A D ⟧ B = ∀ x -> ⟦ D x ⟧ B ⟦ D ⊛ E ⟧ B = ⟦ D ⟧ B × ⟦ E ⟧ B Extend : ∀ {I} -> Desc I -> (I -> Set) -> I -> Set Extend (var i) B j = i ≡ j Extend (π A D) B i = ∃ λ x -> Extend (D x) B i Extend (D ⊛ E) B i = ⟦ D ⟧ B × Extend E B i data μ {I} (D : Desc I) j : Set where node : Extend D (μ D) j -> μ D j -- It is crucial to define `μ` as a `data` and not as an inductive `record`, -- because termination checker works better with `data`s. -- While defining the generic `elim` function, we'll be keeping in mind some -- described constructor. Let it be `_∷_` for vectors: -- `cons-desc = π ℕ λ n -> π A λ _ -> var n ⊛ var (suc n)` module Verbose where -- How to get the actual type of the constructor from this description? -- Each `π` correspons to some `->` and each `_⊛_` corresponds to it as well. -- I.e. the actual type is `(n : ℕ) -> A -> Vec A n -> Vec (suc n)`. -- After generalizing `Vec A` to `B`, we get the following definition: Cons : ∀ {I} -> (I -> Set) -> Desc I -> Set Cons B (var i) = B i Cons B (π A D) = ∀ x -> Cons B (D x) Cons B (D ⊛ E) = ⟦ D ⟧ B -> Cons B E -- `Cons B cons-desc` evaluates to `(n : ℕ) -> A -> B n -> B (suc n)` as required. -- Eliminator of `_∷_` (with `Vec A` generalized to `B`) looks like this: -- `(n : ℕ) -> (x : A) -> {xs : B n} -> P xs -> P (x ∷ xs)` -- so we need to eliminate `cons-desc` again, but now with `_∷_ : Cons B cons-desc` provided -- (to form the final `P (x ∷ xs)` part). Note that each inductive occurrence in a description -- becomes replaced by the corresponding induction hypothesis, hence the `_⊛_` case -- in the function below: ElimBy : ∀ {I B} -> ((D : Desc I) -> ⟦ D ⟧ B -> Set) -> (D : Desc I) -> Cons B D -> Set ElimBy P (var i) x = P (var i) x ElimBy P (π A D) f = ∀ x -> ElimBy P (D x) (f x) ElimBy P (D ⊛ E) f = ∀ {x} -> P D x -> ElimBy P E (f x) -- The type of `P` is `(D : Desc I) -> ⟦ D ⟧ B -> Set` instead of `∀ {i} -> B i -> Set`, -- because there can be a higher-order inductive occurrence (like in `W`) and -- the induction hypothesis have to be computed by induction on a `Desc`. -- We'll do this in a moment. -- The next step is to compute the constructor. -- As described in the previous post the actual `_∷_` can be recovered as -- `_∷_ {n} x xs = node (n , x , xs , refl)` -- (it's `node (false, n , x , xs , refl)` for the actual `Vec`, -- because the first element in a tuple allows to distinguish `[]` and `_∷_`) -- So all we need is to define a function that receives `n` arguments, -- puts them in a tuple and applies `node` to it. That's the usual CPS stuff: cons : ∀ {I B} -> (D : Desc I) -> (∀ {j} -> Extend D B j -> B j) -> Cons B D cons (var i) k = k refl cons (π A D) k = λ x -> cons (D x) (k ∘ _,_ x) cons (D ⊛ E) k = λ x -> cons E (k ∘ _,_ x) -- However note that `ElimBy` and `cons` are defined by the same induction on `D`. -- Hence we can drop `Cons` and `cons` stuff and compute `ElimBy` directly. -- Here is the final definition of `ElimBy`: ElimBy : ∀ {I B} -> ((D : Desc I) -> ⟦ D ⟧ B -> Set) -> (D : Desc I) -> (∀ {j} -> Extend D B j -> B j) -> Set ElimBy C (var i) k = C (var i) (k refl) ElimBy C (π A D) k = ∀ x -> ElimBy C (D x) (k ∘ _,_ x) ElimBy C (D ⊛ E) k = ∀ {x} -> C D x -> ElimBy C E (k ∘ _,_ x) -- Now we need to compute induction hypotheses. Recall how `W` looks like: data W (A : Set) (B : A -> Set) : Set where sup : ∀ x -> (B x -> W A B) -> W A B -- Its eliminator is elimW : ∀ {α β π} {A : Set α} {B : A -> Set β} -> (P : W A B -> Set π) -> (∀ {x} {g : B x -> W A B} -> (∀ y -> P (g y)) -> P (sup x g)) -> ∀ w -> P w elimW P h (sup x g) = h (λ y -> elimW P h (g y)) -- I.e. the induction hypothesis for higher-order `g : B x -> W A B` is -- `(y : B x) -> P (g y)` (higher-order as well). Hyp : ∀ {I B} -> (∀ {i} -> B i -> Set) -> (D : Desc I) -> ⟦ D ⟧ B -> Set Hyp C (var i) y = C y Hyp C (π A D) f = ∀ x -> Hyp C (D x) (f x) Hyp C (D ⊛ E) (x , y) = Hyp C D x × Hyp C E y -- When an inductive occurrence is a tuple, the induction hypothesis is a tuple too, -- hence the `_⊛_` case above. -- Finally, the type of a function that eliminator receives -- (I'll call it "an eliminating function") is Elim : ∀ {I B} -> (∀ {i} -> B i -> Set) -> (D : Desc I) -> (∀ {j} -> Extend D B j -> B j) -> Set Elim = ElimBy ∘ Hyp -- It only remains to construct the actual generic eliminator. module _ {I} {D₀ : Desc I} (P : ∀ {j} -> μ D₀ j -> Set) (h : Elim P D₀ node) where mutual elimExtend : ∀ {j} -> (D : Desc I) {k : ∀ {j} -> Extend D (μ D₀) j -> μ D₀ j} -> Elim P D k -> (e : Extend D (μ D₀) j) -> P (k e) elimExtend (var i) z refl = z elimExtend (π A D) h (x , e) = elimExtend (D x) (h x) e elimExtend (D ⊛ E) h (d , e) = elimExtend E (h (hyp D d)) e hyp : ∀ D -> (d : ⟦ D ⟧ (μ D₀)) -> Hyp P D d hyp (var i) d = elim d hyp (π A D) f = λ x -> hyp (D x) (f x) hyp (D ⊛ E) (x , y) = hyp D x , hyp E y elim : ∀ {j} -> (d : μ D₀ j) -> P d elim (node e) = elimExtend D₀ h e -- No surpise we need a family of mutually defined functions. -- `D₀` is the description of a data being eliminated. It's in the module parameter -- among with `P` and an eliminating function `h`, because otherwise it would be required -- to trace them explicitly through all three functions and these parameters never change. -- `elim` unfolds a `μ` and delegates the work to `elimExtend`. -- `elimExtend` is defined by induction on `D`: -- - At the end of a description we simply return what has been computed so far. -- - On encountering a non-inductive argument to a constructor we -- apply the eliminating function to it. -- - On encountering an inductive argument to a constructor we -- compute recursively (`hyp` calls `elim` in the `var` case) and -- apply the elimination function to the result of the computation. -- That's basically it. An example: open import Data.Bool.Base open import Data.Nat.Base _<?>_ : ∀ {α} {A : Bool -> Set α} -> A true -> A false -> ∀ b -> A b (x <?> y) true = x (x <?> y) false = y _⊕_ : ∀ {I} -> Desc I -> Desc I -> Desc I D ⊕ E = π Bool (D <?> E) vec : Set -> Desc ℕ vec A = var 0 ⊕ π ℕ λ n -> π A λ _ -> var n ⊛ var (suc n) Vec : Set -> ℕ -> Set Vec A = μ (vec A) pattern [] = node (true , refl) pattern _∷_ {n} x xs = node (false , n , x , xs , refl) elimVec : ∀ {n A} -> (P : ∀ {n} -> Vec A n -> Set) -> (∀ {n} x {xs : Vec A n} -> P xs -> P (x ∷ xs)) -> P [] -> (xs : Vec A n) -> P xs elimVec P f z = elim P (z <?> λ _ -> f) -- Since vectors have two constructors, `vec` starts with `π Bool` which allows to split -- the description into two parts: the one that describes `[]` and the other that describes `_∷_`. -- That's why an eliminating function for vectors is of the form `(b : Bool) -> ...` and -- we use `_<?>_` to choose between an eliminating function for `[]` (just a value `z`) and -- an eliminating function for `_∷_` (which ignores `n : ℕ`).
Thursday 16 June 2016
Deriving eliminators of described data types
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment