added test cases
This commit is contained in:
wadler
parent
dce878d6e8
commit
67d27d0843
1 changed files with 176 additions and 186 deletions
|
|
@ -62,238 +62,228 @@ Id : Set
|
|||
Id = String
|
||||
\end{code}
|
||||
|
||||
### Lists of identifiers
|
||||
## Syntax
|
||||
|
||||
\begin{code}
|
||||
open Collections (Id) (_≟_)
|
||||
infix 4 _∋_`:_
|
||||
infix 4 _⊢_↑_
|
||||
infix 4 _⊢_↓_
|
||||
infixl 5 _,_`:_
|
||||
infix 5 _`:_
|
||||
infixr 6 _`→_
|
||||
infix 6 `λ_`→_
|
||||
infix 6 `μ_`→_
|
||||
infixl 9 _·_
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_`→_ : Type → Type → Type
|
||||
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,_`:_ : Ctx → Id → Type → Ctx
|
||||
|
||||
data Term : Set where
|
||||
⌊_⌋ : Id → Term
|
||||
`λ_`→_ : Id → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
`zero : Term
|
||||
`suc : Term → Term
|
||||
`case_[`zero`→_|`suc_`→_] : Term → Term → Id → Term → Term
|
||||
`μ_`→_ : Id → Term → Term
|
||||
_`:_ : Term → Type → Term
|
||||
\end{code}
|
||||
|
||||
## First development: Raw
|
||||
## Example terms
|
||||
|
||||
\begin{code}
|
||||
module Raw where
|
||||
\end{code}
|
||||
two : Term
|
||||
two = `suc (`suc `zero) `: `ℕ
|
||||
|
||||
### Syntax
|
||||
plus : Term
|
||||
plus = (`μ "p" `→ `λ "m" `→ `λ "n" `→
|
||||
`case ⌊ "m" ⌋ [`zero`→ ⌊ "n" ⌋
|
||||
|`suc "m" `→ `suc (⌊ "p" ⌋ · ⌊ "m" ⌋) · ⌊ "n" ⌋ ])
|
||||
`: `ℕ `→ `ℕ
|
||||
|
||||
\begin{code}
|
||||
infix 4 _∋_`:_
|
||||
infix 4 _⊢_↑_
|
||||
infix 4 _⊢_↓_
|
||||
infixl 5 _,_`:_
|
||||
infix 5 _`:_
|
||||
infixr 6 _`→_
|
||||
infix 6 `λ_`→_
|
||||
infix 6 `μ_`→_
|
||||
infixl 9 _·_
|
||||
four : Term
|
||||
four = plus · two · two
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_`→_ : Type → Type → Type
|
||||
Ch : Type
|
||||
Ch = (`ℕ `→ `ℕ) `→ `ℕ `→ `ℕ
|
||||
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,_`:_ : Ctx → Id → Type → Ctx
|
||||
twoCh : Term
|
||||
twoCh = (`λ "s" `→ `λ "z" `→ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)) `: Ch
|
||||
|
||||
data Term : Set where
|
||||
⌊_⌋ : Id → Term
|
||||
`λ_`→_ : Id → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
`zero : Term
|
||||
`suc : Term → Term
|
||||
`case_[`zero`→_|`suc_`→_] : Term → Term → Id → Term → Term
|
||||
`μ_`→_ : Id → Term → Term
|
||||
_`:_ : Term → Type → Term
|
||||
|
||||
\end{code}
|
||||
|
||||
### Example terms
|
||||
|
||||
\begin{code}
|
||||
Ch : Type
|
||||
Ch = (`ℕ `→ `ℕ) `→ `ℕ `→ `ℕ
|
||||
|
||||
two : Term
|
||||
two = (`λ "s" `→ `λ "z" `→ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)) `: Ch
|
||||
|
||||
plus : Term
|
||||
plus = (`λ "m" `→ `λ "n" `→ `λ "s" `→ `λ "z" `→
|
||||
plusCh : Term
|
||||
plusCh = (`λ "m" `→ `λ "n" `→ `λ "s" `→ `λ "z" `→
|
||||
⌊ "m" ⌋ · ⌊ "s" ⌋ · (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋))
|
||||
`: Ch `→ Ch `→ Ch
|
||||
`: Ch `→ Ch `→ Ch
|
||||
|
||||
norm : Term
|
||||
norm = (`λ "m" `→ ⌊ "m" ⌋ · (`λ "x" `→ `suc ⌊ "x" ⌋) · `zero)
|
||||
`: Ch `→ `ℕ
|
||||
fromCh : Term
|
||||
fromCh = (`λ "m" `→ ⌊ "m" ⌋ · (`λ "x" `→ `suc ⌊ "x" ⌋) · `zero)
|
||||
`: Ch `→ `ℕ
|
||||
|
||||
four : Term
|
||||
four = norm · (plus · two · two)
|
||||
fourCh : Term
|
||||
fourCh = fromCh · (plusCh · twoCh · twoCh)
|
||||
\end{code}
|
||||
|
||||
### Bidirectional type checking
|
||||
## Bidirectional type checking
|
||||
|
||||
\begin{code}
|
||||
data _∋_`:_ : Ctx → Id → Type → Set where
|
||||
data _∋_`:_ : Ctx → Id → Type → Set where
|
||||
|
||||
Z : ∀ {Γ x A}
|
||||
--------------------
|
||||
→ Γ , x `: A ∋ x `: A
|
||||
Z : ∀ {Γ x A}
|
||||
--------------------
|
||||
→ Γ , x `: A ∋ x `: A
|
||||
|
||||
S : ∀ {Γ w x A B}
|
||||
→ w ≢ x
|
||||
→ Γ ∋ w `: B
|
||||
--------------------
|
||||
→ Γ , x `: A ∋ w `: B
|
||||
S : ∀ {Γ w x A B}
|
||||
→ w ≢ x
|
||||
→ Γ ∋ w `: B
|
||||
--------------------
|
||||
→ Γ , x `: A ∋ w `: B
|
||||
|
||||
data _⊢_↑_ : Ctx → Term → Type → Set
|
||||
data _⊢_↓_ : Ctx → Term → Type → Set
|
||||
data _⊢_↑_ : Ctx → Term → Type → Set
|
||||
data _⊢_↓_ : Ctx → Term → Type → Set
|
||||
|
||||
data _⊢_↑_ where
|
||||
data _⊢_↑_ where
|
||||
|
||||
Ax : ∀ {Γ A x}
|
||||
→ Γ ∋ x `: A
|
||||
--------------
|
||||
→ Γ ⊢ ⌊ x ⌋ ↑ A
|
||||
Ax : ∀ {Γ A x}
|
||||
→ Γ ∋ x `: A
|
||||
--------------
|
||||
→ Γ ⊢ ⌊ x ⌋ ↑ A
|
||||
|
||||
_·_ : ∀ {Γ L M A B}
|
||||
→ Γ ⊢ L ↑ A `→ B
|
||||
→ Γ ⊢ M ↑ A
|
||||
---------------
|
||||
→ Γ ⊢ L · M ↑ B
|
||||
_·_ : ∀ {Γ L M A B}
|
||||
→ Γ ⊢ L ↑ A `→ B
|
||||
→ Γ ⊢ M ↑ A
|
||||
---------------
|
||||
→ Γ ⊢ L · M ↑ B
|
||||
|
||||
↑↓ : ∀ {Γ M A}
|
||||
→ Γ ⊢ M ↓ A
|
||||
----------------
|
||||
→ Γ ⊢ M `: A ↑ A
|
||||
↑↓ : ∀ {Γ M A}
|
||||
→ Γ ⊢ M ↓ A
|
||||
----------------
|
||||
→ Γ ⊢ M `: A ↑ A
|
||||
|
||||
data _⊢_↓_ where
|
||||
data _⊢_↓_ where
|
||||
|
||||
⊢λ : ∀ {Γ x N A B}
|
||||
→ Γ , x `: A ⊢ N ↓ B
|
||||
-----------------------
|
||||
→ Γ ⊢ `λ x `→ N ↓ A `→ B
|
||||
⊢λ : ∀ {Γ x N A B}
|
||||
→ Γ , x `: A ⊢ N ↓ B
|
||||
-----------------------
|
||||
→ Γ ⊢ `λ x `→ N ↓ A `→ B
|
||||
|
||||
⊢zero : ∀ {Γ}
|
||||
---------------
|
||||
→ Γ ⊢ `zero ↓ `ℕ
|
||||
⊢zero : ∀ {Γ}
|
||||
---------------
|
||||
→ Γ ⊢ `zero ↓ `ℕ
|
||||
|
||||
⊢suc : ∀ {Γ M}
|
||||
→ Γ ⊢ M ↓ `ℕ
|
||||
----------------
|
||||
→ Γ ⊢ `suc M ↓ `ℕ
|
||||
⊢suc : ∀ {Γ M}
|
||||
→ Γ ⊢ M ↓ `ℕ
|
||||
----------------
|
||||
→ Γ ⊢ `suc M ↓ `ℕ
|
||||
|
||||
⊢case : ∀ {Γ L M x N A}
|
||||
→ Γ ⊢ L ↑ `ℕ
|
||||
→ Γ ⊢ M ↓ A
|
||||
→ Γ , x `: `ℕ ⊢ N ↓ A
|
||||
------------------------------------------
|
||||
→ Γ ⊢ `case L [`zero`→ M |`suc x `→ N ] ↓ A
|
||||
⊢case : ∀ {Γ L M x N A}
|
||||
→ Γ ⊢ L ↑ `ℕ
|
||||
→ Γ ⊢ M ↓ A
|
||||
→ Γ , x `: `ℕ ⊢ N ↓ A
|
||||
------------------------------------------
|
||||
→ Γ ⊢ `case L [`zero`→ M |`suc x `→ N ] ↓ A
|
||||
|
||||
⊢μ : ∀ {Γ x N A}
|
||||
→ Γ , x `: A ⊢ N ↓ A
|
||||
-----------------------
|
||||
→ Γ ⊢ `μ x `→ N ↓ A
|
||||
⊢μ : ∀ {Γ x N A}
|
||||
→ Γ , x `: A ⊢ N ↓ A
|
||||
-----------------------
|
||||
→ Γ ⊢ `μ x `→ N ↓ A
|
||||
|
||||
↓↑ : ∀ {Γ M A}
|
||||
→ Γ ⊢ M ↑ A
|
||||
----------
|
||||
→ Γ ⊢ M ↓ A
|
||||
↓↑ : ∀ {Γ M A}
|
||||
→ Γ ⊢ M ↑ A
|
||||
----------
|
||||
→ Γ ⊢ M ↓ A
|
||||
\end{code}
|
||||
|
||||
## Type checking monad
|
||||
|
||||
\begin{code}
|
||||
Msg : Set
|
||||
Msg = String
|
||||
Msg : Set
|
||||
Msg = String
|
||||
|
||||
data Error : Set where
|
||||
err : Msg → Term → List Type → Error
|
||||
data TC (A : Set) : Set where
|
||||
error : Msg → Term → List Type → TC A
|
||||
return : A → TC A
|
||||
|
||||
TC : Set → Set
|
||||
TC A = Error ⊎ A
|
||||
|
||||
error : ∀ {A : Set} → Msg → Term → List Type → TC A
|
||||
error msg M As = inj₁ (err msg M As)
|
||||
|
||||
return : ∀ {A : Set} → A → TC A
|
||||
return = inj₂
|
||||
|
||||
_>>=_ : ∀ {A B : Set} → TC A → (A → TC B) → TC B
|
||||
inj₁ e >>= k = inj₁ e
|
||||
inj₂ x >>= k = k x
|
||||
_>>=_ : ∀ {A B : Set} → TC A → (A → TC B) → TC B
|
||||
error msg M As >>= k = error msg M As
|
||||
return v >>= k = k v
|
||||
\end{code}
|
||||
|
||||
## Type inferencer
|
||||
|
||||
\begin{code}
|
||||
_≟Tp_ : (A B : Type) → Dec (A ≡ B)
|
||||
A ≟Tp B = {!!}
|
||||
_≟Tp_ : (A B : Type) → Dec (A ≡ B)
|
||||
A ≟Tp B = {!!}
|
||||
|
||||
data Lookup (Γ : Ctx) (x : Id) : Set where
|
||||
ok : ∀ (A : Type) → (Γ ∋ x `: A) → Lookup Γ x
|
||||
data Lookup (Γ : Ctx) (x : Id) : Set where
|
||||
ok : ∀ (A : Type) → (Γ ∋ x `: A) → Lookup Γ x
|
||||
|
||||
lookup : ∀ (Γ : Ctx) (x : Id) → TC (Lookup Γ x)
|
||||
lookup ε x =
|
||||
error "variable not bound" ⌊ x ⌋ []
|
||||
lookup (Γ , x `: A) w with w ≟ x
|
||||
... | yes refl =
|
||||
return (ok A Z)
|
||||
... | no w≢ =
|
||||
do ok A ⊢x ← lookup Γ w
|
||||
return (ok A (S w≢ ⊢x))
|
||||
|
||||
lookup : ∀ (Γ : Ctx) (x : Id) → TC (Lookup Γ x)
|
||||
lookup ε x =
|
||||
error "variable not bound" ⌊ x ⌋ []
|
||||
lookup (Γ , x `: A) w with w ≟ x
|
||||
... | yes refl =
|
||||
return (ok A Z)
|
||||
... | no w≢ =
|
||||
do ok A ⊢x ← lookup Γ w
|
||||
return (ok A (S w≢ ⊢x))
|
||||
|
||||
data Synth (Γ : Ctx) (M : Term) : Set where
|
||||
ok : ∀ (A : Type) → (Γ ⊢ M ↑ A) → Synth Γ M
|
||||
|
||||
synth : ∀ (Γ : Ctx) (M : Term) → TC (Synth Γ M)
|
||||
inher : ∀ (Γ : Ctx) (M : Term) (A : Type) → TC (Γ ⊢ M ↓ A)
|
||||
data Synthesize (Γ : Ctx) (M : Term) : Set where
|
||||
ok : ∀ (A : Type) → (Γ ⊢ M ↑ A) → Synthesize Γ M
|
||||
|
||||
synth Γ ⌊ x ⌋ =
|
||||
do ok A ⊢x ← lookup Γ x
|
||||
return (ok A (Ax ⊢x))
|
||||
synth Γ (L · M) =
|
||||
do ok (A₀ `→ B) ⊢L ← synth Γ L
|
||||
where ok `ℕ _ → error "must apply function" (L · M) []
|
||||
ok A₁ ⊢M ← synth Γ M
|
||||
yes refl ← return (A₀ ≟Tp A₁)
|
||||
where no _ → error "types differ in application" (L · M) [ A₀ , A₁ ]
|
||||
return (ok B (⊢L · ⊢M))
|
||||
synth Γ (M `: A) =
|
||||
do ⊢M ← inher Γ M A
|
||||
return (ok A (↑↓ ⊢M))
|
||||
{-# CATCHALL #-}
|
||||
synth Γ M =
|
||||
error "untypable term" M []
|
||||
synthesize : ∀ (Γ : Ctx) (M : Term) → TC (Synthesize Γ M)
|
||||
inherit : ∀ (Γ : Ctx) (M : Term) (A : Type) → TC (Γ ⊢ M ↓ A)
|
||||
|
||||
inher Γ (`λ x `→ N) (A `→ B) =
|
||||
do ⊢N ← inher (Γ , x `: A) N B
|
||||
return (⊢λ ⊢N)
|
||||
inher Γ (`λ x `→ N) `ℕ =
|
||||
error "lambda cannot be natural" (`λ x `→ N) []
|
||||
inher Γ `zero `ℕ =
|
||||
return ⊢zero
|
||||
inher Γ `zero (A `→ B) =
|
||||
error "zero cannot be function" `zero [ A `→ B ]
|
||||
inher Γ (`suc M) `ℕ =
|
||||
do ⊢M ← inher Γ M `ℕ
|
||||
return (⊢suc ⊢M)
|
||||
inher Γ (`suc M) (A `→ B) =
|
||||
error "suc cannot be function" (`suc M) [ A `→ B ]
|
||||
inher Γ `case L [`zero`→ M |`suc x `→ N ] A =
|
||||
do ok `ℕ ⊢L ← synth Γ L
|
||||
where ok (A `→ B) _ → error "cannot case on function"
|
||||
(`case L [`zero`→ M |`suc x `→ N ])
|
||||
[ A `→ B ]
|
||||
⊢M ← inher Γ M A
|
||||
⊢N ← inher (Γ , x `: `ℕ) N A
|
||||
return (⊢case ⊢L ⊢M ⊢N)
|
||||
inher Γ (`μ x `→ M) A =
|
||||
do ⊢M ← inher (Γ , x `: A) M A
|
||||
return (⊢μ ⊢M)
|
||||
{-# CATCHALL #-}
|
||||
inher Γ M A₀ =
|
||||
do ok A₁ ⊢M ← synth Γ M
|
||||
yes refl ← return (A₀ ≟Tp A₁)
|
||||
where no _ → error "inheritance and synthesis conflict" M [ A₀ , A₁ ]
|
||||
return (↓↑ ⊢M)
|
||||
synthesize Γ ⌊ x ⌋ =
|
||||
do ok A ⊢x ← lookup Γ x
|
||||
return (ok A (Ax ⊢x))
|
||||
synthesize Γ (L · M) =
|
||||
do ok (A₀ `→ B) ⊢L ← synthesize Γ L
|
||||
where ok `ℕ _ → error "must apply function" (L · M) []
|
||||
ok A₁ ⊢M ← synthesize Γ M
|
||||
yes refl ← return (A₀ ≟Tp A₁)
|
||||
where no _ → error "types differ in application" (L · M) [ A₀ , A₁ ]
|
||||
return (ok B (⊢L · ⊢M))
|
||||
synthesize Γ (M `: A) =
|
||||
do ⊢M ← inherit Γ M A
|
||||
return (ok A (↑↓ ⊢M))
|
||||
{-# CATCHALL #-}
|
||||
synthesize Γ M =
|
||||
error "cannot synthesize type for term" M []
|
||||
|
||||
inherit Γ (`λ x `→ N) (A `→ B) =
|
||||
do ⊢N ← inherit (Γ , x `: A) N B
|
||||
return (⊢λ ⊢N)
|
||||
inherit Γ (`λ x `→ N) `ℕ =
|
||||
error "lambda cannot be natural" (`λ x `→ N) []
|
||||
inherit Γ `zero `ℕ =
|
||||
return ⊢zero
|
||||
inherit Γ `zero (A `→ B) =
|
||||
error "zero cannot be function" `zero [ A `→ B ]
|
||||
inherit Γ (`suc M) `ℕ =
|
||||
do ⊢M ← inherit Γ M `ℕ
|
||||
return (⊢suc ⊢M)
|
||||
inherit Γ (`suc M) (A `→ B) =
|
||||
error "suc cannot be function" (`suc M) [ A `→ B ]
|
||||
inherit Γ `case L [`zero`→ M |`suc x `→ N ] A =
|
||||
do ok `ℕ ⊢L ← synthesize Γ L
|
||||
where ok (A `→ B) _ → error "cannot case on function"
|
||||
(`case L [`zero`→ M |`suc x `→ N ])
|
||||
[ A `→ B ]
|
||||
⊢M ← inherit Γ M A
|
||||
⊢N ← inherit (Γ , x `: `ℕ) N A
|
||||
return (⊢case ⊢L ⊢M ⊢N)
|
||||
inherit Γ (`μ x `→ M) A =
|
||||
do ⊢M ← inherit (Γ , x `: A) M A
|
||||
return (⊢μ ⊢M)
|
||||
{-# CATCHALL #-}
|
||||
inherit Γ M A₀ =
|
||||
do ok A₁ ⊢M ← synthesize Γ M
|
||||
yes refl ← return (A₀ ≟Tp A₁)
|
||||
where no _ → error "inheritance and synthesis conflict" M [ A₀ , A₁ ]
|
||||
return (↓↑ ⊢M)
|
||||
\end{code}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue