<div dir="ltr"><div>The typed DeBruijn representation is well known, as are typed PHOAS</div><div>and untyped DeBruijn.  It is easy to convert PHOAS to untyped</div><div>DeBruijn.  Is it known how to convert PHOAS to typed DeBruijn?</div><div><br></div><div>Yours, -- 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>\end{code}</div><div><br></div><div>## Typed DeBruijn</div><div><br></div><div>\begin{code}</div><div>infixr 4 _⇒_</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)</div><div>  h (abs N) j    =  abs (h (N (j + 1)) (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><br></div><div><div class="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>
</div>