Philip Wadler

2018-02-27 13:26:52 UTC

The typed DeBruijn representation is well known, as are typed PHOAS

and untyped DeBruijn. It is easy to convert PHOAS to untyped

DeBruijn. Is it known how to convert PHOAS to typed DeBruijn?

Yours, -- P

## Imports

\begin{code}

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

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

\end{code}

## Typed DeBruijn

\begin{code}

infixr 4 _â_

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)

h (abs N) j = abs (h (N (j + 1)) (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}

. \ 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/

and untyped DeBruijn. It is easy to convert PHOAS to untyped

DeBruijn. Is it known how to convert PHOAS to typed DeBruijn?

Yours, -- P

## Imports

\begin{code}

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

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

\end{code}

## Typed DeBruijn

\begin{code}

infixr 4 _â_

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)

h (abs N) j = abs (h (N (j + 1)) (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}

. \ 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/