<div dir="ltr"><div>Many thanks to Nils and Roman.</div><div><br></div><div>Attached find an implementation along the lines sketched by Roman;</div><div>I found it after I sent my request and before Roman sent his helpful</div><div>reply.</div><div><br></div><div>One thing I note, in both Roman's code and mine, is that the code to</div><div>decide whether two contexts are equal is lengthy (_≟T_ and _≟_,</div><div>below). Is there a better way to do it? Does Agda offer an</div><div>equivalent of Haskell's derivable for equality?</div><div><br></div><div>Cheers, -- P</div><div><br></div><div><br></div><div>## Imports</div><div><br></div><div>\begin{code}</div><div>open import Relation.Binary.PropositionalEquality using (_≡_; refl)</div><div>open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)</div><div>open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)</div><div>open import Data.Sum using (_⊎_; inj₁; inj₂)</div><div>open import Relation.Nullary using (¬_; Dec; yes; no)</div><div>open import Relation.Nullary.Decidable using (map)</div><div>open import Relation.Nullary.Negation using (contraposition)</div><div>open import Relation.Nullary.Product using (_×-dec_)</div><div>open import Data.Unit using (⊤; tt)</div><div>open import Data.Empty using (⊥; ⊥-elim)</div><div>open import Function using (_∘_)</div><div>open import Function.Equivalence using (_⇔_; equivalence)</div><div>\end{code}</div><div><br></div><div>## Typed DeBruijn</div><div><br></div><div>\begin{code}</div><div>infixr 5 _⇒_</div><div><br></div><div>data Type : Set where</div><div> o : Type</div><div> _⇒_ : Type → Type → Type</div><div><br></div><div>data Env : Set where</div><div> ε : Env</div><div> _,_ : Env → Type → Env</div><div><br></div><div>data Var : Env → Type → Set where</div><div> Z : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A</div><div> S : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B</div><div><br></div><div>data Exp : Env → Type → Set where</div><div> var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A</div><div> abs : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ (A ⇒ B)</div><div> app : ∀ {Γ : Env} {A B : Type} → Exp Γ (A ⇒ B) → Exp Γ A → Exp Γ B</div><div>\end{code}</div><div><br></div><div>## Untyped DeBruijn</div><div><br></div><div>\begin{code}</div><div>data DB : Set where</div><div> var : ℕ → DB</div><div> abs : DB → DB</div><div> app : DB → DB → DB</div><div>\end{code}</div><div><br></div><div># PHOAS</div><div><br></div><div>\begin{code}</div><div>data PH (X : Type → Set) : Type → Set where</div><div> var : ∀ {A : Type} → X A → PH X A</div><div> abs : ∀ {A B : Type} → (X A → PH X B) → PH X (A ⇒ B)</div><div> app : ∀ {A B : Type} → PH X (A ⇒ B) → PH X A → PH X B</div><div>\end{code}</div><div><br></div><div># Convert PHOAS to DB</div><div><br></div><div>\begin{code}</div><div>PH→DB : ∀ {A} → (∀ {X} → PH X A) → DB</div><div>PH→DB M = h M 0</div><div> where</div><div> K : Type → Set</div><div> K A = ℕ</div><div><br></div><div> h : ∀ {A} → PH K A → ℕ → DB</div><div> h (var k) j = var (j ∸ (k + 1))</div><div> h (abs N) j = abs (h (N j) (j + 1))</div><div> h (app L M) j = app (h L j) (h M j)</div><div>\end{code}</div><div><br></div><div># Test examples</div><div><br></div><div>\begin{code}</div><div>Church : Type</div><div>Church = (o ⇒ o) ⇒ o ⇒ o</div><div><br></div><div>twoExp : Exp ε Church</div><div>twoExp = (abs (abs (app (var (S Z)) (app (var (S Z)) (var Z)))))</div><div><br></div><div>twoPH : ∀ {X} → PH X Church</div><div>twoPH = (abs (λ f → (abs (λ x → (app (var f) (app (var f) (var x)))))))</div><div><br></div><div>twoDB : DB</div><div>twoDB = (abs (abs (app (var 1) (app (var 1) (var 0)))))</div><div><br></div><div>ex : PH→DB twoPH ≡ twoDB</div><div>ex = refl</div><div>\end{code}</div><div><br></div><div>## Decide whether environments and types are equal</div><div><br></div><div>\begin{code}</div><div>_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)</div><div>o ≟T o = yes refl</div><div>o ≟T (A′ ⇒ B′) = no (λ())</div><div>(A ⇒ B) ≟T o = no (λ())</div><div>(A ⇒ B) ≟T (A′ ⇒ B′) = map (equivalence obv1 obv2) ((A ≟T A′) ×-dec (B ≟T B′))</div><div> where</div><div> obv1 : ∀ {A B A′ B′ : Type} → (A ≡ A′) × (B ≡ B′) → A ⇒ B ≡ A′ ⇒ B′</div><div> obv1 ⟨ refl , refl ⟩ = refl</div><div> obv2 : ∀ {A B A′ B′ : Type} → A ⇒ B ≡ A′ ⇒ B′ → (A ≡ A′) × (B ≡ B′)</div><div> obv2 refl = ⟨ refl , refl ⟩</div><div><br></div><div>_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)</div><div>ε ≟ ε = yes refl</div><div>ε ≟ (Γ , A) = no (λ())</div><div>(Γ , A) ≟ ε = no (λ())</div><div>(Γ , A) ≟ (Δ , B) = map (equivalence obv1 obv2) ((Γ ≟ Δ) ×-dec (A ≟T B))</div><div> where</div><div> obv1 : ∀ {Γ Δ A B} → (Γ ≡ Δ) × (A ≡ B) → (Γ , A) ≡ (Δ , B)</div><div> obv1 ⟨ refl , refl ⟩ = refl</div><div> obv2 : ∀ {Γ Δ A B} → (Γ , A) ≡ (Δ , B) → (Γ ≡ Δ) × (A ≡ B)</div><div> obv2 refl = ⟨ refl , refl ⟩</div><div>\end{code}</div><div><br></div><div><br></div><div>## Convert Phoas to Exp</div><div><br></div><div>\begin{code}</div><div>compare : ∀ (A : Type) (Γ Δ : Env) → Var Δ A</div><div>compare A Γ Δ with (Γ , A) ≟ Δ</div><div>compare A Γ Δ | yes refl = Z</div><div>compare A Γ (Δ , B) | no _ = S (compare A Γ Δ)</div><div>compare A Γ ε | no _ = impossible</div><div> where</div><div> postulate</div><div> impossible : ∀ {A : Set} → A</div><div><br></div><div>PH→Exp : ∀ {A : Type} → (∀ {X} → PH X A) → Exp ε A</div><div>PH→Exp M = h M ε</div><div> where</div><div> K : Type → Set</div><div> K A = Env</div><div><br></div><div> h : ∀ {A} → PH K A → (Δ : Env) → Exp Δ A</div><div> h {A} (var Γ) Δ = var (compare A Γ Δ)</div><div> h {A ⇒ B} (abs N) Δ = abs (h (N Δ) (Δ , A))</div><div> h (app L M) Δ = app (h L Δ) (h M Δ)</div><div><br></div><div>ex₁ : PH→Exp twoPH ≡ twoExp</div><div>ex₁ = refl</div><div>\end{code}</div><div><br></div><div>## When one environment extends another</div><div><br></div><div>We could get rid of the use of `impossible` above if we could prove</div><div>that `Extends (Γ , A) Δ` in the `(var Γ)` case of the definition of `h`.</div><div><br></div><div>\begin{code}</div><div>data Extends : (Γ : Env) → (Δ : Env) → Set where</div><div> Z : ∀ {Γ : Env} → Extends Γ Γ</div><div> S : ∀ {A : Type} {Γ Δ : Env} → Extends Γ Δ → Extends Γ (Δ , A)</div><div><br></div><div>extract : ∀ {A : Type} {Γ Δ : Env} → Extends (Γ , A) Δ → Var Δ A</div><div>extract Z = Z</div><div>extract (S k) = S (extract k)</div><div>\end{code}</div><div><br></div><div><br></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 27 February 2018 at 22:07, Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You can easily get the PHOAS representation of a regular Agda lambda<br>
expression [1]. E.g.<br>
<br>
K : Term (⋆ ⇒ ⋆ ⇒ ⋆)<br>
K = ↓ const<br>
<br>
S : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)<br>
S = ↓ _ˢ_<br>
<br>
Here `↓` takes an Agda combinator, specializes all type variables as<br>
it desires and constructs the corresponding PHOAS term. The<br>
implementation is just a matter of a few lines.<br>
<br>
Constructing typed de Bruijn terms from metalanguage lambda terms is<br>
much harder. When you do normalisation by evaluation, you use some<br>
form of Kripke semantics in order to get an easy way to reify<br>
target-language terms back. But PHOAS representation is basically a<br>
shallow embedding of metalanguage terms which do not have the notions<br>
of weakening, future contexts and such, so things become quite more<br>
involved as witnessed by Adam Chlipala's elaborations Nils referred<br>
to.<br>
<br>
There is always a way to cheat, though. You can turn the PHOAS -><br>
untyped de Bruijn machinery into the PHOAS -> typed de Bruijn<br>
machinery by checking that future contexts indeed extend past contexts<br>
and throwing an error otherwise (which can't happed, because future<br>
contexts always extend past contexts, but it's a metatheorem). Not a<br>
type-theoretic way to do things, "but works". This is discussed in the<br>
Andreas Abel's habilitation thesis [2] under the heading "Liftable<br>
terms". I have an implementation of these ideas in Agda: [3]. Reifying<br>
regular Agda lambda terms costs one postulate with this approach.<br>
<br>
But I'm not a type theorist, so take it with a grain of salt.<br>
<br>
[1] <a href="https://github.com/effectfully/random-stuff/blob/master/Normalization/PHOAS.agda" rel="noreferrer" target="_blank">https://github.com/<wbr>effectfully/random-stuff/blob/<wbr>master/Normalization/PHOAS.<wbr>agda</a><br>
[2] <a href="http://www.cse.chalmers.se/~abela/habil.pdf" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~<wbr>abela/habil.pdf</a><br>
[3] <a href="https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda" rel="noreferrer" target="_blank">https://github.com/<wbr>effectfully/random-stuff/blob/<wbr>master/Normalization/Liftable.<wbr>agda</a><br>
<br>
</blockquote></div><br></div>