Project topics and materials
Get Complete Project Material File(s) Now! »
The general setting
It may be unclear from the following chapters since we will go deep into obscure details, but this dissertation started from two questions about com-munication:
1. How do I explain to my computer what I want it to do ?
2. How do I get sure that my computer actually did what I asked ?
Computers as we know them are quite recent, with the first room-sized computers that were built during the 1940’s. However, even before that, they were mechanical devices that could be informally called “computer”: a Barrel organ is a musical instrument that can read and play music from a written sheet, or a Jacquard loom can create complex textiles from some recipe. Both examples are in fact using the same input: a collection of punched cards. As you may remember, some of the first computers also used punched cards as computing instructions or data-input. In these three cases, the goal is the same: we want to give a sequence of instructions to a device so it achieves a particular purpose, whether it be playing music or computing some complex mathematical function.
We should all agree on the following points:
• Punched cards are not a reasonable “human-readable media”.
• One can not store so much information on a single punched card.
These are some reasons why we study programming languages. The ul-timate language may change among people, but everyone will agree on the fact that a good programming language should be easy to write, easy to read and expressive enough to let the programmer spend most of this time “programming”, not “reinventing the wheel” every time.
You may have noticed that we did not ask the language to be “computer-readable” and in fact, we do not want that. However, we will need another language that will fulfill this purpose, but this one does not have to be intelligible to human beings, since it is dedicated to the Computer Processing Unit (CPU). Back in the early years of computer science, both languages were almost the same (you may remember punched cards and assembly language for example), but now we can make a fortunate distinction between both. All we need is a way to translate our favorite programming language into the favorite programming language of our CPU, which is a process called compilation. We will not talk about compilation anymore in this dissertation, but this is a good example to emphasize one more time our two previous questions: how can we be sure that this translation process is correct ?
The purpose of programming languages
Hopefully, we now all agree on the fact that we want to give orders to a computer in a human-friendly manner. Nowadays, computers are quite so-phisticated, but they are merely bigger calculators than the ones we all used at school to compute simple equations like “what is the result of 126 di-vided by 3?”. So programming languages should be about describing the data-structures we want to work with, and the things we want to compute with them (this is question 1 of the previous section), and also about how to compute “in a safe way” (this is question 2): we want to give orders to a computer, and have some fairly good insurances that the computed results are what we actually expected.
What do we have at hand to do such computations ? We will keep it simple by stating: a CPU which will blindly execute the orders we give him and some space for data storage, which is commonly called memory. This memory can be seen as a big array of zeros and ones (called bits), most of the time stored in packs of eight (eight bits are called an octet). In our language, we will have to handle data such as natural numbers, strings, lists and so on, but in the end, they will all be stored as a chunk of memory. So, we need a way to distinguish one chunk of memory from another: let us say we have the plus function that take two natural numbers and add them together. What if we call this function on a string and a list of natural numbers ? What should happen ? What will happen ?
If it happens, we can almost be sure that your program will crash. But it should never have been allowed in the first place! Just by taking a look at the types involved in such a program, we can see it fails to work. This is where question 1 and 2 are facing one another: we manage to write down a program for our computer, but it was not safe to execute.
How did we guess that this program was not safe to run ? This is an easy question: plus is waiting for two natural numbers, and we gave it something else. But we are clever human beings who saw this issue, while the computer only saw two chunk of memory with octets in them. It is our work, through the programming language, to give more information to the computer, so it can avoid such traps. We need to make the computer understand that a chunk of memory representing a string should not be used when a natural number is expected. This is commonly achieved by adding labels to this structure, saying for example “this chunk is a natural number and this other one is a list of strings”. With this information, the computer can be aware of the kind of data it is computing over, and will reject a program like plus (3, »foo ») just because « foo » is not a natural number.
These labels are called types, and the action of seeing if the type of an input matches the expected type of a function is called type checking. The structure of types inside a programming language is called a type system. They are here to enforce some guard properties in a program, to have some guarantees that the computation will be done in a safe manner. The expres-siveness of type systems is directly linked to the kind of guarantees we will have: if they are too simple, we will only be able to have simple information as in the toy example we just saw. With more expressive languages, we can have much more powerful assertions, like pre-conditions to fulfill before being able to use a function, or additional information on the values returned by a program.
A common example to emphasize the power of a type system is Euclid’s division algorithm: extensionally, it can be stated as “given a and b two natural numbers, if b is not equal to 0, we want to find q and r such that a = b ∗ q + r and r < b”. In real programming languages, the type of this program may vary depending of the power of the type system:
• in C-LIKE: void div(int a, int b, int *q, int *r)
• in ML-LIKE: div: int -> int -> (int * int)
• in COQ: div : forall (a b:nat), 0 < b ->
{q : nat & {r : nat & a = b * q + r /\ r < b }}.
In the first two examples, the programming language is not informative enough to carry around information “about” the data, like b is not 0 or a = b ∗ q + r. The only information we have is that div is expecting two natural numbers (or integers) and will return two natural numbers, without any information about the computation itself.
In the last one, there is a pre-condition and two post-conditions: to be able to call this function, we need to give a witness that b is not 0, and this function will give us two natural numbers that verify the two relations that we are interested in. It is pretty nice to have such power in the type system, but there is a drawback: in the code of the third program, we need to build the proof that the resulting q and r enjoy the nice relations with the input. More expressiveness will require more work from the programmer. In this particular example, we already know some automatic ways to prove these arithmetical results, but we have to keep in mind the following statement: the more we want, the more we need to provide first.
A practical example
To be able to study a programming language, we first need to explain its syntax, and then we can try to prove some nice properties over it. In fact, we need to define two things: the syntax of the language, and the process of computation. We need to formalize our language along with the process of computation. As an example of the properties a programming language can have, we are going to consider a simple (but still powerful) example by studying the λ-calculus.
This language was introduced by Alonzo Church [Chu51, Bar84] in the 1930’s as a tool to study the foundations of mathematics. Since then, many extensions of this language have been used as a basis for real programming language and for logic programming [HAS, SML, Gal, PS]. Here is its syntax: M, N ::= x | M N | λx.M
A term of the λ-calculus can be built from three different constructors. The first one is about variables (which we will always write as lower-case letters x, y, . . . ). They are names for more complex terms. The second one, M N , is called an application: given a function f and an argument a, f a stands for “let us apply the function f to a”. Back in high-school, we would write it f (a), this is just another notation for it. Please remember that this is not the result of the computation of this function when applied to a particular argument, it is just the syntactic juxtaposition of two terms: for example, if we consider the identity function id that just return whatever data we give it, id a is syntactically different from a, but it will compute to a. If a function has several arguments (like the plus function for example), we simply use several applications :(plus x) y. By convention, application is left-associative, so we can even get rid of the parentheses and just write plus x y.
Finally, the most awkward of the symbols above, the λ-abstraction is used to define functions. Until now, we gave name to functions but names can be complicated to handle during a strict formalization, so we introduce anonymous functions with this abstraction. Here are some simple examples to illustrate this λ construction:
• the identity function is denoted by the term λx.x, which is equivalent to the declarative statement “for any term x, we return x”.
• the plus function1 is denoted by the term λxλy.x + y: “given a x and a y, we return x + y”.
• the app function, that takes a function, an argument, and apply this function to this argument is denoted by the term λf λx.f x.
In a λ-abstraction λx.M , the variable x is bound by the λ inside the body M . It means that if we apply this function to an argument N , all occurrences of x inside M will be placeholders for N .
Now that we have a simple syntax for terms (without types at the mo-ment), we need to explain how to compute with them: how do we go from id x to x ? This process of rewriting a term into another one is called β-reduction, and is informally defined as follows: if an abstraction λx.M is applied to term N , the application (λx.M ) N can be β-reduced to M [N/x], which stands for “replace all the occurrences of x in M by N ”. This process will be noted →β for a one step reduction, and ։β for several consecutive steps:
• id N →β N
• app id a →β (λx.id x) a →β id a
• plus 3 4 ։β 7
1Here we cheated: + is not part of our syntax, but it was just to illustrate with a known example. This language is rather simple, but it is quite interesting to study its computational behavior, even without type information: we can encode a lot of interesting data-structures (natural numbers, pairs, lists, . . . ), but this is not what we are interested in at this point.
What can we say about this language ? What properties does it give us on the structure of our program, or on its computation behavior? In fact, nothing much at the moment: we need types! Since we only have one function constructor (using the λ-abstraction), we only need one type con-structor, written →, which is pretty much like the mathematical implication for function:
• id has type A → A: it takes a data of type A and returns it directly, so the type is not changed.
• plus has type nat → nat → nat: it takes two natural numbers and returns a natural number.
• app has type (A → B) → A → B: it takes a function of type A → B, an argument of type A, and returns the result of their application, which is of type B.
We will also need some base types (like nat or string) for our data, but we do not really care about it for our study. Last thing, we need to store all the type information we will collect in a context, as a remainder of the types that we already know: as soon as we know that plus has type nat → nat → nat, we can put this information in our context so we do not need to rebuild this information the next time we will need it.
With all this, we can build a type system for the λ-calculus, called the Simply Typed λ-calculus. This extension of the λ-calculus was also introduced by Church [Chu40] a few years after first presenting the λ-calculus to avoid some paradoxes that were discovered in the untyped calculus. The system is defined according to the following rules:
• a variable x has type A if this information is in our context.
• if, knowing that x has type A, we can prove that M has type B, then λx.M has type A → B.
• if M is a function of type A → B and N has type A, the resulting application M N has type B.
Since we are trying to be a little more formal, we now give the same set of rules, but written in a much more concise way, it will be easier to talk about a specific rule. The typing rules for the Simply Typed λ-calculus are detailed in Fig. 1.1. This kind of presentation is called a type system.
Table of contents :
I Introduction
1 Type systems in a nutshell
1.1 The general setting
1.2 The purpose of programming languages
1.3 A practical example
1.4 Computation on types
1.5 Where to go next ?
II Untyped equality
2 Pure Type Systems
2.1 Pure Type System in Natural Deduction
2.1.1 Terms and Untyped Reductions
2.1.2 Presentation of Pure Type Systems
2.2 Pure Type Systems in Sequent Calculus
2.2.1 Terms and Reduction
2.2.2 Confluence of β-reduction in λ
2.2.3 Typing Rules
2.2.4 Properties of the system
2.3 Delayed Pure Type System in Sequent Calculus
2.3.1 Typing Rules
2.3.2 Properties of the system
2.4 Expansion Postponement in Delayed System
2.4.1 Postponement in Sequent Calculus
2.4.2 Postponement in Natural Deduction
2.5 Sequent Calculus and Type Inference
2.6 A brief look back at syntactical Pure Type Systems
III Typed equality
3 Judgmental Equality
3.1 PTSs with Judgmental Equality
3.1.1 Typing Rules
3.1.2 Subject Reduction and Equivalence
3.2 Basic meta-theory of the annotated system
3.2.1 Definition of PTSs with Annotated Type Reduction
3.2.2 General properties of PTSatr
3.2.3 The Church-Rosser Property in PTSatr
3.2.4 Consequences of the Church-Rosser property
3.3 Equivalence of PTSatr and PTSs
3.3.1 Confluence of the annotation process
3.3.2 Consequences of the Erased Confluence
3.3.3 Consequences of the equivalence
4 Formalization in Coq
4.1 Formal proof: paper or computer ?
4.1.1 What is a formal proof ?
4.1.2 Automatic resolution and induction schemes
4.2 Encoding PTSs in a proof assistant
4.2.1 Questions about encodings of binders
4.2.2 Higher order encodings
4.2.3 Our final choice: de Bruijn indices
IV Conclusion and Further Research
5 Extensions of PTS
5.1 Sorts, order and subtyping
5.2 Toward a typed conversion for CC!
5.2.1 The straightforward approach
5.2.2 Other attempts and possible leads
5.3 Other leads for future investigations
