Many thanks to Nils and Roman.

Attached find an implementation along the lines sketched by Roman;

I found it after I sent my request and before Roman sent his helpful

reply.

One thing I note, in both Roman's code and mine, is that the code to

decide whether two contexts are equal is lengthy (_âT_ and _â_,

below). Is there a better way to do it? Does Agda offer an

equivalent of Haskell's derivable for equality?

Cheers, -- P

## Imports

\begin{code}

open import Relation.Binary.PropositionalEquality using (_â¡_; refl)

open import Data.Nat using (â; zero; suc; _+_; _âž_)

open import Data.Product using (_Ã_; projâ; projâ; â; â-syntax) renaming

(_,_ to âš_,_â©)

open import Data.Sum using (_â_; injâ; injâ)

open import Relation.Nullary using (Â¬_; Dec; yes; no)

open import Relation.Nullary.Decidable using (map)

open import Relation.Nullary.Negation using (contraposition)

open import Relation.Nullary.Product using (_Ã-dec_)

open import Data.Unit using (â€; tt)

open import Data.Empty using (â¥; â¥-elim)

open import Function using (_â_)

open import Function.Equivalence using (_â_; equivalence)

\end{code}

## Typed DeBruijn

\begin{code}

infixr 5 _â_

data Type : Set where

o : Type

_â_ : Type â Type â Type

data Env : Set where

Îµ : Env

_,_ : Env â Type â Env

data Var : Env â Type â Set where

Z : â {Î : Env} {A : Type} â Var (Î , A) A

S : â {Î : Env} {A B : Type} â Var Î B â Var (Î , A) B

data Exp : Env â Type â Set where

var : â {Î : Env} {A : Type} â Var Î A â Exp Î A

abs : â {Î : Env} {A B : Type} â Exp (Î , A) B â Exp Î (A â B)

app : â {Î : Env} {A B : Type} â Exp Î (A â B) â Exp Î A â Exp Î B

\end{code}

## Untyped DeBruijn

\begin{code}

data DB : Set where

var : â â DB

abs : DB â DB

app : DB â DB â DB

\end{code}

# PHOAS

\begin{code}

data PH (X : Type â Set) : Type â Set where

var : â {A : Type} â X A â PH X A

abs : â {A B : Type} â (X A â PH X B) â PH X (A â B)

app : â {A B : Type} â PH X (A â B) â PH X A â PH X B

\end{code}

# Convert PHOAS to DB

\begin{code}

PHâDB : â {A} â (â {X} â PH X A) â DB

PHâDB M = h M 0

where

K : Type â Set

K A = â

h : â {A} â PH K A â â â DB

h (var k) j = var (j âž (k + 1))

h (abs N) j = abs (h (N j) (j + 1))

h (app L M) j = app (h L j) (h M j)

\end{code}

# Test examples

\begin{code}

Church : Type

Church = (o â o) â o â o

twoExp : Exp Îµ Church

twoExp = (abs (abs (app (var (S Z)) (app (var (S Z)) (var Z)))))

twoPH : â {X} â PH X Church

twoPH = (abs (Î» f â (abs (Î» x â (app (var f) (app (var f) (var x)))))))

twoDB : DB

twoDB = (abs (abs (app (var 1) (app (var 1) (var 0)))))

ex : PHâDB twoPH â¡ twoDB

ex = refl

\end{code}

## Decide whether environments and types are equal

\begin{code}

_âT_ : â (A B : Type) â Dec (A â¡ B)

o âT o = yes refl

o âT (Aâ² â Bâ²) = no (Î»())

(A â B) âT o = no (Î»())

(A â B) âT (Aâ² â Bâ²) = map (equivalence obv1 obv2) ((A âT Aâ²) Ã-dec (B âT

Bâ²))

where

obv1 : â {A B Aâ² Bâ² : Type} â (A â¡ Aâ²) Ã (B â¡ Bâ²) â A â B â¡ Aâ² â Bâ²

obv1 âš refl , refl â© = refl

obv2 : â {A B Aâ² Bâ² : Type} â A â B â¡ Aâ² â Bâ² â (A â¡ Aâ²) Ã (B â¡ Bâ²)

