From ba7f2d99e2262a6f3b18da9089578eb72dc25e95 Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 30 Jun 2018 20:04:48 -0300 Subject: [PATCH] inherently typed terms complete up to example --- src/plta/Connectives.lagda | 9 ++ src/plta/DeBruijn.lagda | 232 +++++++++++++++++++++++++++---------- src/plta/Lambda.lagda | 15 ++- 3 files changed, 193 insertions(+), 63 deletions(-) diff --git a/src/plta/Connectives.lagda b/src/plta/Connectives.lagda index 7191bc92..73130cbd 100644 --- a/src/plta/Connectives.lagda +++ b/src/plta/Connectives.lagda @@ -802,6 +802,15 @@ import Data.Unit using (⊤; tt) import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to ⊎-elim) import Data.Empty using (⊥; ⊥-elim) \end{code} +The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`. +The former makes it convenient to make triples or larger tuples from pairs, +permitting `a , b , c` to stand for `(a , (b , c))`. But it conflicts with +other useful notations, such as `[_,_]` and `[_,_,_]` to construct +lists of two or three elements in +Chapter [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %}) +or `Γ , A` to extend environments in +Chapter [DeBruijn]({{ site.baseurl }}{% link out/plta/DeBruijn.md %}). + ## Unicode diff --git a/src/plta/DeBruijn.lagda b/src/plta/DeBruijn.lagda index 79a802af..c6542bf2 100644 --- a/src/plta/DeBruijn.lagda +++ b/src/plta/DeBruijn.lagda @@ -174,56 +174,12 @@ refer to the former binding in the scope of the latter, but with de Bruijn indices it could be referred to as `# 2`. +## Inherently typed terms -OBSOLETE TEXT - -For each constructor -of terms `M`, there is a corresponding constructor of type derivations, -`Γ ⊢ M ⦂ A`: - -* `` `_ `` corresponds to `Ax` -* `ƛ_⇒_` corresponds to `⊢ƛ` -* `_·_` corresponds to `_·_` -* `` `zero `` corresponds to `⊢zero` -* `` `suc_ `` corresponds to `⊢suc` -* `` `case_[zero⇒_|suc_⇒_] `` corresponds to `⊢case` -* `μ_⇒_` corresponds to `⊢μ` - -Variable names `x` in terms correspond to derivations that -look up a name in the environment. There are two constructors of such -derivations `Z` and `S`, which behave similarly to constructors `here` -and `there` for looking up elements in a list. But derivations also -correspond to a natural number, take `Z` as zero and `S` as successor. - - - - ∋s ∋s ∋z - ------------------- `_ ------------------- `_ --------------- `_ - Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "z" ⦂ A - ------------------- `_ ------------------------------------------ _·_ - Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "s" · ` "z" ⦂ A - -------------------------------------------------- _·_ - Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ A - ---------------------------------------------- ⊢ƛ - Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A - ------------------------------------------------------------- ⊢ƛ - ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (A ⇒ A) ⇒ A ⇒ A - -where `∋s` and `∋z` abbreviate the two derivations: - - ---------------- Z - "s" ≢ "z" Γ₁ ∋ "s" ⦂ A ⇒ A - ----------------------------- S ------------- Z - Γ₂ ∋ "s" ⦂ A ⇒ A Γ₂ ∋ "z" ⦂ A - -and where `Γ₁ = ∅ , s ⦂ A ⇒ A` and `Γ₂ = ∅ , s ⦂ A ⇒ A , z ⦂ A`. - - - - - -## Syntax +With two examples under our belt, we can begin our formal development. +First, we get all our infix declarations out of the way. For ease of reading, +we list operators in order from least tightly binding to most. \begin{code} infix 4 _⊢_ infix 4 _∋_ @@ -233,29 +189,106 @@ infix 5 μ_ infixr 7 _⇒_ infixl 7 _·_ infix 8 `suc_ -infix 8 `_ -infix 8 S_ +infix 9 `_ +infix 9 S_ +infix 9 #_ +\end{code} +Since terms are inherently typed, we must define types and contexts +before terms. + +### Types + +As before, we have just two types, functions and naturals. The formal definition +is unchanged. +\begin{code} data Type : Set where - `ℕ : Type _⇒_ : Type → Type → Type + `ℕ : Type +\end{code} +For example, +\begin{code} +_ : Type +_ = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ +\end{code} +is a type that can be assigned to a Church numeral. -data Ctx : Set where - ∅ : Ctx - _,_ : Ctx → Type → Ctx +### Contexts -data _∋_ : Ctx → Type → Set where +Contexts are as before, but we drop the names. +Contexts are formalised as follows. +\begin{code} +data Context : Set where + ∅ : Context + _,_ : Context → Type → Context +\end{code} +A context is just a list of types, with the type of the most recently +bound variable on the right. As before, we let `Γ` and `Δ` range over contexts. +We write `∅` for the empty context, and `Γ , A` for the context `Γ` extended +by type `A`. For example +\begin{code} +_ : Context +_ = ∅ , `ℕ ⇒ `ℕ , `ℕ +\end{code} +is a context with two variables in scope, where the outer bound one has +type `` `ℕ → `ℕ ``, and the inner bound one has type `` `ℕ ``. - Z : ∀ {Γ} {A} +### Variables and the lookup judgement + +Inherently typed variables correspond to the lookup judgement. +They are represented by de Bruijn indices, and hence also correspond to natural numbers. +We write + + Γ ∋ A + +for variables which in context `Γ` have type `A`. +Their formalisation looks exactly like the old lookup judgement, +but with all names dropped. +\begin{code} +data _∋_ : Context → Type → Set where + + Z : ∀ {Γ A} ---------- → Γ , A ∋ A - S_ : ∀ {Γ} {A B} - → Γ ∋ B + S_ : ∀ {Γ A B} + → Γ ∋ A --------- - → Γ , A ∋ B + → Γ , B ∋ A +\end{code} +Constructor `S` no longer requires an additional parameter, since +without names shadowing is no longer an issue. Now constructors +`Z` and `S` correspond even more closely to the constructors +`here` and `there` for the element-of relation `_∈_` on lists, +as well as to constructors `zero` and `suc` for natural numbers. -data _⊢_ : Ctx → Type → Set where +For example, consider the following old-style lookup judgements: + +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "z" ⦂ `ℕ `` +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ `` + +They correspond to the following inherently-typed variables. +\begin{code} +_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ +_ = Z + +_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ +_ = S Z +\end{code} +In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`. + +### Terms and the typing judgement + +Inherently typed terms correspond to the typing judgement. +We write + + Γ ⊢ A + +for terms which in context `Γ` has type `A`. +Their formalisation looks exactly like the old typing judgement, +but with all terms and names dropped. +\begin{code} +data _⊢_ : Context → Type → Set where `_ : ∀ {Γ} {A} → Γ ∋ A @@ -294,10 +327,89 @@ data _⊢_ : Ctx → Type → Set where ---------- → Γ ⊢ A \end{code} +The definition exploits the close correspondence between the +structure of terms and the structure of a derivation showing that it +is well-typed: now we use the derivation _as_ the term. For example, +consider the following three terms, building up the Church numeral +two. + +For example, consider the following old-style typing judgements: + +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` ` "s" · ` "z" ⦂ `ℕ `` +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ `` +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ `ℕ ⇒ `ℕ `` +* `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` + +They correspond to the following inherently-typed terms. +\begin{code} +_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ `ℕ +_ = ` Z + +_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ `ℕ ⇒ `ℕ +_ = ` S Z + +_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ `ℕ +_ = ` S Z · ` Z + +_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ `ℕ +_ = ` S Z · (` S Z · ` Z) + +_ : ∅ , `ℕ ⇒ `ℕ ⊢ `ℕ ⇒ `ℕ +_ = ƛ (` S Z · (` S Z · ` Z)) + +_ : ∅ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ +_ = ƛ ƛ (` S Z · (` S Z · ` Z)) +\end{code} +The final inherently-typed term represents the Church numeral two. + +### A convenient abbreviation + +We can use a natural number to select a type from a context. +\begin{code} +lookup : Context → ℕ → Type +lookup (Γ , A) zero = A +lookup (Γ , _) (suc n) = lookup Γ n +lookup ∅ _ = ⊥-elim impossible + where postulate impossible : ⊥ +\end{code} +We intend to apply the function only when the natural is shorter +than the length of the context, which we indicate by postulating +an `impossible` term, just as we did +[here]({{ site.baseurl }}{% link out/plta/Lambda.md %}/#impossible). + +Given the above, we can convert a natural to a corresponding +De Bruijn indice, looking up its type in the context. +\begin{code} +count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n +count {Γ , _} zero = Z +count {Γ , _} (suc n) = S (count n) +count {∅} _ = ⊥-elim impossible + where postulate impossible : ⊥ +\end{code} +This requires the same trick as before. + +We can then introduce a convenient abbreviation for variables. +\begin{code} +#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n +# n = ` count n +\end{code} + +With this abbreviation, we can rewrite the Church numeral two more compactly. +\begin{code} +_ : ∅ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ +_ = ƛ ƛ (# 1 · (# 1 · # 0)) +\end{code} ## Test examples +We repeat the test examples from +Chapter [Lambda]({{ site.baseurl }}{% link out/plta/Lambda.md %}). +You can find the +[here]({{ site.baseurl }}{% link out/plta/Lambda.md %}/#derivation) +for comparison. \begin{code} two : ∀ {Γ} → Γ ⊢ `ℕ two = `suc `suc `zero diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda index 8a5a3018..e91934ed 100644 --- a/src/plta/Lambda.lagda +++ b/src/plta/Lambda.lagda @@ -782,7 +782,7 @@ sequence demonstrating that two times two is four. ## Syntax of types -We have just two types. +We have just two types: * Functions, `A ⇒ B` * Naturals, `` `ℕ `` @@ -844,6 +844,8 @@ Thus, ## Typing +### Contexts + While reduction considers only closed terms, typing must consider terms with free variables. To type a term, we must first type its subterms, and in particular in the @@ -869,6 +871,8 @@ data Context : Set where _,_⦂_ : Context → Id → Type → Context \end{code} +### Lookup judgement + We have two forms of _judgement_. The first is written Γ ∋ x ⦂ A @@ -912,10 +916,12 @@ data _∋_⦂_ : Context → Id → Type → Set where The constructors `Z` and `S` correspond roughly to the constructors `here` and `there` for the element-of relation `_∈_` on lists. -Constructor `S` takes an additional paramemer, which ensures that +Constructor `S` takes an additional parameter, which ensures that when we look up a variable that it is not _shadowed_ by another variable with the same name earlier in the list. +### Typing judgement + The second judgement is written Γ ⊢ M ⦂ A @@ -924,6 +930,9 @@ and indicates in context `Γ` that term `M` has type `A`. Context `Γ` provides types for all the free variables in `M`. For example +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ +* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` ` "s" · ` "z" ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ `ℕ ⇒ `ℕ `` * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` @@ -998,7 +1007,7 @@ functions, case expressions use naturals). The rules are deterministic, in that at most one rule applies to every term. -### Checking inequality and postulating the impossible +### Checking inequality and postulating the impossible {#impossible} The following function makes it convenient to assert an inequality. \begin{code}