[Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn

[Philip Wadler]

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/

[Nils Anders Danielsson]

Post by Philip Wadler
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?

I haven't checked the details, but Adam Chlipala seems to discuss this topic:

http://adam.chlipala.net/cpdt/html/Intensional.html

[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

[Philip Wadler]

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

[Roman]

Agda doesn't have a built-in deriving machinery, but Agda has tactics
which can be used to implement it. Ulf's `agda-prelude` allows to
derive decidable equality [1]. The downside is that `agda-prelude` is
not compatible with the standard library. There are several instances
you can derive with this library, but there is no strongly typed
representation of data types, hence if you want to derive your own
instances, you'll need to roll out substitution, unification, de
Bruijn indices/levels shifting and other tools from scratch and deal
with weakly typed `Term`s which is inconvenient and error-prone.

I have a library [2] that is compatible with the standard one and
allows to derive decidable equality and has a typed data type
representation (based on The Gentle Art of Levitation) and even though
it's able to handle a vast amount of data types (universe
polymorphism, implicit and instance arguments, indices and parameters,
higher-order induction -- all of these are supported), there are
practical (you can't reflect mutually recursive data types) and
theoretical limitations (you can't reflect non-strictly-positive,
inductive-inductive data types and most notably there is no internal
notion of polarity like in the Indexed Functors approach [4]).
Deriving your own instances is complicated and requires knowledge of
internals of the library. Still inconvenient, but not as error-prone
as dealing with weakly typed `Term`s.

I'd say switch to `agda-prelude` and use it.

[1] https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
[2] https://github.com/effectfully/Generic
[3] https://pages.lip6.fr/Pierre-Evariste.Dagand/papers/levitation.pdf
[4] https://www.andres-loeh.de/IndexedFunctors/

[Ulf Norell]

The downside is that `agda-prelude` is not compatible with the standard
library.

These days agda-prelude is compatible with the standard library. The only
wrinkle
is that the deriving Eq functionality gives you an implementation of the
agda-prelude
Eq record, but converting it to the standard library equivalent should be
straight-forward.

In fact here's the code:

\begin{code}
-- These two imports are from agda-prelude (
https://github.com/UlfNorell/agda-prelude)
open import Tactic.Deriving.Eq using (deriveEq)
import Prelude

instance
unquoteDecl EqType = deriveEq EqType (quote Type)
unquoteDecl EqEnv = deriveEq EqEnv (quote Env)

⊥To⊥ : Prelude.⊥ → ⊥
⊥To⊥ ()

decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
decToDec (Prelude.yes x) = yes x
decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)

_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
A ≟T B = decToDec (A Prelude.== B)

_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
\end{code}

/ Ulf

[Philip Wadler]

That worked perfectly!!! Thank you, Ulf! Cheers, -- P

. \ 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 Ulf Norell

The downside is that `agda-prelude` is not compatible with the standard
library.

These days agda-prelude is compatible with the standard library. The only
wrinkle
is that the deriving Eq functionality gives you an implementation of the
agda-prelude
Eq record, but converting it to the standard library equivalent should be
straight-forward.
\begin{code}
-- These two imports are from agda-prelude (https://github.com/UlfNorell/
agda-prelude)
open import Tactic.Deriving.Eq using (deriveEq)
import Prelude
instance
unquoteDecl EqType = deriveEq EqType (quote Type)
unquoteDecl EqEnv = deriveEq EqEnv (quote Env)
⊥To⊥ : Prelude.⊥ → ⊥
⊥To⊥ ()
decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
decToDec (Prelude.yes x) = yes x
decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)
_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
A ≟T B = decToDec (A Prelude.== B)
_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
\end{code}
/ Ulf

[András Kovács]

Alternatively, we can postulate parametricity <http://lpaste.net/363029>
for PHOAS terms, and then the translation works without further cheating
(that's why it's "parametric", right?).

Post by Philip Wadler
That worked perfectly!!! Thank you, Ulf! Cheers, -- P
. \ 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 Ulf Norell

The downside is that `agda-prelude` is not compatible with the standard
library.

These days agda-prelude is compatible with the standard library. The only
wrinkle
is that the deriving Eq functionality gives you an implementation of the
agda-prelude
Eq record, but converting it to the standard library equivalent should be
straight-forward.
\begin{code}
-- These two imports are from agda-prelude (https://github.com/UlfNorell/
agda-prelude)
open import Tactic.Deriving.Eq using (deriveEq)
import Prelude
instance
unquoteDecl EqType = deriveEq EqType (quote Type)
unquoteDecl EqEnv = deriveEq EqEnv (quote Env)
⊥To⊥ : Prelude.⊥ → ⊥
⊥To⊥ ()
decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
decToDec (Prelude.yes x) = yes x
decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)
_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
A ≟T B = decToDec (A Prelude.== B)
_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
\end{code}
/ Ulf

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Andras, Thank you, that's very cool. It will take a while to work my head
around it! Yours, -- P

