-- Stealing an intro from sigfpe ([1]), -- I've decided that Normalization by Evaluation is the hardest trivial thing in type theory. -- Let's go down the rabbit hole. module NbE where open import Function open import Relation.Binary.PropositionalEquality open import Data.Empty open import Data.Nat.Base open import Data.Sum open import Data.List.Base module Readback where infixr 3 ƛ_ infixl 6 _·_ _∙_ -- NbE is usually explained like this: -- 1. first-order lambda terms representation -- 2. higher-order lambda terms representation -- 3. `readback' -- 4. `eval` -- 5. `norm = readback ∘ eval` -- Our plan is as follows: -- 1. higher-order lambda terms representation -- 2. normalization for higher-order lambda terms -- 3. first-order lambda terms representation -- 4. `toValue`, `fromValue` -- 5. `norm = fromValue ∘ normValue ∘ toValue` -- 6. `eval` -- 7. `norm = readback ∘ eval` -- The higher-order lambda terms representation is {-# NO_POSITIVITY_CHECK #-} data Value (A : Set) : Set where pure : A -> Value A lam : (Value A -> Value A) -> Value A _·_ : Value A -> Value A -> Value A VTerm : Set₁ VTerm = ∀ {A} -> Value A -- A few examples: Iᵥ : VTerm Iᵥ = lam λ x -> x Kᵥ : VTerm Kᵥ = lam λ x -> lam λ y -> x Sᵥ : VTerm Sᵥ = lam λ f -> lam λ g -> lam λ x -> f · x · (g · x) -- It might be instructive to add some parentheses: S⁽⁾ : VTerm S⁽⁾ = lam (λ f -> lam (λ g -> lam (λ x -> f · x · (g · x)))) -- `lam` receives a continuation that returns a `Value`. -- "Continuations are programs with holes in them" (quoted from [2]), -- so `S` says "give me some `f`, `g` and `x`" and I'll produce `f · x · (g · x)` to you". -- But these `f`, `g` and `x` are themselves `VTerm`s, -- hence we can define function application that β-reduces: _∙_ : ∀ {A} -> Value A -> Value A -> Value A lam k ∙ x = k x f ∙ x = f · x -- If the head constructor is `lam`, then there is a hole that we can fill. -- Otherwise we simply use the `_·_` constructor. -- A simple test: SI : ∀ {A} -> Sᵥ {A} ∙ Iᵥ ≡ lam λ g -> lam λ x -> Iᵥ · x · (g · x) SI = refl -- `f` was substituted by `Iᵥ`. -- Normalization of a `Value` is similar: {-# TERMINATING #-} normValue : ∀ {A} -> Value A -> Value A normValue (pure x) = pure x normValue (lam k ) = lam λ x -> normValue (k x) normValue (f · x ) = case normValue f of λ { (lam k) -> normValue (k x) ; nf -> nf · normValue x } -- In the `f · x` case we first normalize `f`, if the head constructor is `lam`, -- then there is a hole, we fill it and proceed further. Otherwise -- `normValue (f · x)` is the same as `normValue f · normValue x`. -- An example: SKK : normValue (Sᵥ · Kᵥ · Kᵥ · pure 0) ≡ normValue (Iᵥ · pure 0) SKK = refl -- The first-order representation of lambda terms will contain de Bruijn indices data Term : Set where var : ℕ -> Term ƛ_ : Term -> Term _·_ : Term -> Term -> Term -- A few examples: I : Term I = ƛ var 0 K : Term K = ƛ ƛ var 1 S : Term S = ƛ ƛ ƛ var 2 · var 0 · (var 1 · var 0) -- Here is a function that converts higher-order lambda terms to theiry first-order counterparts: var⁺ : ℕ -> ℕ -> Term var⁺ m n = var (n ∸ m ∸ 1) fromValue : VTerm -> Term fromValue x = go 0 x where go : ℕ -> Value ℕ -> Term go n (pure m) = var⁺ m n go n (lam k ) = ƛ (go (suc n) (k (pure n))) go n (f · x ) = go n f · go n x -- In `go` `n` represents the number of already encountered lambda abstractions. -- On encountering a `lam`, we prepend a lambda to the resulting term and -- apply the continuation to a fresh variable represented as a number of encountered -- lambdas wrapped in `pure`. We also increase the lambdas counter. -- In the `go n (pure m)` case we know that some variable was substituted by `pure m`, -- where `m` was a number of encountered so far lambdas. -- And now the number of encountered lambdas is `n`. -- Thus, the resulting de Bruijn index is `n ∸ m ∸ 1`. -- Here are some reductions: -- `fromValue Iᵥ` -- `go 0 (lam λ x -> x)` -- `ƛ (go 1 (pure 0))` -- `ƛ var vz` -- `fromValue Kᵥ` -- `go 0 (lam λ x -> lam λ y -> x)` -- `ƛ (go 1 (lam λ y -> pure 0))` -- `ƛ ƛ (go 2 (pure 0))` -- `ƛ ƛ var 1` Sᵥ≈S : fromValue Sᵥ ≡ S Sᵥ≈S = refl -- We'll need some unsafe silliness in order to define the `toValue` function. module _ where postulate undefined : ∀ {α} {A : Set α} -> A unsafeLookup : ∀ {α} {A : Set α} -> ℕ -> List A -> A unsafeLookup _ [] = undefined unsafeLookup 0 (x ∷ xs) = x unsafeLookup (suc n) (x ∷ xs) = unsafeLookup n xs toValue : Term -> VTerm toValue t = go [] t where go : ∀ {A} -> List (Value A) -> Term -> Value A go ρ (var n) = unsafeLookup n ρ go ρ (ƛ b ) = lam (λ x -> go (x ∷ ρ) b) go ρ (f · x) = go ρ f · go ρ x -- In `go` `ρ` is an environment -- a list of already introduced bindings. -- When encounter a `ƛ`, we prepend `lam` to the result, bind a variable -- and add this binding to the environment. Later, in the `var n` case we take the nth binding. -- Here are some reductions: -- `toValue I` -- `go [] (ƛ var 0)` -- `lam λ x -> go (x ∷ []) (var 0)` -- `lam λ x -> x` -- `toValue K` -- `go [] (ƛ ƛ var 1)` -- `lam λ x -> go (x ∷ []) (ƛ var 1)` -- `lam λ x -> lam λ y -> go (y ∷ x ∷ []) (var 1)` -- `lam λ x -> lam λ y -> x` S≈Sᵥ : ∀ {A} -> toValue S {A} ≡ Sᵥ S≈Sᵥ = refl -- Finally, the normalization function: norm′ : Term -> Term norm′ t = fromValue (normValue (toValue t)) SKK≈I′ : norm′ (S · K · K) ≡ I SKK≈I′ = refl -- `norm` is usually defined in terms of `readback` (or `quote`) and `eval`. -- `readback` is the same thing as `fromValue` readback : VTerm -> Term readback = fromValue -- and `eval` is like `normValue ∘ toValue`, but in one phase: eval : Term -> VTerm eval t = go [] t where go : ∀ {A} -> List (Value A) -> Term -> Value A go ρ (var n) = unsafeLookup n ρ go ρ (ƛ b ) = lam (λ x -> go (x ∷ ρ) b) go ρ (f · x) = go ρ f ∙ go ρ x -- The only difference between toValue` and `eval` is that function application -- β-reduces in the latter case, i.e. it's `go ρ f ∙ go ρ x` instead of `go ρ f · go ρ x`. norm : Term -> Term norm = readback ∘ eval SKK≈I : norm (S · K · K) ≡ I SKK≈I = refl S≈S : norm S ≡ S S≈S = refl module NewValues where open Readback using (Term; var; ƛ_; _·_; var⁺; unsafeLookup; I; K; S) public infixl 6 _·⁺_ _∙_ -- Our next step is to remove `_·_` from `Value`s and define normalization within this setting. {-# NO_POSITIVITY_CHECK #-} data Value (A : Set) : Set where pure : A -> Value A lam : (Value A -> Value A) -> Value A -- With the de Bruijn indices approach a variable can be denoted by different indices in a term, -- depending on how many variables were introduced after it. -- E.g. consider the `ω` combinator: `ƛ var 0 · var 0`. We can η-expand the last `var 0` and get -- `ƛ var 0 · (ƛ var 1 · var 0)`. The variable introduced by the first lambda is denoted -- first as `var 0` and then as `var 1`. -- It's a problem, because we want to fill a hole in a term `lam λ x -> ...` -- by passing something to the continuation, so `x` will everywhere be replaced by -- some expression. But de Bruijn indices are context dependent, so it's not possible to -- do that with them. -- There is no such problem with de Bruijn levels (e.g. the `S` combinator with -- de Bruijn levels is represented as `ƛ ƛ ƛ var 0 · var 2 · (var 1 · var 2)`). -- The `ω` combinator with de Bruijn levels is the same `ƛ var 0 · var 0`, -- but if we now η-expand the last `var 0`, we'll get `ƛ var 0 · (ƛ var 0 · var 1)`. -- The variable introduced by the first lambda is `var 0` everywhere. -- The solution is to emulate de Bruijn levels using the liftable terms approach -- (the terminology is due to [3]). Instead of instantiating `x` in `lam λ x -> ...` with -- a term, we'll instantiate it with a function that returns a term. Lately, the function -- will be applied to the number of encountered lambdas and will compute the term -- accordingly to this context. -- Liftable terms are Term⁺ : Set Term⁺ = ℕ -> Term -- We have already seen liftable variables: -- var⁺ : ℕ -> ℕ -> Term -- var⁺ m n = var (n ∸ m ∸ 1) -- Function application for liftable terms is straightforward: _·⁺_ : Term⁺ -> Term⁺ -> Term⁺ (f ·⁺ x) n = f n · x n -- As promised terms in the model are VTerm : Set VTerm = Value Term⁺ -- `readback` receives a `VTerm` and a number of already encountered lambdas. readback : VTerm -> Term⁺ readback (pure t) n = t n readback (lam k) n = ƛ (readback (k (pure (var⁺ n))) (suc n)) -- On encountering `lam λ x -> ...` `x` gets instantiated to `pure (var⁺ n)` -- -- recall that `var⁺ n m` returns the de Bruijn index of a variable introduced by `n`th lambda -- in a context with `m` lambdas. We also increase the lambdas counter by `suc n`. -- Function application for values is _∙_ : VTerm -> VTerm -> VTerm pure f ∙ x = pure (f ·⁺ readback x) lam k ∙ x = k x -- The `lam` case is the same. `_∙_` is used such that in the `pure` case -- `f` is always a neutral term and hence `x` can safely be readback -- it won't participate -- in β-reductions. So this is how we construct terms: we collect function applications -- under the `pure` wrapper. -- `eval` is the same as before. eval : Term -> VTerm eval = go [] where go : List VTerm -> Term -> VTerm go ρ (var n) = unsafeLookup n ρ go ρ (ƛ b ) = lam (λ x -> go (x ∷ ρ) b) go ρ (f · x) = go ρ f ∙ go ρ x norm : Term -> Term norm t = readback (eval t) 0 -- Let's now look at an example. ηω : Term ηω = ƛ var 0 · (ƛ var 1 · var 0) -- `norm ηω` reduces like this: -- expand all definitions: -- `norm ηω` -- `readback (eval ηω) 0` -- `readback (lam λ x -> x ∙ (lam λ y -> x ∙ y)) 0` -- `readback` consumes `lam`: -- `ƛ readback (pure (var⁺ 0) ∙ (lam λ y -> pure (var⁺ 0) ∙ y)) 1` -- `_∙_` fires: -- `ƛ readback (pure (var⁺ 0 ·⁺ readback (lam λ y -> pure (var⁺ 0) ∙ y))) 1` -- `readback` consumes `pure`: -- `ƛ (var⁺ 0 ·⁺ readback (lam λ y -> pure (var⁺ 0) ∙ y)) 1` -- `_·⁺_` fires: -- `ƛ var⁺ 0 1 · readback (lam λ y -> pure (var⁺ 0) ∙ y)) 1` -- `var⁺ 0 1` reduces: -- `ƛ var 0 · readback (lam λ y -> pure (var⁺ 0) ∙ y)) 1` -- `readback` consumes `lam`: -- `ƛ var 0 · (ƛ readback (pure (var⁺ 0) ∙ pure (var⁺ 1)) 2)` -- `_∙_` fires: -- `ƛ var 0 · (ƛ readback (pure (var⁺ 0 ·⁺ readback (pure (var⁺ 1)))) 2)` -- `readback`s consume `pure`s: -- `ƛ var 0 · (ƛ (var⁺ 0 ·⁺ var⁺ 1) 2)` -- `_·⁺_` fires -- `ƛ var 0 · (ƛ var⁺ 0 2 · var⁺ 1 2)` -- `var⁺` reduce: -- `ƛ var 0 · (ƛ var 1 · var 0)` -- and we're done. -- The key point is that the number of encountered lambdas is traced over the whole computation. -- `_·⁺_` "distributes" it, `var⁺` and `readback` consume it. `_∙_` "resumes" `readback`: -- `pure f ∙ x = pure (f ·⁺ readback x)` -- and it always starts at the point where the previous `readback` stopped -- (i.e. with the same amount of encountered lambdas), where "stopping" is -- `readback (pure t) n = t n` -- This also explains why we can't simply use de Bruijn levels -- it's anyway necessarily to -- trace a number of encountered lambdas to be able to resume `readback`. module Reify&Reflect where open NewValues hiding (readback; _∙_; eval; norm) infixr 6 _⇒_ -- There is another standard variant of Normalization by Evaluation: -- in terms of `reify` and `reflect`. It's type-directed, so we'll need some types for it: data Type : Set where ⋆ : Type _⇒_ : Type -> Type -> Type postulate undefined : ∀ {α} {A : Set α} -> A -- Function application that β-reduces remains the same for the `lam` case -- and becomes undefined otherwise. _∙_ : ∀ {A} -> Value A -> Value A -> Value A pure _ ∙ x = undefined lam k ∙ x = k x -- `eval` is the same. eval : ∀ {A} -> Term -> Value A eval t = go [] t where go : ∀ {A} -> List (Value A) -> Term -> Value A go ρ (var n) = unsafeLookup n ρ go ρ (ƛ b ) = lam (λ x -> go (x ∷ ρ) b) go ρ (f · x) = go ρ f ∙ go ρ x -- The core of the approach: mutual reify : Type -> VTerm -> Term⁺ reify ⋆ (pure t) n = t n reify (σ ⇒ τ) (lam k) n = ƛ (reify τ (k (rvar⁺ σ n)) (suc n)) reify _ _ n = undefined reflect : Type -> Term⁺ -> VTerm reflect ⋆ t = pure t reflect (σ ⇒ τ) f = lam λ x -> reflect τ (f ·⁺ reify σ x) rvar⁺ : Type -> ℕ -> VTerm rvar⁺ σ n = reflect σ (var⁺ n) norm : Type -> Term -> Term norm σ t = reify σ (eval t) 0 -- Compare `reify` to `readback`: -- readback : VTerm -> Term⁺ -- readback (pure t) n = t n -- readback (lam k) n = ƛ (readback (k (pure (var⁺ n))) (suc n)) -- They are very similar except that in `readback` `k` receives `pure (var⁺ n)` -- and in `reify` `k` receives `reflect σ (var⁺ n)` (after unfolding `rvar⁺ σ n`). -- `reify` is also type-directed, hence it performs full η-expansion. -- So what's the difference between `pure (var⁺ n)` and `reflect σ (var⁺ n)`? -- `reflect` performs η-expansion of values. -- Recall how `_∙_` was defined in the previous section: -- _∙_ : VTerm -> VTerm -> VTerm -- pure f ∙ x = pure (f ·⁺ readback x) -- lam k ∙ x = k x -- With this definition `pure (var⁺ n) ∙ x` reduces to `pure (var⁺ n ·⁺ readback x)`. -- `reflect` allows to reduce the expression in the same way while leaving `_∙_` undefined -- in the `pure` case. Instead, both the tasks of performing β-reductions and collecting -- function applications under the `pure` wrapper we solve using just `lam`. -- Consider `rvar⁺ (⋆ ⇒ ⋆) n ∙ x`. It reduces to `(lam λ y -> pure (var⁺ n ·⁺ reify σ y)) ∙ x` -- and further to `pure (var⁺ n ·⁺ reify σ x)`. Just the same expression as before -- (keep in mind that `reify` is a new version of `readback`). -- That's basically it. The `reify&reflect` approach is just the `readback` approach -- after some reshuffling. module Typed where -- The next step is to define normalization for Church-like typed terms. -- It's straightforward to adapt the liftable terms approach to typed setting -- (though, it still costs a `postulate`). An implementation can be found here: -- https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda -- Note that this approach allows to get a first-order representation -- of a pure Agda lambda term, see the examples at the end of the file. -- The implementation is in terms of `reify` and `reflect`. It's adapted from [4]. -- But the actual magic happens when you interpret function space of the target language -- in a Kripke-like fashion and thus incorporate weakening into semantics. -- I'm not very comfortable with this approach, so I won't describe it either, but -- a minimal implementation (in terms of `readback`) can be found here: -- https://github.com/effectfully/random-stuff/blob/master/Normalization/Readback.agda module References where -- [1] "Reverse Engineering Machines with the Yoneda Lemma" -- Dan Piponi -- http://blog.sigfpe.com/2006/11/yoneda-lemma.html -- [2] http://stackoverflow.com/a/32146054/3237465 -- [3] "Normalization by Evaluation for Martin-Löf Type Theory with One Universe" -- Andreas Abel, Klaus Aehlig, Peter Dybjer -- http://www.cse.chalmers.se/~peterd/papers/NbeMLTT.pdf -- [4] "Normalization by Evaluation, Dependent Types and Impredicativity" -- Andreas Abel -- http://www.cse.chalmers.se/~abela/habil.pdf

