-- vim: colorcolumn=
-- vim: spell
-- vim: spelllang=en
-- VIM: formatprg=par\ h1p4j
{-# LANGUAGE QuasiQuotes, OverloadedStrings #-}
{-# OPTIONS_GHC -F -pgmF frquotes #-}
{-# OPTIONS -Wall -fno-warn-missing-signatures #-}
import Control.Monad.Writer
import Language.LaTeX (ViewOpts(..), (★), ø, quickView, myViewOpts)
import Language.LaTeX.Unicode
import Language.LaTeX.Builder.QQ
import NaPaKit
-- sections
[keys|intro defNaPa usingNaPa soundness concl paramSection finSection napaTypesSection|]
--figures
[keys|subfig opsfig opsdiag rellogfig datarelfig coreFunRel kitsF coreTypesF coreTypesRelF|]
-- Bibliography
[keys|de-bruijn-72 mcbride-mckinna-04 altenkirch-reus-99 bird-paterson-99
atkey-hoas-09 pouillard-pottier-10 pouillard-11
bernardy-10 reynolds-83 mcbride-paterson-08 altenkirch-93 wadler-free-89
bellegarde-94|]
napacode = pouillard11
title = «Nameless, Painless»
authors = [(«Nicolas Pouillard», «INRIA», «Nicolas.Pouillard@inria.fr»)]
abstract = [texFile|abstract|]
body = execWriter $ do
section «Introduction» intro
p"representations with names and binders in the wild"
«It is quite common in the programming realm to deal with the mundane
business of data structures with names and binders. Compilers, code
generators, static analysers, theorem provers, and type-checkers
have this in common. They manipulate programs, formulae, proofs, and
types. When seen as pieces of data, there is a common difficulty:
the representation of variables (names and binders).»
p"binders are hard"
«One traditional approach is to represent all the occurrences of a
bound variable identically by using character strings or integers.
While being the most obvious representation it is known to cause a
lot of trouble when dealing with operations like substitution. In
particular we name it the capture-avoiding substitution because it
has to rename some variables to avoid accidental changes called
captures.»
p"we focus on nameless"
«In this article we focus on a different kind of representation,
namely {dbis} {cite[debruijn72]}. This representation is said to be
nameless because variables are no longer identified by a name but a
notion of ``distance'' to the binding point. {_Dbis} are the most
famous nameless representation and in the following we will use the
term ``nameless'' as a synonym for ``{dbis}''.»
p"nameless advantages"
«The nameless approach solves part of the problem by providing a
canonical representation. More precisely binding occurrences are no
longer named (we now use {lc|λ.|} instead of {lc|λx.|}). Then bound
variables are represented by the ``distance'' to the binding λ. This
distance is the number of λs to cross in order to reach the
binding{(∼)}λ.»
p"why having a safer system?"
«A major issue with this nameless representation is its
arithmetic flavor. Indeed properties about names and binders are
turned into arithmetic formulae. The result can be harder to
understand, and worse, easier to get wrong. To remedy this,
several techniques have been proposed to give finer grained
types to these representations {cite[mcbridemckinna04, altenkirch93,
altenkirchreus99, birdpaterson99]}. We continue further in this
direction by providing a safer system to program with a nameless
representation.»
subsection «Contributions»
p"nameless only"
«In a previous paper {cite [pouillardpottier10]} we developed an
abstract interface to program with names and binders. The interface
can be both implemented in a named or a nameless style. Here by
focusing on a nameless representation we greatly simplify the
programming interface needed to achieve our safety goals. This is at
the expense of some loss of abstraction. However while the goals are
less ambitious, the results are significantly more applicable since
simpler and closer to a concrete representation.»
p"better worlds"
«Our previous nameless implementation was relying on the {_Fin}
approach (described in section {ref finSection}). The notion of
worlds presented here (in section {ref napaTypesSection}) is
significantly more precise than {_Fin}. However the worlds were
already abstract to the programmer and they still are. Indeed
abstraction is necessary to retain the parametricity properties we
want from world-polymorphic functions.»
p"solid from the ground"
«While a fair amount of proofs were already mechanized in
{cite[pouillardpottier10]}, the logical relation argument was still
largely on paper. Here we not only finished these mechanized proofs
but have every part well connected in one single setup. The code and
proofs are accessible online at {cite[napacode]} and we encourage
the reader to have a look for reference on technical details and
applications.»
subsection «Outline of the paper»
p"plan"
«This paper is organized as follows. In the remainder of this section
we present several nameless techniques to represent data structures
with bindings. In section {ref defNaPa} we detail our approach to
the problem. In section {ref usingNaPa} we give some examples and
advanced operations. In section {ref soundness} we develop a logical
relation construction which ensures the soundness properties we
want, and we show how to exploit these properties on concrete
examples. All the construction is built in the {_Agda} language, our
system is an {_Agda} library and its soundness proof is done in
{_Agda} as well.»
subsection «A brief introduction to {_Agda} notation»
p"agda types"
«Throughout the paper, our definitions are presented in the syntax of
{_Agda}. In {_Agda}, {_Set} (or {_Set0}) is the type of small
types like {_Bool}, {agda|Maybe (List Bool)|}, or {_ℕ}. {_Set1}
is the type of {_Set}, {agda|Set → Bool|}, or {agda|ℕ → Set|}.
The function space is written {agda|A → B|}, while the dependent
function space is written {agda|(x : A) → B|}{mediumspace} or
{agda| ∀ (x : A) → B|}. An implicit parameter, introduced via
{agda| ∀{x : A} → B|}, can be omitted at a call site if its
value can be inferred from the context. There are shortcuts for
introducing multiple arguments at once or for omitting a type
annotation, as in {agda|∀{A} {i j : A} x → e|}. There is no specific
sort for propositions in {_Agda}, everything is in {agda|Set ℓ|} for
some {agda|ℓ|}. The unit type is a record type with no fields named
{(⊤)}, it also represents the {agda|True|} proposition. The empty
type is an (inductive) data type with no constructors named {(⊥)},
it also represents the {agda|False|} proposition. The negation
{agda|¬ A|} is defined as {agda|A → ⊥|}.»
p"agda constructors"
«The same name can be used for different data constructors. {_Agda}
makes use of type annotations to resolve ambiguities.»
p"agda definitions"
«As in Haskell, a definition consists of a type signature and a
sequence of defining equations, which may involve pattern-matching.
The {agda|with|} construct extends a pattern-matching-based
definition with new columns. An ellipsis {emph[agda|...|]} is used
to elide a redundant equation prefix.»
p"agda lexical syntax"
«{_Agda} is strict about whitespace: {agda|x≤y|} is an identifier,
whereas {agda|x ≤ y|} is an application. This allows naming a
variable after its type (deprived of any whitespace). We use mixfix
declarations, such as {agda|_⊕_|}. We use some definitions from
{_Agda}'s standard library: natural numbers, booleans, lists, and
applicative functors ({agda|pure|}, {agda|_⊛_|}).»
p"not self-contained"
«For the sake of conciseness, the code fragments presented in
the paper are sometimes not perfectly self-contained. However, a
complete {_Agda} development is available online {cite[napacode]}.»
subsection «Related work: nameless representations»
p"nameless representations"
«Various techniques have been discovered to build a nameless
representation. We have chosen a few of them which gradually setup
the stage.»
subsubsection «{bare}: The original approach»
p"description of bare"
«We call this one {bare}, because it solely relies on natural
numbers. To make things more concrete here is an example of its
use when defining the untyped λ-calculus with local bindings
({agda|let|}). Our naming convention is as follows: we call {_Tm}
the type of λ-terms, {_V} is the data constructor for variables, {op
_App} is for the application, {ƛ} is for the λ-abstraction, and
finally {_Let} is for local bindings.»
[agdaP|
data Tm : Set where
V : (x : ℕ) → Tm
_·_ : (t u : Tm) → Tm
ƛ : (t : Tm) → Tm
Let : (t u : Tm) → Tm
|]
p"in bare, types are weak"
«From the point of view of the binding structure, it is striking that
no difference appears between the constructors of the data type. It
is completely up to the programmer to manage the scoping difference
introduced by {ƛ} and {_Let}. This is even more worrying in the
{_Let} case since we have no clue of difference between the
arguments.»
p"appTm in bare"
«Here is an example using this representation to build the λ-term for
{lc|λf.λx.f x|}.»
[agdaP|
appTm : Tm
appTm = ƛ (ƛ (V 1 · V 0))
|]
p"bare expressiveness"
«The main advantages of this approach are its simplicity and
its expressiveness. The expressiveness is almost maximal since
no restriction is put on the usage of variables. Actually
expressiveness is really maximal only in partial languages where all
types are inhabited by a looping term. Indeed the absence of
restrictions on data can be constraining when receiving data as
argument. In a total language all cases have to be covered, even
those we consider as impossible. For instance a function accepting
only closed terms will have to provide a return value for the
variable case anyway. Sometimes the return type is so constrained
that the type is actually empty in this case, and so no dummy
value can be returned. However, even in a partial language the
expressiveness is maximal if we are willing to live in an error
monad.»
subsubsection «{_Maybe}: The nested data type approach»
p"Tm in Maybe"
«The nested data type approach {cite [bellegarde94, birdpaterson99,
altenkirchreus99]} is a first step towards better properties about
the binding structure of terms. Let us start with the definition of
{_Tm} with this approach:»
[agdaP|
data Tm (A : Set) : Set where
V : (x : A) → Tm A
_·_ : (t u : Tm A) → Tm A
ƛ : (t : Tm (Maybe A)) → Tm A
Let : (t : Tm A) (u : Tm (Maybe A)) → Tm A
|]
p"explaining Tm in Maybe"
«There are three points to look at. The {_Tm} type is parameterized
by another type called {_A}, so we can look at it as a kind of
container. Note also that the variable case {_V} does not hold a
{_ℕ} but an {_A}. Last but not least the {ƛ} case holds a term whose
parameter is not simply an {_A} but a {agda|Maybe A|}.»
p"nested/non-regular"
«This last point makes the {_Tm} type a nested data type, also
called a non-regular type. This has the consequence of requiring
polymorphic recursion to write recursive functions on such a type.»
p"adequacy of Maybe"
«To understand why this is an adequate representation of λ-terms one
has to look a bit more at the meaning of {_Maybe}. If types are seen
as sets, then {_Maybe} takes a set and returns a set with one extra
element. So each time we cross a {ƛ}, there is one extra element in
the set of allowed variables, exactly capturing the fact we are
introducing a variable.»
p"appTm in Maybe"
«To see the difference with the previous approach, here is the
{agda|appTm|} λ-term again:»
[agdaP|
appTm : Tm ⊥
appTm = ƛ (ƛ (V (just nothing) · V nothing))
|]
p"⊥ in Maybe"
«Note the use of the empty type {(⊥)} to state the closedness of the
{agda|appTm|} term. Stating this kind of properties was impossible
to do with the previous approach, without resorting to logical
properties on the side.»
subsubsectionLbl «The {_Fin} approach» finSection
p"Fin approach description"
«Another approach already described and used in {cite [altenkirch93,
mcbridemckinna04]} is to index everything (terms for example) by a
bound. This bound is the maximum number of distinct free variables
allowed in the value. This rule is enforced in two parts: variables
have to be strictly lower than their bound, and the bound is
incremented by one when crossing a name abstraction (a λ-abstraction
for instance, called {ƛ} here).»
p"Fin type description"
«The {agda|Fin n|} type is used for variables and represents natural
numbers strictly lower than {agda|n|}. The name {agda|Fin n|} comes
from the fact that it defines finite sets of size {agda|n|}. We call
this approach {_Fin} for its use of this type. The definition found
in {_Agda} standard library is the following:»
[agdaP|
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} (i : Fin n) → Fin (suc n)
|]
p"Tm in Fin"
«Given this {_Fin} type, one can define the {_Tm} data type using
this approach:»
[agdaP|
data Tm n : Set where
V : (x : Fin n) → Tm n
_·_ : (t u : Tm n) → Tm n
ƛ : (t : Tm (suc n)) → Tm n
Let : (t : Tm n) (u : Tm (suc n)) → Tm n
|]
p"Tm 0 in Fin"
«As the previous approach, this representation helps enforcing some
wellformedness properties, for instance {agda|Tm 0|} is the type of
closed λ-terms.»
p"appTm in Fin"
«Here is the {agda|appTm|} λ-term in this approach:»
[agdaP|
appTm : Tm 0
appTm = ƛ (ƛ (V (suc zero) · V zero))
|]
p"Fin/Maybe connection"
«We can easily draw a link with the {_Maybe} approach. Indeed, the
{agda|Fin (suc n)|} type has exactly one more element than the
{agda|Fin n|} type. Although they are not equivalent for at least
two reasons. The {_Maybe} approach can accept any type to represent
variables. This makes the structure more like a container and
this can be particularly helpful to define the substitution as
the composition of {agda|mapTm : ∀{A B} → (A → B) → Tm A → Tm B|}
and {agda|joinTm : ∀{A} → Tm (Tm A) → Tm A|} as in
{cite[birdpaterson99,altenkirchreus99]}. The {_Fin} approach has
advantages as well, the representation is concrete and simpler since
closer to the {bare} approach. However this apparent simplicity
comes at a cost, we will see that its concrete representation is one
root of the problem.»
section «{napa}, a safer nameless representation» defNaPa
subsection «Motivation»
p"wellformedness of terms, what about behavior of functions"
«While these nameless approaches easily guarantee wellformedness of
terms, nothing is said about functions manipulating terms. How are
the inputs of a function related to its output? What should a
function be able to do given unknown free variables? We claim that
free variables should be kept abstract. More precisely a function
{qm|f|} operating on terms should commute with a renaming {qm|Φ|} of
free variables, namely {qm|f ∘ Φ = Φ ∘ f|}. By renaming we mean a
permutation of the free variables (more precisely an injective
function). In fact this is a bit more flexible, depending on the
type of the function {qm|f|} this property will be enforced or not,
as we will see in section {ref paramSection}.»
p"catches programming errors but not a restriction"
«The goal is to catch some programming errors by having finer types
for the manipulated values and for the functions manipulating
values. We will show later that this is not a restriction by
itself since the types do not force the programmer to be precise
everywhere.»
p"forgot to shift?"
«One common kind of programming error with these nameless
representations is to forget to shift the free variables here and
there. While these errors are already caught by the {_Maybe} and the
{_Fin} approaches, in these approaches the programmer is provided
with means to workaround the type error. In complex situations
making the distinction between a valid coercion and a wrong one can
be challenging. With finer types, the mistakes will result in more
informative type errors.»
subsection «A data definition kit»
p"the idea of DataKit"
«The three previous approaches are closely related. Just a few
details change each time. We can capture all of them with a single
abstraction: a triple ({_World}, {_Name}, {_S1}) where {_World} is
the index of types like {_Tm}, {_Name} is the type for names
(indexed by worlds) as used in the {_V} constructor, and finally
{_S1} is an operation to shift a world by one as used in the {ƛ}
constructor.»
p"DataKit in Agda"
«In {_Agda}, this triple can be defined with a record type named
{_DataKit}. This type is made universe polymorphic to accept the
nested data types approach.»
[agdaP|
record DataKit {ℓ} : Set (suc ℓ) where
constructor ⟨_,_,_⟩
field
World : Set ℓ
Name : World → Set
_↑1 : World → World
|]
figure ø «{_DataKit}s for the three previous approaches» kitsF $ do
[agdaP|
bareKit : DataKit
bareKit = ⟨ ⊤ , λ _ → ℕ , id ⟩
maybeKit : DataKit
maybeKit = ⟨ Set , id , Maybe ⟩
finKit : DataKit
finKit = ⟨ ℕ , Fin , suc ⟩
|]
p"kits description"
«The three previous approaches are summed up in figure {ref kitsF} by
defining their {_DataKit}. Note that for the {bare} approach the
index type is the unit type. In the {_Maybe} approach the index type
is {_Set} and the type for names is directly the index so we use the
identity function.»
p"generic Tm"
«We can now give a single definition of {_Tm} generalizing the three
previous ones. To this end, we simply take a {_DataKit} as argument
and use it to define the type {_Tm}.»
-- infixl 4 _·_
[agdaP|
module DataTm {ℓ} (kit : DataKit {ℓ}) where
open DataKit kit
data Tm α : Set ℓ where
V : (x : Name α) → Tm α
_·_ : (t u : Tm α) → Tm α
ƛ : (t : Tm (α ↑1)) → Tm α
Let : (t : Tm α) (u : Tm (α ↑1)) → Tm α
|]
p"the kit is enough"
«We claim that nothing more is required from the kit. As complex
binding structures can be defined in the original nameless
representation ({bare}), they can also be defined using this kit. In
particular having an empty world or making an induction over a world
is not necessary.»
p"translations between kits"
«Translation between data types using different kits can be done
modularly as we do in the {_Agda} development. In any direction (any
pair of kits {agda|k₁|} {agda|k₂|}) one can define a function of
type {agda|∀ {α₁ α₂} → (Name k₁ α₁ → Name k₂ α₂) → Tm k₁ α₁ → Tm k₂
α₂|}. This function takes a mapping for free variables and lifts
this mapping to terms.»
p"initial mapping"
«Whereas using these translations is fine in many cases, when going
from {bare} to a more precise representation, an issue arises. Since
{_Agda} is a total language, the initial mapping must be a total
function. The {bare} approach ensuring nothing about free variables,
one cannot supply the initial mapping to go to a closed term. One
has to keep at least one free variable and then dynamically check
for occurrences of the free variable in a second transformation.»
p"will build on DataKit"
«We will now build on this {_DataKit} abstraction to introduce our
own solution.»
subsectionLbl «{napa} types» napaTypesSection
figure ø «Core types of {napa}» coreTypesF $ do
[agdaP|
World : Set
ø : World
_+1 : World → World
_↑1 : World → World
Name : World → Set
_⊆_ : World → World → Set
napaKit : DataKit
napaKit = ⟨ World , Name , _↑1 ⟩
|]
p"NaPa types description"
«We call our approach {napa} as in {_Nameless_Painless}. At the level
of types, {napa} exposes the interface shown in figure {ref
coreTypesF}. This is a superset of the {_DataKit}, featuring an
empty world, a {_P1} operation on worlds described later on, and a
notion of world inclusion.»
p"too much info"
«If we look closely at the notion of worlds in the {_Fin} approach,
we see that it gives us too much information. Indeed a function
could look at the given world (by pattern-matching or induction) and
behave differently for some values of the world.»
-- Please no Gödel number argument.
p"too coarse"
«On the other hand, {_Fin} worlds are too coarse: a single number
{qm|ℓ|} is used to represent a set, namely the complete interval
{qm|[0 .. ℓ-1]|}.»
p"NaPa worlds"
«In {napa}, a world denotes a subset of {_ℕ} but is kept abstract (no
pattern-matching nor induction). Only the empty world {_ø} and
two operations are given, namely {_P1} and {_S1}. Semantically
{m|α +1|} is defined by {m|{x + 1 | x ∈ α}|} and {m|α ↑1|} by
{m|{0} ∪ (α +1)|}.»
p"Worlds as List Bool"
«Internally we represent worlds by lists of Boolean values. Having
{true} at the {nth} position of the list means that {qm|n|} is in
the world. Here are the {_Agda} definitions:»
[agdaP|
World : Set
World = List Bool
ø : World
ø = []
_+1 : World → World
α +1 = false ∷ α
_↑1 : World → World
α ↑1 = true ∷ α
|]
p"Generalizing ↑1 and +1"
«These one step definitions {_P1} and {_S1} are extended to
any number to produce {op _P} and {op _S} of type
{agda|World → ℕ → World|}.»
p"_+1, _↑1 distinction is new"
«To the best of our knowledge, making the distinction between two
forms of shifting operations for worlds has never been investigated
in the context of representing names and binders.»
p"Name implem"
«In {napa} the type for names is a refinement of {_ℕ}, kept abstract
by not exporting its definition. From a set point of view,
inhabitants of {agda|Name α|} are members of {α}. However we want
worlds to form static information only and to be able to erase them
before running the programs. To do so we will use a pair of a
natural number and a proof it belongs to its world. Here is the
membership predicate and the record definition for names:»
[agdaP|
_∈_ : ℕ → World → Set
_ ∈ [] = ⊥
zero ∈ (false ∷ _) = ⊥
zero ∈ (true ∷ _) = ⊤
suc n ∈ (_ ∷ xs) = n ∈ xs
record Name α : Set where
constructor _,_
field
name : ℕ
name∈α : name ∈ α
|]
-- infixr 4 _,_
p"proof-irrelevance"
«Thanks to our definition of world membership which is canonical,
equality of the {agda|name|} field implies equality on whole {_Name}
values. This means we get provable proof-irrelevance for the {_Name}
type without requiring an additional axiom.»
subsection «Operations on names»
-- the ‽ marks represent half-spaces that should be ignored.
figure ø «Core operations on names» opsfig $ do
[agdaP|
zeroᴺ : ∀ {α} ‽ → Name (α ↑1)
addᴺ : ∀ {α} k ‽ → Name α
→ Name (α +ᵂ k)
subtractᴺ : ∀ {α} k ‽ → Name (α +ᵂ k)
→ Name α
cmpᴺ : ∀ {α} ℓ ‽ → Name (α ↑ ℓ)
→ Name (ø ↑ ℓ)
⊎ Name (α +ᵂ ℓ)
_==ᴺ_ : ∀ {α} (x y : Name α) → Bool
coerceᴺ : ∀ {α β} ‽ → α ⊆ β
→ Name α → Name β
¬Nameø : ¬(Name ø)
syntax addᴺ k x = x +ᴺ k
syntax subtractᴺ k x = x ∸ᴺ k
syntax cmpᴺ ℓ x = x <ᴺ ℓ
|]
p"core operations descriptions"
«The core operations on names are given in figure {ref opsfig}. The
simplest name is {zeroN}, it represents 0 and lives in any world
shifted by one. One can add any constant to a name in any world with
{addN}, the resulting world clearly shows that this function (if
parametric in {α}) does exactly its job. One can do the opposite
operation with {subtractN}. Thanks to its precise type this function
is total and the inverse of {addN}. Figure {ref opsdiag} depict the
core operations we have on names. Starting from the bottom, worlds
of the form {agda|ø ↑ k|} are names which are definitely bound.
There value is completely known as stated by arrows with the
{agda|Fin k|} type. Above we have names that may be bound or free
({agda|Name (α ↑ k)|}), a dynamic test ({cmpN}) can tell whether it
is bound or not. Above we have names that are known to be greater
than {agda|k|} ({agda|Name (α +ᵂ k)|}), apart from that they are
free names. Above we have free names ({agda|Name α|}). On the top we
have impossible names since they are said to belong to an empty
world. From them we can derive everything.»
p"the comparison function"
«Given any world {α}, a name in the world {agda|α ↑ ℓ|} is
either strictly lower than {agda|ℓ|} (and so also lives in
{agda|ø ↑ ℓ|}), or greater or equal to {agda|ℓ|} (thus also lives in
{agda|α +ᵂ ℓ|}). This is exactly what the {cmpN} function is about.
Given a name, it returns a disjoint sum of names which can be read
in two parts. It first gives which side of the disjoint sum it
stands, and second it gives a refined version of the input name.»
p"coerceᴺ, ==ᴺ, and ¬Nameø"
«The {coerceN} function will be described in length in the next
sub-section. The only way left to extract information from a name in
an arbitrary world is to compare it with another name for equality
with {op eqN}. Finally {_Name0} asserts that no name lives in the
empty world. In a total language this is of great use to tackle
impossible cases.»
figure ø «Operations on names» opsdiag $ do
diagram
(completeMat ø
[[[agda|Name (ø +ᵂ k)|]]
,[]
,[[agda|Name ø|]]
,[]
,[[agda|Name α|]]
,[]
,[[agda|Name (α +ᵂ k)|]]
,[]
,[[agda|Name (α ↑ k)|],ø,[agda|cmpᴺ|]]
,[]
,[[agda|Name (ø ↑ k)|],ø,[agda|Fin k|]]
])
[path "->" (1,1) L [agda|coerceᴺ _|] (3,1)
,path "->" (3,1) L [agda|¬Nameø ∘ coerceᴺ _|] (5,1)
,path "->" (5,1) L [agda|addᴺ k|] (7,1)
,path "->" (7,1) R [agda|subtractᴺ k|] (5,1)
,path "->" (9,1) L ø (9,3)
,path "->" (7,1) L [agda|coerceᴺ _|] (9,1)
,path "->" (9,3) R « ({textit «if»} {agda|≥k|})» (7,1)
,path "<-" (9,1) L [agda|coerceᴺ _|] (11,1)
,path "->" (9,3) R « ({textit «if»} {agda|" (11,1) L ø (11,3)]
p"NaPa vs Fin"
«These primitives are enough to show an isomorphism between
{agda|Fin n|} and {agda|Name (ø ↑ n)|}. From this, every program
involving {_Fin} can be translated into our system. This means
that our system does not restrict the programmer more than the
{_Fin} approach. However as soon as one uses finer types than
{agda|Name (ø ↑ n)|}, then fewer ``wrong programs'' type-check and
more properties hold as we will see later.»
subsection «A type for world inclusion witnesses»
p"why _⊆_ and coerceᴺ"
«Having finer types also implies being able to give more types to the
same value. Then cheaply moving from different types is a must. We
call a function which has an output type different from the input
type and behaves as the identity a coercion. To capture a great deal
of coercions from a world {α} to a world {β} we focus on the case
where {α} is included in {β}. In {napa} a type {op incl} is
introduced to witness the inclusion between two worlds. Then the
{coerceN} function turns a {agda| α ⊆ β |} into an identity function
of type {agda|Name α → Name β|}. Here is the {coerceN} function and
its alias {because} which is useful to keep the code separated from
the typing/proof, in particular what is between the angle brackets
can be safely skipped.»
[agdaP|
coerceᴺ : ∀ {α β} → α ⊆ β → Name α → Name β
coerceᴺ α⊆β (x , x∈α) = (x , ⊆-sound α⊆β x x∈α)
infix 0 _⟨-because_-⟩
_⟨-because_-⟩ : ∀{α β}→ Name α → α ⊆ β → Name β
_⟨-because_-⟩ n pf = coerceᴺ pf n
|]
p"on emptiness and (⊆ ø)"
«The inclusion relation also expresses the emptiness of a world {α}
by using {agda|α ⊆ ø|}. We use this definition of emptiness as
opposed to an equality with the empty world for two reasons. First
{_ø} is not the only empty world ({agda|ø +1|} is empty as well).
Second having world equalities would require new definitions and
would be heavy in comparison to the use of inclusions. Combining
{coerceN} and {_Name0} turns any contradiction on names into an
inclusion problem, reusing any automation done on this side.»
[agdaP|
¬Name : ∀ {α} → α ⊆ ø → ¬(Name α)
¬Name α⊆ø = ¬Nameø ∘ coerceᴺ α⊆ø
|]
figure ø «Rules for world inclusion» subfig $ do
[agdaP|
⊆-refl : ∀{α}→ α ⊆ α
⊆-trans : ∀{α β γ}→ α ⊆ β → β ⊆ γ → α ⊆ γ
⊆-ø : ∀{α}→ ø ⊆ α
⊆-ø+1 : ø +1 ⊆ ø
⊆-↑1-↑1 : ∀{α β}→ α ⊆ β ↔ α ↑1 ⊆ β ↑1
⊆-+1-+1 : ∀{α β}→ α ⊆ β ↔ α +1 ⊆ β +1
⊆-+1-↑1 : ∀{α}→ α +1 ⊆ α ↑1
|]
p"⊆ rules"
«We expose the inclusion relation with a set of rules given in
figure {ref subfig}. This states that the inclusion relation is
reflexive, transitive, and has the empty world as lowest element.
The {agda|⊆-ø+1|} rule states that {agda|ø +1|} is empty. The
inclusion is preserved both ways by the contexts {_S1} and {_P1}.
Finally {_P1} can be weakened in {_S1}. This accounts for the
fact that {agda|α ↑1|} means {agda|{0} ∪ (α +1)|} and so is
a superset of {agda|α +1|}. This set of rules has been shown
sound according to a semantic definition of inclusion, namely
{agda|∀ x → x ∈ α → x ∈ β|}. On top of these base rules, we derived
others that we omit to define here but some are used in the code.»
p"⊆-Reasoning"
«Sometimes one has to build complex inclusion witnesses. While
inference would be of great effect here, we propose a modest
syntactic tool to build them, namely the {agda|⊆-Reasoning|} module.
It gives access to the transitivity {agda|⊆-trans|} in a style which
focuses more on the intermediate states of the reasoning rather than
the steps. The syntax is a list of worlds interleaved by inclusion
witnesses, with two {agda|∎|} around the last world. There is
one example of its use in the following section. The code for
{agda|⊆-Reasoning|} is given below for reference and can be safely
skipped.»
[agdaP|
module ⊆-Reasoning where
infix 2 finally
infixr 2 _⊆⟨_⟩_
_⊆⟨_⟩_ : ∀ x {y z} → x ⊆ y → y ⊆ z → x ⊆ z
_ ⊆⟨ x⊆y ⟩ y⊆z = ⊆-trans x⊆y y⊆z
finally : ∀ x y → x ⊆ y → x ⊆ y
finally _ _ x⊆y = x⊆y
syntax finally x y x⊆y = x ⊆⟨ x⊆y ⟩∎ y ∎
|]
subsection «Singleton worlds!»
p"singletons worlds"
«We said that our worlds denote finite subsets of {_ℕ} and are more
precise than in the {_Fin} approach. Actually they can be as precise
as we wish, since any subset of {_ℕ} can be described by our
operations on worlds ({_ø}, {_P1}, and {_S1}). In particular they
can be singleton worlds. From singleton worlds we build singleton
types for names:»
[agdaP|
Worldˢ : ℕ → World
Worldˢ n = ø ↑1 +ᵂ n
Nameˢ : ℕ → Set
Nameˢ = Name ∘ Worldˢ
_ˢ : ∀ n → Nameˢ n
_ˢ n = zeroᴺ +ᴺ n
|]
p"addᴺ & subtractᴺ"
«Singleton worlds not only exist, they are also preserved by our two
updating operations, namely {addN} and {subtractN}.»
[agdaP|
addˢ : ∀ {n} k → Nameˢ n → Nameˢ (k +ℕ n)
addˢ {n} k x = addᴺ k x
⟨-because ⊆-assoc-+ ⊆-refl n k −⟩
subtractˢ : ∀ {n} k → Nameˢ (k +ℕ n) → Nameˢ n
subtractˢ {n} k x = subtractᴺ k x
⟨-because ⊆-assoc-+′ ⊆-refl n k -⟩
|]
section «Using {napa}: examples and advanced operations» usingNaPa
subsection «Some convenience functions»
p"convenience functions description"
«Here are a few functions built on top of the interface
(without using the concrete representation of names). {sucN} is
{agda|addᴺ 1|} and {agda|sucᴺ↑|} is a variant that includes a
coercion from {agda|α +1|} to {agda|α ↑1|}. The function {_N} turns
a number {qm|n|} into a name that inhabits any world with at least
{qm|n + 1|} consecutive binders.»
[agdaP|
sucᴺ : ∀ {α} → Name α → Name (α +1)
sucᴺ = addᴺ 1
sucᴺ↑ : ∀ {α} → Name α → Name (α ↑1)
sucᴺ↑ = coerceᴺ ⊆-+1↑1 ∘ sucᴺ
_ᴺ : ∀ {α} n → Name (α ↑ suc n)
_ᴺ {α} n = zeroᴺ +ᴺ n
⟨-because α ↑1 +ᵂ n ⊆⟨ ⊆-+-↑ n ⟩
α ↑1 ↑ n ⊆⟨ ⊆-exch-↑-↑ 1 n ⟩∎
α ↑ suc n ∎ -⟩
where open ⊆-Reasoning
|]
p"ℓ-bound, ℓ-free"
«We call ℓ-bound, a name bound somewhere in the scope of ℓ binders.
We call ℓ-free, a name free for all ℓ binders. In other words, a de
Bruijn index is ℓ-bound if it is strictly less than ℓ; it is ℓ-free
otherwise.»
p"exportName"
«The {exportName} function tells whether a given name is ℓ-bound or
ℓ-free. In case the name is free, an exported version of it is
returned. This function forms the base case of exporting functions
like {agda|exportTm|} explained later on.»
[agdaP|
-- Partial functions from A to B
A →? B = A → Maybe B
exportName : ∀ {α} ℓ → Name (α ↑ ℓ)
→? Name α
exportName ℓ x
with x <ᴺ ℓ
... | inj₁ _ = nothing
... | inj₂ x′ = just (x′ ∸ᴺ ℓ)
|]
p"shiftName"
«The function {agda|shiftName ℓ k pf|} shifts its argument by
{agda|k|} if this name is ℓ-free, otherwise it leaves the ℓ-bound
name untouched. This function makes use of {cmpN} and coerces the
outputs to the required type. It also perform a coercion on the fly,
giving extra flexibility for free.»
[agdaP|
shiftName : ∀ {α} ℓ k → (α +ᵂ k) ⊆ β
→ Name (α ↑ ℓ)
→ Name (β ↑ ℓ)
shiftName ℓ k pf x
with x <ᴺ ℓ
... | inj₁ x′ = x′
⟨-because pf₁ -⟩
... | inj₂ x′ = x′ +ᴺ k
⟨-because pf₂ -⟩
where
pf₁ = ⊆-cong-↑ ⊆-ø ℓ
pf₂ = ⊆-trans (⊆-exch-+-+ ⊆-refl ℓ k)
‽(⊆-ctx-+↑ pf ℓ)
|]
p"protect↑"
«The {agda|protect↑|} function shifts a name transformer. Let
{agda|f|} be a function from names to names. The function
{agda|protect↑ ℓ f|} is a version of {agda|f|} that is applicable
under {agda|ℓ|} binders. Let {agda|x|} be a name under {agda|ℓ|}
binders. When {agda|x|} is ℓ-bound, it is left untouched by
{agda|protect↑|}. When {agda|x|} is ℓ-free, we can subtract
{agda|ℓ|} to {agda|x|}, give it to {agda|f|}, and then add {agda|ℓ|}
to get the result. By combining {agda|protect↑|} and {agda|addᴺ|}
one obtain an alternative implementation of {agda|shiftName|} called
{agda|shiftName′|}. However {agda|shiftName|} is more efficient
since it avoids to subtracting {agda|ℓ|} to add it back after adding
{agda|k|}.»
[agdaP|
protect↑ : ∀ {α β} ℓ
→ (Name α → Name β)
→ (Name (α ↑ ℓ) → Name (β ↑ ℓ))
protect↑ ℓ f x
with x <ᴺ ℓ
... | inj₁ x′ = x′
⟨-because ⊆-cong-↑ ⊆-ø ℓ -⟩
... | inj₂ x′ = f (x′ ∸ᴺ ℓ) +ᴺ ℓ
⟨-because ⊆-+-↑ ℓ -⟩
shiftName′ : ∀ {α β} ℓ k → (α +ᵂ k) ⊆ β
→ Name (α ↑ ℓ) → Name (β ↑ ℓ)
shiftName′ ℓ k pf = protect↑ (coerceᴺ pf ∘ addᴺ k) ℓ
|]
subsection «Building terms»
p"bulding terms description"
«Building terms in {napa} is as easy as building them in the other
nameless approaches we have seen. The structure is exactly the same,
and the variables are made of numbers (of type {_ℕ}) using {_N}.
Below we define the representation of the identity function as
{agda|idTm|}, the application operator as {agda|appTm|} and finally
the composition function as {agda|compTm|}:»
[agdaP|
idTm : ∀ {α} → Tm α
idTm = ƛ(V (0 ᴺ))
appTm : ∀ {α} → Tm α
appTm = ƛ(ƛ(V (1 ᴺ) · V (0 ᴺ)))
compTm : ∀ {α} → Tm α
compTm = ƛ(ƛ(ƛ(V (2 ᴺ)) · (V (1 ᴺ) · V (0 ᴺ)))))
|]
newpage
subsection «Computing free variables»
p"fv description"
«Our first example of functions over terms simply computes the list
of free variables in the input term. The {agda|fv|} function
below, while straightforward, has the subtle cases of binding
constructs ({ƛ} and {_Let}). In these cases we have to remove the
bound variable from the list of free variables given by the
recursive call. In this nameless representation this amounts to
removing occurrences of {qm|0|} and subtract {qm|1|} to other name
occurrences. This is done by the function {agda|rm₀| which calls
{agda|exportName 1|} on each element of the list and merges the
results. Note that forgetting to remove the bound variable will
result in a type error. In the same vein the typing of {agda|fv|}
ensures that all returned variables do appear free in the given
term.»
[agdaP|
rm₀ : ∀ {α} → List (Name (α ↑1))
→ List (Name α)
rm₀ [] = []
rm₀ (x ∷ xs) with exportName 1 x
... | just x' = x' ∷ rm₀ xs
... | nothing = rm₀ xs
fv : ∀ {α} → Tm α → List (Name α)
fv (V x) = [ x ]
fv (fct · arg) = fv fct ++ fv arg
fv (ƛ t) = rm₀ (fv t)
fv (Let t u) = fv t ++ rm₀ (fv u)
|]
subsection «Generic traversal»
p"TraverseTm"
«In order to build multiple traversal functions at once, we
first define a generic function based on ideas from {cite
[mcbridepaterson08]}. It is essentially a map/subst function where
the free variables are transformed by a user-supplied function.
Moreover a class of effects (an applicative functor) is allowed
during the traversal. An applicative functor is halfway between a
functor and a monad. Like a monad, an applicative functor has a unit
called {agda|pure|}. It allows to embed any pure value as a
potentially effectful one. The second operation called {agda|_⊛_|}
is an effectful application, taking both an effectful function and
argument and resulting in an effectful result.»
[agdaP|
module TraverseTm
{E} (E-app : Applicative E)
{α β} (trName : ∀ ℓ → Name (α ↑ ℓ)
→ E (Tm (β ↑ ℓ)))
where
open Applicative E-app
tr : ∀ ℓ → Tm (α ↑ ℓ) → E (Tm (β ↑ ℓ))
tr ℓ (V x) = trName ℓ x
tr ℓ (t · u) = pure _·_ ⊛ tr ℓ t ⊛ tr ℓ u
tr ℓ (ƛ t) = pure ƛ ⊛ tr (suc ℓ) t
tr ℓ (Let t u) = pure Let ⊛ tr ℓ t
⊛ tr (suc ℓ) u
trTm : Tm α → E (Tm β)
trTm = tr 0
|]
p"trTm′"
«To put this traversal at work we successively instantiate some of
its arguments. For instance you may have noticed the special case we
made for variables. Mapping names to terms will bring us capture
avoiding substitution almost for free. However, in the mean time we
build {agda|trTm′|} which maps names to names. It does so by
applying {agda|pure V|} to the name to name function:»
[agdaP|
open TraverseTm
trTm′ :
∀ {E} (E-app : Applicative E) {α β}
(trName : ∀ ℓ → Name (α ↑ ℓ)
→ E (Name (β ↑ ℓ)))
→ Tm α → E (Tm β)
trTm′ E-app trName
= trTm E-app (λ ℓ x → pure V ⊛ trName ℓ x)
where open Applicative E-app
|]
paragraph «Renaming functions»
p"renameTm, renameTm?"
«In many functions over terms the handling of variables shares a
common part. Given a variable under {agda|ℓ|} binders, we test if
the variable is ℓ-bound. If so we leave it untouched, otherwise we
subtract {agda|ℓ|} and go on a specific processing after which
we add {agda|ℓ|} again to the free variables of the result.
The traversal function is augmented by this processing of bound
variables to build {agda|renameTmA|}. Then by picking either the
identity functor ({agda|id-app|}), or the {_Maybe} one we build two
functions (a total and a partial one) to perform renamings, namely
{agda|renameTm|} and {agda|renameTm?|}:»
[agdaP|
renameTmA : ∀ {E} (E-app : Applicative E)
{α β} (θ : Name α → E (Name β))
→ Tm α → E (Tm β)
renameTmA E-app θ
= trTm′ E-app (protect↑A E-app θ)
|]
[agdaP|
renameTm : ∀ {α β} → (Name α → Name β)
→ Tm α → Tm β
renameTm θ = trTm′ id-app (protect↑ θ)
-- or
-- renameTm = renameTmA id-app
|]
[agdaP|
renameTm? : ∀ {α β} → (Name α →? Name β)
→ Tm α →? Tm β
renameTm? = renameTmA Maybe.applicative
|]
paragraph «Lifting name functions»
p"addTm, subtractTm"
«Any operation on names can now be lifted to terms:»
[agdaP|
addTm : ∀ {α} k → Tm α → Tm (α +ᵂ k)
addTm = renameTm ∘ addᴺ
subtractTm : ∀ {α} k → Tm (α +ᵂ k) → Tm α
subtractTm = renameTm ∘ subtractᴺ
exportTm? : ∀ {α} ℓ → Tm (α ↑ ℓ) →? Tm α
exportTm? = renameTm? ∘ exportName
|]
p"coerceTm"
«While {coerceN} can be lifted to terms in the same way, using
{agda|trTm′|} directly enables to by-pass the {agda|protect↑|}
dynamic tests and directly ``protect'' the inclusion witness with an
appropriate inclusion rule.»
[agdaP|
coerceTm : ∀ {α β} → α ⊆ β → Tm α → Tm β
coerceTm pf = trTm′ id-app (coerceᴺ ∘ ⊆-cong-↑ pf)
-- or less efficiently:
-- coerceTm = renameTm ∘ coerceᴺ
|]
p"shiftTm"
«Lifting {agda|addᴺ|} to terms can be done more efficiently (than
using {agda|protect↑|}) as well. Here the dynamic test performed by
{agda|protect↑|} is necessary. However when the name is ℓ-free we
subtract ℓ to add it back after adding {agda|k|}. The function
{agda|shiftName|} avoids this extra computation, hence the following
{agda|shiftTm|}:»
[agdaP|
shiftTm : ∀ {α β} k → (α +ᵂ k)⊆ β → Tm α → Tm β
shiftTm k p = trTm′ id-app (λ ℓ → shiftName ℓ k p)
-- or less efficiently:
-- shiftTm k pf = renameTm (coerceᴺ pf ∘ addᴺ k)
|]
p"closeTm?"
«A special case of {agda|renameTm?|} is the so-called
{agda|closeTm?|}. This function takes a term in any world and checks
if the term is closed. If so, the same term is returned in the empty
world. Otherwise the function fails by returning {agda|nothing|}:»
[agdaP|
closeTm? : ∀ {α} → Tm α →? Tm ø
closeTm? = renameTm? (const nothing)
|]
paragraph «Capture avoiding substitution»
p"substVar"
«To implement capture avoiding substitution for the {_Tm} type we
solely need a specific {agda|trName|} function for {agda|trTm|}.
Here substitutions are represented as functions from names to terms.
The function {agda|substVarTm|} handles the case for variables. This
function is very close to {agda|protect↑|} but extended to functions
returning terms.»
[agdaP|
substVarTm : ∀{α β} → (Name α → Tm β) →
∀ ℓ → Name (α ↑ ℓ) → Tm (β ↑ ℓ)
substVarTm f ℓ x
with x <ᴺ ℓ
... | inj₁ x′ = V (x′
⟨-because ⊆-cong-↑ ⊆-ø ℓ -⟩)
... | inj₂ x′ = shiftTm ℓ (⊆-+-↑ ℓ) (f (x′ ∸ᴺ ℓ))
|]
p"substTm"
«The main function {agda|substTm|} instantiates {agda|trTm|} with
the identity applicative functor and {agda|substVarTm|}:»
[agdaP|
substTm : ∀ {α β} → (Name α → Tm β)
→ Tm α → Tm β
substTm = trTm id-app ∘ substVarTm
|]
p"β-red"
«As an illustration, the function {agda|β-red|} takes the body of a
λ-abstraction and calls {agda|substTm|} with the substitution that
replaces 0 with a received replacement term:»
[agdaP|
β-red : ∀ {α} → Tm (α ↑1) → Tm α → Tm α
β-red {α} f a = substTm (φ ∘ exportName 1) f
where φ : Maybe (Name α) → Tm α
φ (just x) = V x
φ nothing = a
|]
subsection «Deciding term {α}-equivalence»
p"αEq type"
«Our next example focuses on comparison of terms. We first define
{agda|αEq|}, where {agda|αEq F|} is the type of functions comparing
{agda|F|} structures.»
[agdaP|
αEq : (F : World → Set) (α β : World) → Set
αEq F α β = F α → F β → Bool
|]
p"αeqName"
«We show that all the subtle work is done at the level of names in a
separate and reusable function called {agda|αeqName|}. This function
takes a function that compares two free names and builds one that
compares two names under {agda|ℓ|} bindings. It does so by comparing
both of them to{(∼)}{agda|ℓ|}. If they are both bound they can be
safely compared using {op eqN} since they now are of the same type.
If they are both free, they can be compared using the function
received as argument. Otherwise they are different.»
[agdaP|
αeqName : ∀ {α β} ℓ → αEq Name α β
→ αEq Name (α ↑ ℓ) (β ↑ ℓ)
αeqName ℓ Γ x y with x <ᴺ ℓ | y <ᴺ ℓ
... | inj₁ x′ | inj₁ y′ = x′ ==ᴺ y′
... | inj₂ x′ | inj₂ y′ = Γ (x′ ∸ᴺ ℓ) (y′ ∸ᴺ ℓ)
... | _ | _ = false
|]
p"αeqTm"
«The {agda|αeqTm|} function structurally compares two terms in a
simple way, only keeping track of the number of traversed binders
and calling {agda|αeqName|} at variables.»
[agdaP|
αeqTm : ∀ {α β} → αEq Name α β → αEq Tm α β
αeqTm {α} {β} Γ = go 0 where
go : ∀ ℓ → αEq Tm (α ↑ ℓ) (β ↑ ℓ)
go ℓ (V x) (V y) = αeqName ℓ Γ x y
go ℓ (t · u) (v · w) = go ℓ t v ∧ go ℓ u w
go ℓ (ƛ t) (ƛ u) = go (suc ℓ) t u
go ℓ (Let t u) (Let v w) = go ℓ t v
∧ go (suc ℓ) u w
go _ _ _ = false
|]
section «Soundness using logical relations» soundness
p"why using logical relations?"
«Since our library is written in a type-safe language, one may wonder
what soundness properties are to be proved. Moreover our names are
indexed by worlds and hold membership proofs. The functions over
names are given precise types and have been shown to be type-safe.
However we still wish to show that our library respects a model of
good behavior with respect to names and binders. Our model is based
on logical relations indexed/directed by types. This technique
{cite[bernardy10]} is independent of this work and enables to define
a notion of program equivalence. We use this technique to capture
good behavior of functions involving names and binders. Using this
technique, the set of specific definitions is kept to a minimum of
one per introduced type ({_World}, {_Name}, and {op incl}). One
proof per value introduced has to be done, which keeps the
development modular and forward-compatible to the addition of more
features.»
p"plan"
«This section is organized as follows. First we recall the basics of
logical relations. Then we give a toy example to practice a bit.
Then relations for worlds, names, and world inclusions are given.
Finally we make use of the construction to obtain free theorems
{cite[wadlerfree89]} about world-polymorphic functions over the
{_Tm} type.»
subsection«Recap of the framework»
p"type-directed relation"
«A relation is said to be type-directed when it is recursively
defined on the structure of types. Let {_ℛ} be such a type-directed
relation, and let {τ} be a type. Then, {_ℛτ} is a relation on values
of type {τ}, namely {_ℛτ} {agda|: τ → τ → Set|}. Recall that {_Set}
is also the type of propositions in {_Agda}.»
p"logical"
«A type-directed relation is called ``logical'' when the case for
functions is defined extensionally. Here extensionally means that
two functions are related when they produce related results out of
related arguments. Let {agda|Aᵣ|} be a relation for the arguments
and {agda|Bᵣ|} a relation for results. Two functions {agda|f₁|} and
{agda|f₂|} are related if and only if for every pair of arguments
{agda|(x₁, x₂)|} related by {agda|Aᵣ|}, the results {agda|f₁ x₁|}
and {agda|f₂ x₂|} are related by {agda|Bᵣ|}. This definition can be
given in {_Agda} as well:»
[agdaP|
RelatedFunctions Aᵣ Bᵣ f₁ f₂ =
∀ {x₁ x₂} → Aᵣ x₁ x₂
→ Bᵣ (f₁ x₁) (f₂ x₂)
|]
p"name conventions"
«We say that a program or a value fits a logical relation when it is
related to itself by the relation indexed by its type. We say that a
logical relation is universal if every well-typed program fits the
logical relation. This notion of universality was originally coined
by John Reynolds as the ``Abstraction Theorem'' {cite[reynolds83]}.
We call the ``{_Agda} logical relation'' the one defined by Bernardy
et al. {cite[bernardy10]} for a {_PTS} (pure type system) and
naturally extended as they suggest to other features of {_Agda}.
While no complete mechanized proof has been done for this we will
consider the {_Agda} logical relation as universal.»
p"no universe-polymorphism"
«To simplify matters, the definitions shown here are not universe
polymorphic. You can find universe-polymorphic definitions in our
complete {_Agda} development {cite[napacode]}.»
p"the universe technique"
«To formally define a logical relation indexed by types, a
common technique is to first inductively define the structure
of types. This is known as a ``universe of codes'' {_U}.
Then one defines a function called {_El} from codes to types.
Finally one defines by induction a function called {rel __} from
codes to relations on elements of type described by the given
code. In {_Agda} the {rel __} function has the following type:
{agda|(τ : U) → El τ → El τ → Set|}. Because, when types contain
variables, a good deal of complexity is added to this scheme, we opt
for a lighter scheme. We do not define {_U}, {_El}, and {rel __}.»
p"⟦Π⟧"
«Instead, for each type constructor {κ}, we define a relation {rel κ}
For the function type constructor the {agda|RelatedFunctions|}
definition above is a good start. Actually this is a fine
definition for non-dependent functions. The dependent version
of {agda|RelatedFunctions|}, called {agda|⟦Π⟧|} here, passes the
relation argument {agda|Aᵣ x₁ x₂|} called {agda|xᵣ|} to the relation
for results {agda|Bᵣ|}. In short the relation for results now
depends on the relation for arguments. Here is the definition in
{_Agda}:»
[agdaP|
⟦Π⟧ Aᵣ Bᵣ f₁ f₂ = ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂)
→ Bᵣ xᵣ (f₁ x₁) (f₂ x₂)
|]
p"⟦→⟧, ⟦∀⟧, and ⟦Set₀⟧"
«Note that this definition generalizes the case of non-dependent
functions and universal quantifications as well. For non-dependent
functions we simply provide a relation for results which ignores its
first argument (equivalent to {agda|RelatedFunctions|} and noted
{agda|_⟦→⟧_|} from now on). For universal quantifications, since the
arguments are types, all we need is a relation for types (members of
{_Set0}) themselves. Following our convention we call this relation
{rel _Set0}, its definition is the set of relations between its
arguments:»
[agdaP|
⟦Set₀⟧ : Set₀ → Set₀ → Set₁
⟦Set₀⟧ A₁ A₂ = A₁ → A₂ → Set₀
|]
p"⟦_⟧ as a macro"
«For reference, full definitions for core type theory are given in
figure {ref rellogfig}. We now have all the building blocks of the
meta-function {rel __} and we will not materialize it more here. We
will apply the {rel __} function manually. To this end it suffices
to replace each constructor {κ} by {rel κ}, each non dependent
arrow by {agda|⟦→⟧|}, each dependent arrow {agda|(x : A) → B|} by
{agda|⟨ xᵣ ∶ ⟦ A ⟧ ⟩⟦→⟧ ⟦ B ⟧|}. By convention we subscript the
variables by {agda|r|}. Applications are translated to applications.
Because of dependent types, this translation has to be extended to
all terms but we will not do it here. Finally here are a few
examples of the manual use of the {rel __} function:»
[agdaP|
⟦ ℕ → ℕ → Bool ⟧ =
⟦ℕ⟧ ⟦→⟧ ⟦ℕ⟧ ⟦→⟧ ⟦Bool⟧ =
λ f₁ f₂ →
∀ {x₁ x₂} (xᵣ : ⟦ℕ⟧ x₁ x₂)
{y₁ y₂} (yᵣ : ⟦ℕ⟧ y₁ y₂)
→ ⟦Bool⟧ (f₁ x₁ y₁) (f₂ x₂ y₂)
|]
[agdaP|
⟦ (A : Set₀) → A → A ⟧ =
⟦Π⟧ ⟦Set₀⟧ (λ Aᵣ → Aᵣ ⟦→⟧ Aᵣ) =
λ f₁ f₂ →
∀ {A₁ A₂} (Aᵣ : A₁ → A₂ → Set₀)
{x₁ x₂} (xᵣ : Aᵣ x₁ x₂)
→ Aᵣ (f₁ A₁ x₁) (f₂ A₂ x₂)
|]
[agdaP|
-- Using the notation instead of ⟦Π⟧:
⟦ (A : Set₀) → List A ⟧ =
⟨ Aᵣ ∶ ⟦Set₀⟧ ⟩⟦→⟧ ⟦List⟧ Aᵣ =
λ l₁ l₂ →
∀ {A₁ A₂} (Aᵣ : A₁ → A₂ → Set₀)
→ ⟦List⟧ Aᵣ (l₁ A₁) (l₂ A₂)
|]
figure (★) «Logical relations for core types» rellogfig $ do
[agdaP|
⟦Set₀⟧ : ∀ (A₁ A₂ : Set₀) → Set₁
⟦Set₀⟧ A₁ A₂ = A₁ → A₂ → Set₀
⟦Set₁⟧ : ∀ (A₁ A₂ : Set₁) → Set₂
⟦Set₁⟧ A₁ A₂ = A₁ → A₂ → Set₁
_⟦→⟧_ : ∀ {A₁ A₂ B₁ B₂} → ⟦Set₀⟧ A₁ A₂ → ⟦Set₀⟧ B₁ B₂ → ⟦Set₀⟧ (A₁ → B₁) (A₂ → B₂)
Aᵣ ⟦→⟧ Bᵣ = λ f₁ f₂ → ∀ {x₁ x₂} → Aᵣ x₁ x₂ → Bᵣ (f₁ x₁) (f₂ x₂)
infixr 0 _⟦→⟧_
⟦Π⟧ : ∀ {A₁ A₂} (Aᵣ : ⟦Set₀⟧ A₁ A₂)
{B₁ B₂} (Bᵣ : (Aᵣ ⟦→⟧ ⟦Set₀⟧) B₁ B₂)
→ ((x : A₁) → B₁ x) → ((x : A₂) → B₂ x) → Set₁
⟦Π⟧ Aᵣ Bᵣ = λ f₁ f₂ → ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → Bᵣ xᵣ (f₁ x₁) (f₂ x₂)
syntax ⟦Π⟧ Aᵣ (λ xᵣ → f) = ⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ f
⟦∀⟧ : ∀ {A₁ A₂} (Aᵣ : ⟦Set₀⟧ A₁ A₂)
{B₁ B₂} (Bᵣ : (⟦Set₀⟧ ⟦→⟧ ⟦Set₀⟧) B₁ B₂)
→ ⟦Set₁⟧ ({x : A₁} → B₁ x) ({x : A₂} → B₂ x)
⟦∀⟧ Aᵣ Bᵣ = λ f₁ f₂ → ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → Bᵣ xᵣ (f₁ {x₁}) (f₂ {x₂})
syntax ⟦∀⟧ Aᵣ (λ xᵣ → f) = ∀⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ f
|]
p"relations for data types"
«We now have the definition of the {_Agda} logical relation for the
core type theory part. It extends nicely to inductive data types and
records. The process is as follows: for each constructor {κ} of
type {(∼)}{τ}, declare a new constructor {rel κ} whose type is
{agda|⟦ τ ⟧ κ κ|}. This process applies to type constructors and
data constructors of data types, and type constructors and fields of
record types. For reference, the logical relations for data types we
use in this development are in figure {ref datarelfig}.»
figure ø «Logical relations for data types» datarelfig $ do
[agdaP|
data ⟦⊥⟧ : ⟦Set₀⟧ ⊥ ⊥ -- no constructors
data ⟦Bool⟧ : ⟦Set₀⟧ Bool Bool where
⟦true⟧ : ⟦Bool⟧ true true
⟦false⟧ : ⟦Bool⟧ false false
data ⟦ℕ⟧ : ⟦Set₀⟧ ℕ ℕ where
⟦zero⟧ : ⟦ℕ⟧ zero zero
⟦suc⟧ : (⟦ℕ⟧ ⟦→⟧ ⟦ℕ⟧) suc suc
data _⟦⊎⟧_ {A₁ A₂ B₁ B₂} (Aᵣ : ⟦Set₀⟧ A₁ A₂)
(Bᵣ : ⟦Set₀⟧ B₁ B₂) :
A₁ ⊎ B₁ → A₂ ⊎ B₂ → Set₀ where
⟦inj₁⟧ : (Aᵣ → Aᵣ ⟦⊎⟧ Bᵣ) inj₁ inj₁
⟦inj₂⟧ : (Bᵣ → Aᵣ ⟦⊎⟧ Bᵣ) inj₂ inj₂
|]
subsection «An example: booleans represented by numbers»
p"describe our bool as ℕ example"
«We wish to explain how logical relations can help build a safe
interface to an abstract type. To do so we introduce a tiny example
about booleans represented using natural numbers. We want {qm|0|}
to represent {false} and any other number to represent {true}.
Therefore the boolean disjunction can be implemented using addition.
We show that logical relations help build a model, ensure that a
given implementation respects this model, and finally show that a
client that uses only the interface will also respect the model.»
p"toy however"
«Note however that this is a toy example in several ways. There are
no polymorphic functions in the interface, so no interesting free
theorems are to be expected. While we could prove the safety by
defining a representation predicate in unary style, the logical
relations approach is different. It relies on comparing concrete
data as opposed to mapping to abstract data. The unary construction
would allow for a simpler construction, however this oversimplifies
the problem here and would be no longer useful for proving {napa}.»
p"description of B implem"
«Our tiny implementation of booleans using natural numbers is given
below. It contains a type {_B} that we want to keep abstract.
It contains obvious definitions for {true}, {false}, and the
disjunction {op(∨)}. It intentionally has a dubious function {is42}
which breaks our still informal expectations from such a module.»
[agdaP|
B : Set
B = ℕ
false : B
false = 0
true : B
true = 1
|]
[agdaP|
_∨_ : B → B → B
m ∨ n = m + n
|]
[agdaP|
is42? : B → B
is42? 42 = true
is42? _ = false
|]
p"introduce ⟦B⟧"
«The next step is to define our expectations. To do so, we give a
binary relation which tells when two {_B} values have the same
meaning. We do so with an (inductive) data type named {rel _B} which
states that {qm|0|} is related only with itself, and that any two
non zero numbers are related:»
[agdaP|
data ⟦B⟧ : B → B → Set where
⟦false⟧ : ⟦B⟧ 0 0
⟦true⟧ : ∀ {m n} → ⟦B⟧ (suc m) (suc n)
|]
p"plugging ⟦B⟧"
«When plugged into the machinery of logical relations this single
definition suffices to define a complete model of well-typed
programs. However, the plumbing requires some care. While the
{_Agda} logical relation is universal, we have no such guarantee
about the {_Agda} logical relation where the relation for {_B} is no
longer {agda|⟦ℕ⟧|} but {rel _B}. Fortunately changing the relation
at a given type ({_B} here) can be done safely. All we have to do is
to consider programs abstracted away from {_B} and its operations:
{true}, {false} and {op(∨)}. This can be done either through a
mechanism for abstract types, or by requiring the client to be a
function taking the implementation for {_B} and its operations as
argument.»
p"proof obligations when plugging ⟦B⟧"
«However to use {rel _B} as the relation for {_B}, we have to show
that the definitions which make use of the representation of {_B}
actually fit the relation. Since {rel true} and {rel false} are
obvious witnesses for {true} and {false}, only {op(∨)} and {is42}
are left to be proved. Each time the goal to prove is mechanical:
wrap the type with {agda|⟦·⟧|} on each constructor and put the name
of the function twice to state we want it to be related to itself.
Here is the definition for {op(rel(∨))}:»
[agdaP|
_⟦∨⟧_ : (⟦B⟧ ⟦→⟧ ⟦B⟧ ⟦→⟧ ⟦B⟧) _∨_ _∨_
|]
p"_⟦∨⟧_'s type, description"
«The type of {op(rel(∨))} means that given inputs related in the
model, the results are related in the model as well. Once unfolded
the type looks like:»
[agdaP|
_⟦∨⟧_ : ∀ {x₁ x₂} (xᵣ : ⟦B⟧ x₁ x₂)
{y₁ y₂} (yᵣ : ⟦B⟧ y₁ y₂)
→ ⟦B⟧ (x₁ ∨ y₁) (x₂ ∨ y₂)
|]
p"_⟦∨⟧_ description"
«The fact that input arguments come as implicit arguments will
greatly shorten definitions. Now, thanks to the inductive definition
of {op plus}, simply pattern-matching on the first relation suffices
to reduce the goal, and allows this nice looking definition where we
see the usual lazy definition of the left biased disjunction:»
[agdaP|
⟦false⟧ ⟦∨⟧ x = x
⟦true⟧ ⟦∨⟧ _ = ⟦true⟧
|]
p"¬⟦is42?⟧ description"
«Let us now consider a proof for the {is42} function. Fortunately
there is no such proof since this function gladly breaks the
intended abstraction. Instead we simply prove its negation
by exhibiting that given two related inputs ({qm|42|} and
{qm|27|}) we get non related outputs ({agda|is42? 42 = 1|} and
{agda|is42? 27 = 0|}).»
[agdaP|
¬⟦is42?⟧ : ¬((⟦B⟧ ⟦→⟧ ⟦B⟧) is42? is42?)
¬⟦is42?⟧ ⟦is42?⟧ with ⟦is42?⟧ {42} {27} ⟦true⟧
... | () -- absurd
|]
p"model vs interface only"
«Note that {is42} is rejected by our model with no considerations
about the other exported functions. Indeed with another
implementation of {op(∨)} there would be no way to produce {qm|42|}
and so no way to expose the wrong behavior of {is42} using the
interface. Using a model provides a better forward compatibility and
enables proofs to be done in a modular way.»
subsection «Relations for {napa}»
p"same process as for B"
«For {napa}, we apply the same process as with booleans. We
define our expectations, by defining relations for introduced
types (worlds, names, and inclusions). Finally we prove that each
value/function exported fits the relation.»
subsubsection «Relations for {napa} types»
p"functional and injective"
«Valid names are those which belong to their worlds, names with the
same meaning are those related by the relation between their worlds.
What matters is not just the fact that two worlds are related, but
``how'' they are related. Indeed this will dictate when two names
are related. We need to define a set of valid relations between
worlds. The more relations are accepted, the more power it gives to
the free theorems of world-polymorphic functions. However we want
the equality test on names to be accepted. Thus we at least need
the relation to preserve name equalities across the relation in
both directions. We require these relations to be functional and
injective:»
[agdaP|
FunctionalAndInjective ℛ =
∀ x₁ y₁ x₂ y₂ → ℛ x₁ x₂ → ℛ y₁ y₂
→ x₁ ≡ y₁ ↔ x₂ ≡ y₂
|]
pt"⟦World⟧ and ⟦Name⟧"
«The relation {rel _World} between two worlds {agda|α₁|} and
{agda|α₂|} is the set of functional and injective relations between
{agda|Name α₁|} and {agda|Name α₂|}. Then, two names {agda|x|}
(in {agda|α₁|}) and {agda|y|} (in {agda|α₂|}) are related by
{agda| ⟦Name⟧ αᵣ |} if and only if they are related by the
{agda|αᵣ|} relation.»
p"_⟦⊆⟧_"
«For the {op.rel$incl} relation, we exploit the fact there is only
one way to use an inclusion witness, namely {coerceN}. Thus, for the
purpose of building the model, we identify inclusions with their use
in {coerceN}. Put differently, whatever the representation for
inclusions is, the model takes them as functions from names to
names. Yet another way to look at it is from the perspective of
relation inclusions. A relation {_ℛ1} is included in a relation
{_ℛ2} if and only if all pairs related by {_ℛ1} are related by {_ℛ2}
as well. The {coerceN} function behaving like the identity function
all these definitions coincide. For instance if we expand the
definitions for {rel _Name} and {agda|⟦→⟧|}, we get the definition
for relation inclusion modulo the coercions:»
[agdaP|
_⟦⊆⟧_ αᵣ βᵣ p₁ p₂
= ∀ {x₁ x₂} → (x₁ , x₂) ∈ αᵣ
→ (coerceᴺ p₁ x₁ , coerceᴺ p₂ x₂) ∈ βᵣ
|]
figure ø «Relations for {napa} types» coreTypesRelF $ do
[agdaP|
record ⟦World⟧ α₁ α₂ : Set where
constructor _,_
field
ℛ : Name α₁ → Name α₂ → Set
ℛ-fun-inj : FunctionalAndInjective ℛ
⟦Name⟧ : (⟦World⟧ ⟦→⟧ ⟦Set₀⟧) Name Name
⟦Name⟧ (ℛ , _) x₁ x₂ = ℛ x₁ x₂
_⟦⊆⟧_ : (⟦World⟧ ⟦→⟧ ⟦World⟧ ⟦→⟧ ⟦Set₀⟧)
_⊆_ _⊆_
_⟦⊆⟧_ αᵣ βᵣ α₁⊆β₁ α₂⊆β₂
= (⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ βᵣ) (coerceᴺ α₁⊆β₁)
(coerceᴺ α₂⊆β₂)
|]
pt"world operation lemmas"
«We now have to define operations on worlds that fit the logical
relation. The case for {rel _ø} is trivial. Then {m|αᵣ ⟦+1⟧|} is
defined by {m| { (x+1, y+1) | (x, y) ∈ αᵣ } |} and {agda|αᵣ ⟦↑1⟧|}
is defined by {m| {(0, 0)} ∪ αᵣ ⟦+1⟧ |}. We shown that both
operations preserve functionality and injectiveness. Here are the
signatures that these operations fit the relation:»
[agdaP|
⟦ø⟧ : ⟦World⟧ ø ø
_⟦+1⟧ : (⟦World⟧ ⟦→⟧ ⟦World⟧) _+1 _+1
_⟦↑1⟧ : (⟦World⟧ ⟦→⟧ ⟦World⟧) _↑1 _↑1
|]
subsubsection «{napa} values fit the relation»
p"zeroᴺ, addᴺ, subtractᴺ, and ¬Nameø"
«We now give a short overview of the proofs needed to show that
our functions fit the relation. Thanks to the definition of
{_S1Rel}, {zeroN} fits the relation by definition. Thanks to the
definition of {_P1Rel}, {agda|addᴺ 1|} and {agda|subtractᴺ 1|} fit
the relation as well. These two are later extended to {agda|addᴺ k|}
and {agda|subtractᴺ k|} by an induction on {agda|k|}. Since
{agda|⟦¬Nameø⟧|} receives names in the empty world, it trivially
holds. Here is for instance the type signature for {rel addN}:»
-- ‽ is a half-space
[agdaP|
⟦addᴺ⟧ : ‽(∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧
⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧
⟦Name⟧ αᵣ ⟦→⟧
⟦Name⟧ (αᵣ ⟦+ᵂ⟧ kᵣ)) addᴺ addᴺ
|]
p"==ᴺ"
«For {op.rel$eqN}, once unfolded, the statement tells that the
equality test commutes with a renaming. This means that the
result of the equality test does not change when its inputs are
consistently renamed. The proof for {op.rel$eqN} is done in two
parts. First, we have to relate the Boolean-valued function {op eqN}
to the fact it decides equality on names. Second, we make use of the
two properties (functionality and injectiveness) of the relation
between the two worlds.»
p"cmpᴺ"
«The definition of {cmpN} is not a simple induction on its first
argument. It calls {op le} (which does an induction) and returns a
Boolean value. Based on this Boolean value, the function {cmpN}
returns either {inj1} or {inj2} (the constructors of {op _Either})
with the same name (with a different proof). To prove {op.rel$cmpN}
we show the equivalence with a simpler inductive function and show
that this simpler function is in the relation. Thanks to the
extensionality of the logical relation, no additional axiom is
required to show that {cmpN} fits the relation.»
p"coerceᴺ and ⊆ rules"
«Thanks to the definition of {op.rel$incl}, the proof that {coerceN}
fits the relation is a simple application of the hypotheses. Then
the real job is to show that all the inclusion rules fit the
relation. This means that they all behave as the identity function.
All eleven rules stated in figure {ref subfig} have been shown to
fit the relation.»
newpage
subsection «On the strength of free theorems»
p"free theorems"
«Every well-typed function comes with a free theorem
{cite[wadlerfree89]}. However depending on the type of the function
the strength of the theorem varies a lot. For instance at
type {agda|Int → Bool|} it says no more than the function is
deterministic. At type {agda| ∀{A : Set} → A → A|} it says that the
function behaves like the identity function, which is much stronger.
We now give a few elements of what can affect the strength of free
theorems in our context. We will continue to use our {_Tm} type to
represent some data structures with names and binders but it could
be any other.»
paragraph «Various term types»
p"the weakest"
«The weakest type we can give to a value with names and binders is
{agda|Tm (ø ↑ ℓ)|} for a given {agda|ℓ|}. Such a term can have a
statically unknown number of distinct free variables, but we know
that these variables are comprised in the interval {qm|[0 .. ℓ-1]|}.
The free theorem of {agda|∀{ℓ} → Tm (ø ↑ ℓ) → Tm (ø ↑ ℓ)|} says no
more than ``the function is deterministic''. We also know because of
typing that the resulting term cannot have ℓ-free occurrences.»
p"Tm (α ↑ ℓ)"
«A stronger type is to use any world instead of the empty
world, but still have a known amount of bindings. A function of
type {agda|∀{α ℓ} → Tm (α ↑ ℓ) → Tm (α ↑ ℓ)|} has a stronger free
theorem. It says that the function commutes with a renaming of the
variables in the world {α} (section {ref paramSection}). This is a
common type to deal with open terms under a partial environment:
{agda|∀{α ℓ} → Vec Info ℓ → Tm (α ↑ ℓ) → Tm (α ↑ ℓ)|}.»
p"Tm α"
«The strongest type for terms is to make no assumptions on their free
variables. This can be done by quantifying by an arbitrary world.
The free theorem associated with the type {agda|∀ {α} → Tm α →
Tm α|} says that the function commutes with renamings of the free
variables. This particular type is studied in detail in the section
{ref paramSection}.»
paragraph «Extra arguments»
p"extra arguments"
«Note that adding extra arguments to a function can drastically
affect the strength of its free theorem. An extreme example is the
type {agda|∀{α} → (α ≡ ø) → Tm α → Tm α|}, which is ruined by its
{agda|α ≡ ø|} argument. While the above example is extreme, this is
an important point to watch out for when adding extra arguments to a
function. Another example is the type {agda|∀{α β} → Tm α → Tm β →
Tm β|} versus {agda|∀{α β} → (Name α → Name β → Bool) → Tm α → Tm β →
Tm β|}, the first one cannot compare the free variables of the two
given terms while the second can apply a user-supplied function to do
so.»
paragraph «Shifting versus adding»
p"↑ versus +ᵂ"
«Last but not least using {_P} instead of {_S} significantly improves
the strength of the associated free theorem. Consider the function:»
[agdaP|
protectedAdd : ∀ {α} ℓ k → Name (α ↑ ℓ)
→ Name (α +ᵂ k ↑ ℓ)
protectedAdd ℓ k = protect↑ ℓ (addᴺ k)
|]
p"protectedAdd↑"
«Consider now a weaker type, namely:»
[agdaP|
protectedAdd↑ : ∀ {α} ℓ k → Name (α ↑ ℓ)
→ Name (α ↑ k ↑ ℓ)
protectedAdd↑ ℓ k = protect↑ ℓ (addᴺ↑ k)
|]
p"unprotectedAdd↑"
«We simply replaced the occurrence of {_P} by {_S}. The consequences
of this change are disastrous: this type allows more behaviors for
its functions. Indeed the {agda|addᴺ k|} function can be given the
latter type (but not the former) when using the appropriate
inclusion witness to exploit the commutativity of {_S}:»
[agdaP|
unprotectedAdd : ∀ {α} ℓ k → Name (α ↑ ℓ)
→ Name (α ↑ k ↑ ℓ)
unprotectedAdd ℓ k
= coerceᴺ (⊆-exch-↑-↑′ ℓ k) ∘ addᴺ↑ k
|]
p"the bug"
«In our previous work {cite [pouillardpottier10]} we had only the
{_S} operation. Our function {agda|shiftName|} ({agda|protectedAdd|}
in this example) was defined with the {agda|unprotectedAdd|}
behavior. It took us a long time to discover this mistake, since we
thought that our logical relation argument was enough. In summary we
want to emphasis that all the logical relations proofs have to be
taken with great care. A weaker function type than expected can ruin
the intended informal properties.»
subsectionLbl «Using logical relations and parametricity» paramSection
p"using the parametricity results"
«To formally show that a world-polymorphic function {agda|f|} of type
{agda|∀ {α} → Tm α → Tm α|} commutes with a renaming of the free
variables, we proceed as follows. First we recall the natural
definition of logical relation on the type {_Tm}. Second we present
the type {agda|Ren|} of renamings as injective functions. Third
renaming is shown equivalent to being related at the type {_Tm}.
Finally we prove our commutation lemma by using the free-theorem
associated to the function {agda|f|}.»
p"⟦Tm⟧"
«The logical relation for the type {_Tm} is mechanical. It states
that two terms are related if they have the same structure and
related free variables:»
[agdaP|
data ⟦Tm⟧ {α₁ α₂} (αᵣ : ⟦World⟧ α₁ α₂) :
Tm α₁ → Tm α₂ → Set where
⟦V⟧ : ∀ {x₁ x₂} (xᵣ : ⟦Name⟧ αᵣ x₁ x₂)
→ ⟦Tm⟧ αᵣ (V x₁) (V x₂)
_⟦·⟧_ : ∀ {t₁ t₂ u₁ u₂}
(tᵣ : ⟦Tm⟧ αᵣ t₁ t₂)
(uᵣ : ⟦Tm⟧ αᵣ u₁ u₂)
→ ⟦Tm⟧ αᵣ (t₁ · u₁) (t₂ · u₂)
⟦ƛ⟧ : ∀ {t₁ t₂} (tᵣ : ⟦Tm⟧ (αᵣ ⟦↑1⟧) t₁ t₂)
→ ⟦Tm⟧ αᵣ (ƛ t₁) (ƛ t₂)
⟦Let⟧ : ∀ {t₁ t₂ u₁ u₂}
(tᵣ : ⟦Tm⟧ αᵣ t₁ t₂)
(uᵣ : ⟦Tm⟧ (αᵣ ⟦↑1⟧) u₁ u₂)
→ ⟦Tm⟧ αᵣ (Let t₁ u₁) (Let t₂ u₂)
|]
p"Ren"
«Then we need a notion of renaming. We choose to use injective
functions over names. The type for a renaming is {agda|Ren|}, and
the functions {agda|⟨_⟩|} and {agda|⟪_⟫|} respectively convert a
renaming to a function over names, and to a relation over worlds:»
[agdaP|
Ren : (α β : World) → Set
⟨_⟩ : ∀ {α β} → Ren α β → Tm α → Tm β
⟪_⟫ : ∀ {α β} → Ren α β → ⟦World⟧ α β
|]
p"⟦Tm⟧⇔rename"
«We now observe that given a renaming {agda|Φ|}, it is equivalent
for two terms {agda|t₁|} and {agda|t₂|} to be related by
{agda|⟦Tm⟧ ⟪ Φ ⟫|} and for {agda|t₂|} to be equal to {agda|t₁|}
renamed with {agda|Φ|}.»
[agdaP|
⟦Tm⟧⇔rename :
∀ {α β} (Φ : Ren α β) {t₁ t₂}
→ ⟦Tm⟧ ⟪ Φ ⟫ t₁ t₂ ⇔ (⟨ Φ ⟩ t₁) ≡ t₂
|]
newpage
p"ren-comm"
«Finally given a function {agda|f|} and a proof {agda|fᵣ|} that
{agda|f|} is in the logical relation, we can show that any renaming
{agda|Φ|} commutes with the function {agda|f|}. To prove so we apply
our {agda|⟦Tm⟧⇔rename|} lemma in both directions and use {agda|fᵣ|}
with the renaming {agda|Φ|} lifted as a {agda|⟦World⟧|}.»
[agdaP|
ren-comm :
(f : ∀ {α} → Tm α → Tm α)
(fᵣ:(∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Tm⟧ αᵣ ⟦→⟧ ⟦Tm⟧ αᵣ)f f)
→ ∀ {α β} (Φ : Ren α β)
→ ⟨ Φ ⟩ ∘ f ≗ f ∘ ⟨ Φ ⟩
ren-comm f fᵣ Φ t
= ⟦Tm⟧⇒rename Φ
(fᵣ ⟪ Φ ⟫ (rename⇒⟦Tm⟧ Φ ≡.refl))
|]
section «Conclusion and future work» concl
p"conclusion"
«We have shown a new approach for a safer nameless programming
interface. Our work relies on a different notion of worlds both
finer and more abstract. The type of names while being represented
as a natural number is kept abstract as well. Only a few functions
are required from the interface to get complete expressiveness.
Indeed while our worlds are more precise, nothing forces the
programmer to be precise with them. Thus there is no loss of
expressiveness compared to the {_Fin} approach. Through concrete
examples we have shown how we can program in this system using
classical examples like capture avoiding substitution. However the
most challenging result comes from the solid mechanized development
we have made in {_Agda}. This development not only demonstrates
the soundness of our approach but allows to derive properties
of functions using the system. This way we have shown that
world-polymorphic functions over terms commute with renamings of
free variables. These soundness results are shown in a modular way
and reuse the solid foundations of logical relations.»
p"future work"
«As future work we would like to explore more properties of this
system. We have also seen that a major convenience problem in our
system was to build world inclusion witnesses. We would like to
address this problem through a witness inference system built
within {_Agda}, using the recent reflection mechanism. Another
time-consuming task was to apply the {_Agda} logical relations to
types and operations, so we would like to explore the integration of
inspection primitives and meta-programming facilities for {_Agda},
namely {_Template_Agda}. Finally we would like to investigate how
this system could scale to representations of well-typed terms.»
paragraph «Acknowledgements»
p"Acknowledgements"
«Thanks to François Pottier, Jean-Philippe Bernardy, Alexandre
Pilkiewicz, and the anonymous reviewers for providing us with very
valuable feedback.»
newpage
doc = document title authors abstract body
main = quickView myViewOpts{basedir="out",showoutput=False,pdfviewer="echo"} "napa" =<< doc