. \ 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 András Kovács
Alternatively, we can postulate parametricity <http://lpaste.net/363029>
for PHOAS terms, and then the translation works without further cheating
(that's why it's "parametric", right?).

Post by Philip Wadler
That worked perfectly!!! Thank you, Ulf! Cheers, -- P
. \ 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 Ulf Norell

The downside is that `agda-prelude` is not compatible with the standard
library.

These days agda-prelude is compatible with the standard library. The
only wrinkle
is that the deriving Eq functionality gives you an implementation of the
agda-prelude
Eq record, but converting it to the standard library equivalent should
be straight-forward.
\begin{code}
-- These two imports are from agda-prelude (
https://github.com/UlfNorell/agda-prelude)
open import Tactic.Deriving.Eq using (deriveEq)
import Prelude
instance
unquoteDecl EqType = deriveEq EqType (quote Type)
unquoteDecl EqEnv = deriveEq EqEnv (quote Env)
⊥To⊥ : Prelude.⊥ → ⊥
⊥To⊥ ()
decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
decToDec (Prelude.yes x) = yes x
decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)
_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
A ≟T B = decToDec (A Prelude.== B)
_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
\end{code}
/ Ulf

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Andras, Thank you very much for your note [1]. Your proof appears related
to the wf relation of Chlipala [2,3]. One difference is that yours is unary
whereas his is binary, so I would expect his is more powerful, or do you
think they have equal power? Yours, -- P

[1] http://lpaste.net/363029
[2] http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html#HigherOrder.Wf
[3] http://adam.chlipala.net/cpdt/html/Intensional.html

. \ 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 András Kovács
Alternatively, we can postulate parametricity <http://lpaste.net/363029>
for PHOAS terms, and then the translation works without further cheating
(that's why it's "parametric", right?).

Post by Philip Wadler
That worked perfectly!!! Thank you, Ulf! Cheers, -- P
. \ 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 Ulf Norell

The downside is that `agda-prelude` is not compatible with the standard
library.

These days agda-prelude is compatible with the standard library. The
only wrinkle
is that the deriving Eq functionality gives you an implementation of the
agda-prelude
Eq record, but converting it to the standard library equivalent should
be straight-forward.
\begin{code}
-- These two imports are from agda-prelude (
https://github.com/UlfNorell/agda-prelude)
open import Tactic.Deriving.Eq using (deriveEq)
import Prelude
instance
unquoteDecl EqType = deriveEq EqType (quote Type)
unquoteDecl EqEnv = deriveEq EqEnv (quote Env)
⊥To⊥ : Prelude.⊥ → ⊥
⊥To⊥ ()
decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
decToDec (Prelude.yes x) = yes x
decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)
_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
A ≟T B = decToDec (A Prelude.== B)
_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
\end{code}
/ Ulf

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda