Merge pull request #389 from plfa/intrinsic
Change inherent to intrinsic
This commit is contained in:
Philip Wadler
GitHub
commit
3ef66e5dbe
5 changed files with 70 additions and 56 deletions
|
|
@ -1,5 +1,5 @@
|
|||
---
|
||||
title : "DeBruijn: Inherently typed de Bruijn representation"
|
||||
title : "DeBruijn: Intrinsically-typed de Bruijn representation"
|
||||
layout : page
|
||||
prev : /Properties/
|
||||
permalink : /DeBruijn/
|
||||
|
|
@ -16,17 +16,30 @@ separately from types. We began with that approach because it
|
|||
is traditional, but it is not the one we recommend. This
|
||||
chapter presents an alternative approach, where named
|
||||
variables are replaced by de Bruijn indices and terms are
|
||||
inherently typed. Our new presentation is more compact, using
|
||||
less than half the lines of code required previously to cover
|
||||
the same ground.
|
||||
indexed by their types. Our new presentation is more compact, using
|
||||
substantially fewer lines of code to cover the same ground.
|
||||
|
||||
The inherently typed representation was first proposed by
|
||||
There are two fundamental approaches to typed lambda calculi.
|
||||
One approach, followed in the last two chapters,
|
||||
is to first define terms and then define types.
|
||||
Terms exist independent of types, and may have types assigned to them
|
||||
by separate typing rules.
|
||||
Another approach, followed in this chapter,
|
||||
is to first define types and then define terms.
|
||||
Terms and type rules are intertwined, and it makes no sense to talk
|
||||
of a term without a type.
|
||||
The two approaches are sometimes called _Curry style_ and _Church style_.
|
||||
Following Reynolds, we will refer to them as _extrinsic_ and _intrinsic_.
|
||||
|
||||
The particular representation described here
|
||||
was first proposed by
|
||||
Thorsten Altenkirch and Bernhard Reus.
|
||||
The formalisation of renaming and substitution
|
||||
we use is due to Conor McBride.
|
||||
Related work has been carried out by
|
||||
James Chapman, James McKinna, and many others.
|
||||
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
|
|
@ -99,22 +112,22 @@ unique representation, rather than being represented by the
|
|||
equivalence class of terms under alpha renaming.
|
||||
|
||||
The other important feature of our chosen representation is
|
||||
that it is _inherently typed_. In the previous two chapters,
|
||||
that it is _intrinsically typed_. In the previous two chapters,
|
||||
the definition of terms and the definition of types are
|
||||
completely separate. All terms have type `Term`, and nothing
|
||||
in Agda prevents one from writing a nonsense term such as
|
||||
`` `zero · `suc `zero `` which has no type. Such terms that
|
||||
exist independent of types are sometimes called _preterms_ or
|
||||
_raw terms_. Here we are going to replace the type `Term` of
|
||||
raw terms by the more sophisticated type `Γ ⊢ A` of inherently
|
||||
typed terms, which in context `Γ` have type `A`.
|
||||
raw terms by the type `Γ ⊢ A` of intrinsically-typed terms
|
||||
which in context `Γ` have type `A`.
|
||||
|
||||
While these two choices fit well, they are independent. One
|
||||
can use de Bruijn indices in raw terms, or (with more
|
||||
difficulty) have inherently typed terms with names. In
|
||||
can use de Bruijn indices in raw terms, or
|
||||
have intrinsically-typed terms with names. In
|
||||
Chapter [Untyped]({{ site.baseurl }}/Untyped/),
|
||||
we will introduce terms with de Bruijn indices that
|
||||
are inherently scoped but not typed.
|
||||
are intrinsically scoped but not typed.
|
||||
|
||||
|
||||
## A second example
|
||||
|
|
@ -189,7 +202,7 @@ Bruijn indices it could be referred to as `# 2`.
|
|||
|
||||
## Order of presentation
|
||||
|
||||
In the current chapter, the use of inherently-typed terms
|
||||
In the current chapter, the use of intrinsically-typed terms
|
||||
necessitates that we cannot introduce operations such as
|
||||
substitution or reduction without also showing that they
|
||||
preserve types. Hence, the order of presentation must change.
|
||||
|
|
@ -223,7 +236,7 @@ infix 9 S_
|
|||
infix 9 #_
|
||||
```
|
||||
|
||||
Since terms are inherently typed, we must define types and
|
||||
Since terms are intrinsically typed, we must define types and
|
||||
contexts before terms.
|
||||
|
||||
### Types
|
||||
|
|
@ -260,14 +273,16 @@ type `` `ℕ ``.
|
|||
|
||||
### Variables and the lookup judgment
|
||||
|
||||
Inherently typed variables correspond to the lookup judgment.
|
||||
Intrinsically-typed variables correspond to the lookup judgment.
|
||||
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 judgment, but
|
||||
for variables which in context `Γ` have type `A`.
|
||||
The lookup judgement is formalised by a datatype indexed
|
||||
by a context and a type.
|
||||
It looks exactly like the old lookup judgment, but
|
||||
with all variable names dropped:
|
||||
```
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
|
@ -294,7 +309,7 @@ judgments:
|
|||
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "z" ⦂ `ℕ ``
|
||||
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
|
||||
|
||||
They correspond to the following inherently-typed variables:
|
||||
They correspond to the following intrinsically-typed variables:
|
||||
```
|
||||
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ
|
||||
_ = Z
|
||||
|
|
@ -309,13 +324,15 @@ and `"s"` by `S Z`
|
|||
|
||||
### Terms and the typing judgment
|
||||
|
||||
Inherently typed terms correspond to the typing judgment.
|
||||
Intrinsically-typed terms correspond to the typing judgment.
|
||||
We write
|
||||
|
||||
Γ ⊢ A
|
||||
|
||||
for terms which in context `Γ` has type `A`. Their
|
||||
formalisation looks exactly like the old typing judgment, but
|
||||
for terms which in context `Γ` has type `A`.
|
||||
The judgement is formalised by a datatype indexed
|
||||
by a context and a type.
|
||||
It looks exactly like the old typing judgment, but
|
||||
with all terms and variable names dropped:
|
||||
```
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
|
@ -362,8 +379,7 @@ 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 old-style typing
|
||||
judgments:
|
||||
For example, consider the following old-style typing judgments:
|
||||
|
||||
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ ``
|
||||
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ ``
|
||||
|
|
@ -372,7 +388,7 @@ judgments:
|
|||
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ `ℕ ⇒ `ℕ ``
|
||||
* `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ ``
|
||||
|
||||
They correspond to the following inherently-typed terms:
|
||||
They correspond to the following intrinsically-typed terms:
|
||||
```
|
||||
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ `ℕ
|
||||
_ = ` Z
|
||||
|
|
@ -392,8 +408,7 @@ _ = ƛ (` S Z · (` S Z · ` Z))
|
|||
_ : ∅ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ
|
||||
_ = ƛ ƛ (` S Z · (` S Z · ` Z))
|
||||
```
|
||||
The final inherently-typed term represents the Church numeral
|
||||
two.
|
||||
The final term represents the Church numeral two.
|
||||
|
||||
### Abbreviating de Bruijn indices
|
||||
|
||||
|
|
@ -482,7 +497,7 @@ contexts. While we are at it, we also generalise `twoᶜ` and
|
|||
#### Exercise `mul` (recommended)
|
||||
|
||||
Write out the definition of a lambda term that multiplies
|
||||
two natural numbers, now adapted to the inherently typed
|
||||
two natural numbers, now adapted to the intrinsically-typed
|
||||
DeBruijn representation.
|
||||
|
||||
```
|
||||
|
|
@ -585,13 +600,13 @@ unchanged.
|
|||
|
||||
We will see below that renaming by `S_` plays a key role in
|
||||
substitution. For traditional uses of de Bruijn indices
|
||||
without inherent typing, this is a little tricky. The code
|
||||
without intrinsic typing, this is a little tricky. The code
|
||||
keeps count of a number where all greater indexes are free and
|
||||
all smaller indexes bound, and increment only indexes greater
|
||||
than the number. It's easy to have off-by-one errors. But
|
||||
it's hard to imagine an off-by-one error that preserves
|
||||
typing, and hence the Agda code for inherently-typed de Bruijn
|
||||
terms is inherently reliable.
|
||||
typing, and hence the Agda code for intrinsically-typed de Bruijn
|
||||
terms is intrinsically reliable.
|
||||
|
||||
|
||||
## Simultaneous Substitution
|
||||
|
|
@ -1331,7 +1346,7 @@ Using the evaluator, confirm that two times two is four.
|
|||
```
|
||||
|
||||
|
||||
## Inherently-typed is golden
|
||||
## Intrinsic typing is golden
|
||||
|
||||
Counting the lines of code is instructive. While this chapter
|
||||
covers the same formal development as the previous two
|
||||
|
|
@ -1345,9 +1360,8 @@ number of lines of code is as follows:
|
|||
DeBruijn 275
|
||||
|
||||
The relation between the two approaches approximates the
|
||||
golden ratio: raw terms with a separate typing relation
|
||||
require about 1.6 times as much code as inherently-typed terms
|
||||
with de Bruijn indices.
|
||||
golden ratio: extrinsically-typed terms
|
||||
require about 1.6 times as much code as intrinsicaly-typed.
|
||||
|
||||
## Unicode
|
||||
|
||||
|
|
|
|||
|
|
@ -13,22 +13,23 @@ module plfa.part2.Inference where
|
|||
So far in our development, type derivations for the corresponding
|
||||
term have been provided by fiat.
|
||||
In Chapter [Lambda]({{ site.baseurl }}/Lambda/)
|
||||
type derivations were given separately from the term, while
|
||||
type derivations are extrinsic to the term, while
|
||||
in Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/)
|
||||
the type derivation was inherently part of the term.
|
||||
type derivations are intrinsic to the term,
|
||||
but in both we have written out the type derivations in full.
|
||||
|
||||
In practice, one often writes down a term with a few decorations and
|
||||
applies an algorithm to _infer_ the corresponding type derivation.
|
||||
Indeed, this is exactly what happens in Agda: we specify the types for
|
||||
top-level function declarations, and type information for everything
|
||||
else is inferred from what has been given. The style of inference
|
||||
used is based on a technique called _bidirectional_ type
|
||||
Agda uses is based on a technique called _bidirectional_ type
|
||||
inference, which will be presented in this chapter.
|
||||
|
||||
This chapter ties our previous developments together. We begin with
|
||||
a term with some type annotations, quite close to the raw terms of
|
||||
a term with some type annotations, close to the raw terms of
|
||||
Chapter [Lambda]({{ site.baseurl }}/Lambda/),
|
||||
and from it we compute a term with inherent types, in the style of
|
||||
and from it we compute an intrinsically-typed term, in the style of
|
||||
Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
|
||||
|
||||
## Introduction: Inference rules as algorithms {#algorithms}
|
||||
|
|
@ -257,7 +258,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
|
|||
```
|
||||
|
||||
Once we have a type derivation, it will be easy to construct
|
||||
from it the inherently typed representation. In order that we
|
||||
from it the intrinsically-typed representation. In order that we
|
||||
can compare with our previous development, we import
|
||||
module `pfla.DeBruijn`:
|
||||
|
||||
|
|
@ -268,9 +269,7 @@ import plfa.part2.DeBruijn as DB
|
|||
The phrase `as DB` allows us to refer to definitions
|
||||
from that module as, for instance, `DB._⊢_`, which is
|
||||
invoked as `Γ DB.⊢ A`, where `Γ` has type
|
||||
`DB.Context` and `A` has type `DB.Type`. We also import
|
||||
`Type` and its constructors directly, so the latter may
|
||||
also be referred to as just `Type`.
|
||||
`DB.Context` and `A` has type `DB.Type`.
|
||||
|
||||
|
||||
## Syntax
|
||||
|
|
@ -1002,11 +1001,11 @@ _ = refl
|
|||
## Erasure
|
||||
|
||||
From the evidence that a decorated term has the correct type it is
|
||||
easy to extract the corresponding inherently typed term. We use the
|
||||
easy to extract the corresponding intrinsically-typed term. We use the
|
||||
name `DB` to refer to the code in
|
||||
Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
|
||||
It is easy to define an _erasure_ function that takes evidence of a
|
||||
type judgment into the corresponding inherently typed term.
|
||||
It is easy to define an _erasure_ function that takes an extrinsic
|
||||
type judgment into the corresponding intrinsically-typed term.
|
||||
|
||||
First, we give code to erase a type:
|
||||
```
|
||||
|
|
@ -1056,7 +1055,7 @@ constructors that correspond to switching from synthesized
|
|||
to inherited or vice versa are dropped.
|
||||
|
||||
We confirm that the erasure of the type derivations in
|
||||
this chapter yield the corresponding inherently typed terms
|
||||
this chapter yield the corresponding intrinsically-typed terms
|
||||
from the earlier chapter:
|
||||
```
|
||||
_ : ∥ ⊢2+2 ∥⁺ ≡ DB.2+2
|
||||
|
|
@ -1068,7 +1067,7 @@ _ = refl
|
|||
Thus, we have confirmed that bidirectional type inference
|
||||
converts decorated versions of the lambda terms from
|
||||
Chapter [Lambda]({{ site.baseurl }}/Lambda/)
|
||||
to the inherently typed terms of
|
||||
to the intrinsically-typed terms of
|
||||
Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -32,11 +32,12 @@ of variants of lambda calculus.
|
|||
|
||||
Be aware that the approach we take here is _not_ our recommended
|
||||
approach to formalisation. Using de Bruijn indices and
|
||||
inherently-typed terms, as we will do in
|
||||
intrinsically-typed terms, as we will do in
|
||||
Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
|
||||
leads to a more compact formulation. Nonetheless, we begin with named
|
||||
variables, partly because such terms are easier to read and partly
|
||||
because the development is more traditional.
|
||||
variables and extrinsically-typed terms,
|
||||
partly because names are easier than indices to read,
|
||||
and partly because the development is more traditional.
|
||||
|
||||
The development in this chapter was inspired by the corresponding
|
||||
development in Chapter _Stlc_ of _Software Foundations_
|
||||
|
|
|
|||
|
|
@ -32,10 +32,10 @@ the rest as an exercise for the reader.
|
|||
|
||||
Our informal descriptions will be in the style of
|
||||
Chapter [Lambda]({{ site.baseurl }}/Lambda/),
|
||||
using named variables and a separate type relation,
|
||||
using extrinsically-typed terms,
|
||||
while our formalisation will be in the style of
|
||||
Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
|
||||
using de Bruijn indices and inherently typed terms.
|
||||
using intrinsically-typed terms.
|
||||
|
||||
By now, explaining with symbols should be more concise, more precise,
|
||||
and easier to follow than explaining in prose.
|
||||
|
|
|
|||
|
|
@ -12,8 +12,8 @@ module plfa.part2.Untyped where
|
|||
|
||||
In this chapter we play with variations on a theme:
|
||||
|
||||
* Previous chapters consider inherently-typed calculi;
|
||||
here we consider one that is untyped but inherently scoped.
|
||||
* Previous chapters consider intrinsically-typed calculi;
|
||||
here we consider one that is untyped but intrinsically scoped.
|
||||
|
||||
* Previous chapters consider call-by-value calculi;
|
||||
here we consider call-by-name.
|
||||
|
|
@ -128,7 +128,7 @@ Show that `Context` is isomorphic to `ℕ`.
|
|||
|
||||
## Variables and the lookup judgment
|
||||
|
||||
Inherently typed variables correspond to the lookup judgment. The
|
||||
Intrinsically-scoped variables correspond to the lookup judgment. The
|
||||
rules are as before:
|
||||
```
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
|
@ -153,7 +153,7 @@ binds two variables.
|
|||
|
||||
## Terms and the scoping judgment
|
||||
|
||||
Inherently typed terms correspond to the typing judgment, but with
|
||||
Intrinsically-scoped terms correspond to the typing judgment, but with
|
||||
`★` as the only type. The result is that we check that terms are
|
||||
well scoped — that is, that all variables they mention are in scope —
|
||||
but not that they are well typed:
|
||||
|
|
|
|||
Loading…
Reference in a new issue