obv2 refl = âš refl , refl â©

_â_ : â (Î Î : Env) â Dec (Î â¡ Î)

Îµ â Îµ = yes refl

Îµ â (Î , A) = no (Î»())

(Î , A) â Îµ = no (Î»())

(Î , A) â (Î , B) = map (equivalence obv1 obv2) ((Î â Î) Ã-dec (A âT B))

where

obv1 : â {Î Î A B} â (Î â¡ Î) Ã (A â¡ B) â (Î , A) â¡ (Î , B)

obv1 âš refl , refl â© = refl

obv2 : â {Î Î A B} â (Î , A) â¡ (Î , B) â (Î â¡ Î) Ã (A â¡ B)

obv2 refl = âš refl , refl â©

\end{code}

## Convert Phoas to Exp

\begin{code}

compare : â (A : Type) (Î Î : Env) â Var Î A

compare A Î Î with (Î , A) â Î

compare A Î Î | yes refl = Z

compare A Î (Î , B) | no _ = S (compare A Î Î)

compare A Î Îµ | no _ = impossible

where

postulate

impossible : â {A : Set} â A

PHâExp : â {A : Type} â (â {X} â PH X A) â Exp Îµ A

PHâExp M = h M Îµ

where

K : Type â Set

K A = Env

h : â {A} â PH K A â (Î : Env) â Exp Î A

h {A} (var Î) Î = var (compare A Î Î)

h {A â B} (abs N) Î = abs (h (N Î) (Î , A))

h (app L M) Î = app (h L Î) (h M Î)

exâ : PHâExp twoPH â¡ twoExp

exâ = refl

\end{code}

## When one environment extends another

We could get rid of the use of `impossible` above if we could prove

that `Extends (Î , A) Î` in the `(var Î)` case of the definition of `h`.

\begin{code}

data Extends : (Î : Env) â (Î : Env) â Set where

Z : â {Î : Env} â Extends Î Î

S : â {A : Type} {Î Î : Env} â Extends Î Î â Extends Î (Î , A)

extract : â {A : Type} {Î Î : Env} â Extends (Î , A) Î â Var Î A

extract Z = Z

extract (S k) = S (extract k)

\end{code}

. \ Philip Wadler, Professor of Theoretical Computer Science,

. /\ School of Informatics, University of Edinburgh

. / \ and Senior Research Fellow, IOHK

. http://homepages.inf.ed.ac.uk/wadler/

*Post by Roman*You can easily get the PHOAS representation of a regular Agda lambda

expression [1]. E.g.

K : Term (â â â â â)

K = â const

S : Term ((â â â â â) â (â â â) â â â â)

S = â _Ë¢_

Here `â` takes an Agda combinator, specializes all type variables as

it desires and constructs the corresponding PHOAS term. The

implementation is just a matter of a few lines.

Constructing typed de Bruijn terms from metalanguage lambda terms is

much harder. When you do normalisation by evaluation, you use some

form of Kripke semantics in order to get an easy way to reify

target-language terms back. But PHOAS representation is basically a

shallow embedding of metalanguage terms which do not have the notions

of weakening, future contexts and such, so things become quite more

involved as witnessed by Adam Chlipala's elaborations Nils referred

to.

There is always a way to cheat, though. You can turn the PHOAS ->

untyped de Bruijn machinery into the PHOAS -> typed de Bruijn

machinery by checking that future contexts indeed extend past contexts

and throwing an error otherwise (which can't happed, because future

contexts always extend past contexts, but it's a metatheorem). Not a

type-theoretic way to do things, "but works". This is discussed in the

Andreas Abel's habilitation thesis [2] under the heading "Liftable

terms". I have an implementation of these ideas in Agda: [3]. Reifying

regular Agda lambda terms costs one postulate with this approach.

But I'm not a type theorist, so take it with a grain of salt.

[1] https://github.com/effectfully/random-stuff/blob/

master/Normalization/PHOAS.agda

[2] http://www.cse.chalmers.se/~abela/habil.pdf

[3] https://github.com/effectfully/random-stuff/blob/

master/Normalization/Liftable.agda