## Thursday, 25 February 2016

### Normalization by Evaluation

## Saturday, 20 February 2016

### Simple generic programming.

-- When I was reading about descriptions ([1]), I was wondering whether -- there is an encoding that is not that powerful, but simple, straightforward -- and allows to encode a vast amount of data types among with their elimination principles -- (the containers approach ([2]) doesn't allow this in an intensional type theory [3]). -- I'll describe such encoding. open import Level renaming (zero to lzero; suc to lsuc) open import Function open import Relation.Binary.PropositionalEquality open import Data.Nat.Base renaming (_⊔_ to _⊔ℕ_) open import Data.Product open import Data.List.Base infixr 5 _∷₁_ -- `List₁ B xs` contains a `B x` for each `x` in `xs`. -- It's the same `All` from `Data.List.All`, but lies in `Set β` rather than `Set (α ⊔ β)`. data List₁ {α β} {A : Set α} (B : A -> Set β) : List A -> Set β where []₁ : List₁ B [] _∷₁_ : ∀ {x xs} -> B x -> List₁ B xs -> List₁ B (x ∷ xs) -- And here is the encoding. Over : ∀ {ι} -> Set ι -> ∀ α -> Set (ι ⊔ lsuc α) Over I α = List I -> I -> Set α record Rose {ι α} {I : Set ι} (F : Over I α) j : Set (ι ⊔ α) where inductive constructor node field {is} : List I cons : F is j childs : List₁ (Rose F) is -- `Over` describes all possible constructors of a data type and -- `Rose` ties the knot and connects these constructors together. -- `Rose` is able to express inductive families and that's why there is the `I` -- -- it's the type of the indices of a data type. -- `Over` contains all information about a data type being described -- except for inductive occurrences, which are reflected to the type level -- by storing their indices in `List I`. The final `I` in -- Over I α = List I -> I -> Set α -- is for the index that a constructor produces. -- Here is how it looks for vectors: module Vec where data VecF {α} (A : Set α) : Over ℕ α where -- The first constructor for `Vec` (`[]ᵥ`) doesn't contain any data -- and it produces the index `0`. Nil : VecF A [] 0 -- The second constructor for `Vec` (`_∷ᵥ_`) contains an `A` and -- an inductive occurrence of `Vec`. It produces the index `suc n` -- where `n` is the index of the inductive occurrence. -- Hence we put `n` into the list of indices of inductive occurrences and return `suc n`. Cons : ∀ {n} -> A -> VecF A (n ∷ []) (suc n) -- `Vec` then is Vec : ∀ {α} -> Set α -> ℕ -> Set α Vec A n = Rose (VecF A) n -- Let's look again at the definition of `Rose`: -- record Rose {ι α} {I : Set ι} (F : Over I α) j : Set (ι ⊔ α) where -- inductive -- constructor node -- field -- {is} : List I -- cons : F is j -- childs : List₁ (Rose F) is -- `j` is an index of an inhabitant of a data type. -- `is` is a list of indices of inductive occurrences. -- `cons` is a constructor of this data type. -- `childs` is a list of `Rose F i` for each `i` in `is`, -- i.e. a list that actually contains inductive occurrences (finally). -- Recall the definition of `Cons`: -- `Cons : ∀ {n} -> A -> VecF A (n ∷ []) (suc n)` -- When we write `node (Cons x)` `is` gets unified with `_n ∷ []` and -- `j` gets unified with `suc _n` for a fresh meta `_n`. -- Thus, `childs` has type `List₁ (Vec A) (_n ∷ [])`, -- i.e. there is exactly one child -- `Vec A n`. -- So here are the constructors: -- []ᵥ : ∀ {α} {A : Set α} -> Vec A 0 -- []ᵥ = node Nil []₁ -- _∷ᵥ_ : ∀ {n α} {A : Set α} -> A -> Vec A n -> Vec A (suc n) -- x ∷ᵥ xs = node (Cons x) (xs ∷₁ []₁) -- But for convenience we'll define them as pattern synonyms instead pattern []ᵥ = node Nil []₁ pattern _∷ᵥ_ x xs = node (Cons x) (xs ∷₁ []₁) -- And guess what, we have literally the same eliminator as for the usual `Vec`: elimVec : ∀ {α π} {A : Set α} {n} -> (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) -- So we basically don't need it -- we can use pattern matching directly, e.g.: vmap : ∀ {n α β} {A : Set α} {B : Set β} -> (A -> B) -> Vec A n -> Vec B n vmap f []ᵥ = []ᵥ vmap f (x ∷ᵥ xs) = f x ∷ᵥ vmap f xs vhead : ∀ {n α} {A : Set α} -> Vec A (suc n) -> A vhead (x ∷ᵥ xs) = x module AnEliminator where -- We can of course define an eliminator of `Rose`. -- But let's define an eliminator for something simpler first. data Tree {α} (A : Set α) : Set α where branch : A -> List (Tree A) -> Tree A -- An eliminator is an induction principle and an induction hypothesis -- sounds like "`P` holds, if it holds at every inductive position". -- To say "`P` holds for a list `xs` of inductive occurrences" we write `List₁ P xs`. -- Here is the eliminator: elimTree : ∀ {α π} {A : Set α} -> (P : Tree A -> Set π) -> (∀ {ts} x -> List₁ P ts -> P (branch x ts)) -> ∀ t -> P t elimTree P f (branch x ts) = f x (elimTrees ts) where elimTrees : ∀ ts -> List₁ P ts elimTrees [] = []₁ elimTrees (t ∷ ts) = elimTree P f t ∷₁ elimTrees ts -- `Rose` is basically the same thing as `Tree`, but there is `List₁` instead of `List`. -- All we need is to define `List₂` over `List₁` in the same manner as `List₁` over `List` before. data List₂ {α β γ} {A : Set α} {B : A -> Set β} (C : ∀ {x} -> B x -> Set γ) : ∀ {xs} -> List₁ B xs -> Set γ where []₂ : List₂ C []₁ _∷₂_ : ∀ {x xs} {y : B x} {ys : List₁ B xs} -> C y -> List₂ C ys -> List₂ C (y ∷₁ ys) lmap₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : ∀ {x} -> B x -> Set γ} {xs} -> (∀ {x} -> (y : B x) -> C y) -> (ys : List₁ B xs) -> List₂ C ys lmap₂ g []₁ = []₂ lmap₂ g (y ∷₁ ys) = g y ∷₂ lmap₂ g ys {-# TERMINATING #-} elimRose : ∀ {ι α π} {I : Set ι} {F : Over I α} {j} -> (P : ∀ {j} -> Rose F j -> Set π) -> (∀ {is j cs} -> (c : F is j) -> List₂ P cs -> P (node c cs)) -> (r : Rose F j) -> P r elimRose P f (node c cs) = f c (lmap₂ (elimRose P f) cs) -- We could get rid of the `{-# TERMINATING #-}` pragma by inlining `lmap₂' and -- defining `elimRose` mutually with `elimRoses` as in the case of `Tree`, but I hate this. -- As an example, let's define an eliminator for `Vec` in terms of `elimRose`. open Vec elimVec′ : ∀ {α π} {A : Set α} {n} -> (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′ {A = A} P f z = elimRose P h where h : ∀ {is j cs} -> (c : VecF A is j) -> List₂ P cs -> P (node c cs) h Nil []₂ = z h (Cons x) (xs ∷₂ []₂) = f x xs -- Not super nice, but works. -- A recursor is similar: unmap₁ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {xs} -> (∀ {x} -> B x -> C) -> List₁ B xs -> List C unmap₁ g []₁ = [] unmap₁ g (y ∷₁ ys) = g y ∷ unmap₁ g ys {-# TERMINATING #-} foldRose : ∀ {ι α π} {I : Set ι} {F : Over I α} {j} {P : Set π} -> (∀ {is j} -> F is j -> List P -> P) -> Rose F j -> P foldRose f (node c cs) = f c (unmap₁ (foldRose f) cs) -- We can define a generic `depth` function that returns the depth of any `Rose`. depth : ∀ {ι α} {I : Set ι} {F : Over I α} {j} -> Rose F j -> ℕ depth = foldRose (λ _ -> foldr (_⊔ℕ_ ∘ suc) 0) -- A simple test: vec-depth : ∀ {n α} {A : Set α} -> (xs : Vec A n) -> depth xs ≡ n vec-depth []ᵥ = refl vec-depth (x ∷ᵥ xs) = cong suc (vec-depth xs) -- One restriction is that we can't describe data types in which an inductive position occurs -- to the right of the arrow in a parameter of a constructor (like e.g. in `W`). -- This is fixable: I wrote a library that deals with Observational Type Theory, -- `W` is expressible there and has the usual induction principle. -- Here it is: https://github.com/effectfully/OTT/blob/master/Data/W.agda -- An extended example: simply typed lambda calculus. module STLC where infixr 6 _⇒_ infixl 5 _▻_ infix 3 _∈_ _⊢_ infixr 4 vs_ infixr 0 ƛ_ infixl 6 _·_ data Type : Set where nat : Type _⇒_ : Type -> Type -> Type ⟦_⟧ : Type -> Set ⟦ nat ⟧ = ℕ ⟦ σ ⇒ τ ⟧ = ⟦ σ ⟧ -> ⟦ τ ⟧ data Con : Set where ε : Con _▻_ : Con -> Type -> Con data _∈_ σ : Con -> Set where vz : ∀ {Γ} -> σ ∈ Γ ▻ σ vs_ : ∀ {Γ τ} -> σ ∈ Γ -> σ ∈ Γ ▻ τ data Env : Con -> Set where ∅ : Env ε _▷_ : ∀ {Γ σ} -> Env Γ -> ⟦ σ ⟧ -> Env (Γ ▻ σ) lookupᵉ : ∀ {Γ σ} -> σ ∈ Γ -> Env Γ -> ⟦ σ ⟧ lookupᵉ vz (ρ ▷ x) = x lookupᵉ (vs v) (ρ ▷ x) = lookupᵉ v ρ data TermF : Over (Con × Type) lzero where Pure : ∀ {Γ σ } -> ⟦ σ ⟧ -> TermF [] (Γ , σ ) Var : ∀ {Γ σ } -> σ ∈ Γ -> TermF [] (Γ , σ ) Lam : ∀ {Γ σ τ} -> TermF ((Γ ▻ σ , τ) ∷ []) (Γ , σ ⇒ τ) App : ∀ {Γ σ τ} -> TermF ((Γ , σ ⇒ τ) ∷ (Γ , σ) ∷ []) (Γ , τ ) Z : ∀ {Γ } -> TermF [] (Γ , nat ) S : ∀ {Γ } -> TermF ((Γ , nat) ∷ []) (Γ , nat ) Fold : ∀ {Γ σ } -> TermF ((Γ , σ ⇒ σ) ∷ (Γ , σ) ∷ (Γ , nat) ∷ []) (Γ , σ ) _⊢_ : Con -> Type -> Set Γ ⊢ σ = Rose TermF (Γ , σ) Term⁺ : Type -> Set Term⁺ σ = ∀ {Γ} -> Γ ⊢ σ Term⁽⁾ : Type -> Set Term⁽⁾ σ = ε ⊢ σ pattern pure x = node (Pure x) []₁ pattern var v = node (Var v) []₁ pattern ƛ_ b = node Lam (b ∷₁ []₁) pattern _·_ f x = node App (f ∷₁ x ∷₁ []₁) pattern z = node Z []₁ pattern s n = node S (n ∷₁ []₁) pattern tfold f x n = node Fold (f ∷₁ x ∷₁ n ∷₁ []₁) ⟦_⟧ᵥ : ∀ {Γ σ} -> Γ ⊢ σ -> Env Γ -> ⟦ σ ⟧ ⟦ pure x ⟧ᵥ ρ = x ⟦ var v ⟧ᵥ ρ = lookupᵉ v ρ ⟦ ƛ b ⟧ᵥ ρ = λ x -> ⟦ b ⟧ᵥ (ρ ▷ x) ⟦ f · x ⟧ᵥ ρ = ⟦ f ⟧ᵥ ρ (⟦ x ⟧ᵥ ρ) ⟦ z ⟧ᵥ ρ = 0 ⟦ s n ⟧ᵥ ρ = suc (⟦ n ⟧ᵥ ρ) ⟦ tfold f x n ⟧ᵥ ρ = fold (⟦ x ⟧ᵥ ρ) (⟦ f ⟧ᵥ ρ) (⟦ n ⟧ᵥ ρ) eval : ∀ {σ} -> Term⁽⁾ σ -> ⟦ σ ⟧ eval t = ⟦ t ⟧ᵥ ∅ A : ∀ {σ τ} -> Term⁺ ((σ ⇒ τ) ⇒ σ ⇒ τ) A = ƛ ƛ var (vs vz) · var vz test : ∀ {σ τ} -> eval (A {σ} {τ}) ≡ _$_ test = refl module References where -- [1] "The Gentle Art of Levitation" -- James Chapman, Pierre-Evariste Dagand, Conor McBride, Peter Morris -- http://jmchapman.github.io/papers/levitation.pdf -- [2] "Indexed Containers" -- Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, Peter Morris -- http://www.cs.nott.ac.uk/~psztxa/publ/jcont.pdf -- [3] "W-types: good news and bad news" -- Conor McBride -- http://mazzo.li/epilogue/index.html%3Fp=324.html

Subscribe to:
Posts (Atom)