DeBruijn-agda-list-4 converts Typed to PHOAS
This commit is contained in:
wadler
parent
86f1ea295e
commit
a8d6729e62
2 changed files with 234 additions and 1 deletions
233
src/extra/DeBruijn-agda-list-4.lagda
Normal file
233
src/extra/DeBruijn-agda-list-4.lagda
Normal file
|
|
@ -0,0 +1,233 @@
|
|||
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
|
||||
|
||||
[Version using Ulf's prelude to derive equality]
|
||||
|
||||
## 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}
|
||||
-- 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}
|
||||
|
||||
[Old version, no longer needed]
|
||||
|
||||
_≟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 ⟩
|
||||
|
||||
## 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}
|
||||
|
||||
## Convert Exp to Phoas
|
||||
|
||||
\begin{code}
|
||||
Exp→PH : ∀ {A} → Exp ε A → ∀ {X} → PH X A
|
||||
Exp→PH M = h M tt
|
||||
where
|
||||
|
||||
env : (Type → Set) → Env → Set
|
||||
env X ε = ⊤
|
||||
env X (Γ , A) = env X Γ × X A
|
||||
|
||||
g : ∀ {X Γ A} → Var Γ A → env X Γ → X A
|
||||
g Z ⟨ _ , v ⟩ = v
|
||||
g (S x) ⟨ ρ , _ ⟩ = g x ρ
|
||||
|
||||
h : ∀ {X Γ A} → Exp Γ A → env X Γ → PH X A
|
||||
h (var x) ρ = var (g x ρ)
|
||||
h (abs N) ρ = abs (λ v → h N ⟨ ρ , v ⟩)
|
||||
h (app L M) ρ = app (h L ρ) (h M ρ)
|
||||
|
||||
_ : ∀ {X} → Exp→PH twoExp {X} ≡ twoPH {X}
|
||||
_ = refl
|
||||
\end{code}
|
||||
|
||||
Executing
|
||||
|
||||
Exp→PH twoExp
|
||||
|
||||
returns
|
||||
|
||||
λ {_} → abs (λ v → abs (λ v₁ → app (var v) (app (var v) (var v₁))))
|
||||
|
||||
|
||||
## 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}
|
||||
|
||||
|
||||
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
## DeBruijn encodings in Agda
|
||||
|
||||
\begin{code}
|
||||
module DeBruijn where
|
||||
module DeBruijn2 where
|
||||
\end{code}
|
||||
|
||||
## Imports
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue