Our faculty organises at the end of the summer term an event called *Lectures on lectures*. At some point I presented there my lecture related to type theory. After the presentation a student approached me and asked, "What is type?". My quick answer was that it is a set together with a kind of label or tag. That's very simple, isn't it? But then the student asked me, "Why do we need the whole theory for this kind of simple nomenclature?"

Is that association of *tokens* to *types*, as it was called by C. S. Peirce, really simple? Let us take this line

*Rose is a rose is a rose is a rose.*

from a poem *Sacred Emily* by Gertrude Stein line from her poem. How many words are there in this line? One may answer *three*, but also *ten* is a plausible answer. We immediately see that there is some complexity here. Especially, if we realise that the word *word* also represents a type here the tokens of which may be these three entities we observed in the verse or ten ones or, oh damn, both of them.

AleksySchubert 06-06-2017 23:32 MET

It is a nice view. A type is a set together with its label. But is that really all? Actually, we need one more ingredient. We need a criterion to check is a particular element is an inhabitant of the type. We cannot tell if a number is a *natural* if we do not know how to recognise its `naturalness', we cannot tell if an animal is a *cat* if we do not know how its ears look like and how fluffy is its tail.

One interesting case here is the one we know from the Russell's paradox. We can recall definition used there

*R = { x | x ∉ x}*

with which we can pose the question if *R ∈ R*. If we answer it affirmatively then by the definition of *R* we get *R ∉ R*. If we answer it negatively then by the definition of *R* we get *R ∈ R* so each of the cases contradicts itself. This paradox can be easily stopped by assuming that the predicate ∈ is typed and one can ask *x ∈ R* only when *x* is a proper *element* and *R* is a proper *domain of elements*, i.e. are of different types. However, what is the criterion to check if an entity is an *element* or a *domain of elements*?

AleksySchubert 06-19-2017 00:09 MET

Actually, the solution that I suggested in the previous entry is a little bit vague. It may be the case that theory of types in which we work has a nice workaround for the paradox to exists even though the types separate sets from their extensions. Frege had a system in which a predicate could not have a predicate as an argument. It could only have objects as arguments. However, the system of Frege had a notion of predicate extension extraction such that for a lexical notion of a predicate *P* it could give its *extension*, written 'εP'. This theory had a very natural axiom:

*(Axiom V) εP = εQ <=> ∀x[P(x) <=> Q(x)]*

which basically said that extensions of two predicates are equal if for each object 'x' either both predicates hold for it or they do not hold. In this system we can define a lier's predicate as

- 'R(x) if and only if ∃P[x = εP ∧ ¬P(x)]'

which closely follows the definition from the Russel's paradox, but it carefully restricts the definition to objects that are extensions of some predicates. We can now prove easily a paradoxical fact that

- 'R(εR) <=> ¬R(εR)'

and this proof uses Axiom V in a crucial way.

How to avoid this paradox? We can do it by employing more types. We can say that 'εP' lives on a higher level than the value of 'x' in 'P(x)' and in this way forbid the use of 'x = εP' in the definition of 'R'. In this way we obtain so called 'pedicative' version of the Frege's system (which is sometimes called 'impredicative').

AleksySchubert 08-21-2017 15:12 MET

Let us see how Thorsten Altenkirch explains it.

AleksySchubert 01-09-2018 17:41 MET

I sometimes have trouble in explaining why type systems are useful. Here is one possible explanation that may convince some layman.

You read it because someone automatised the communication process between you and me. Only precisely defined tasks can be automatised, because in the end machines cannot deal with imprecisions. Therefore, we write programs that instruct machines how to proceed (and give the idea how they will do it to other people). Then a need occurs to double-check that the work of the machine agrees with the intent. For this, we need a language to precisely express it and methods to verify that the intent agrees with the program.

One possible way to do this is to use types. Types that are so rich that they can express any property of interest. Type systems that are currently used by mainstream programming languages (Java, C, C++ and so on) eliminate many problems of untyped languages (such as Python, JavaScript, List and similar), but are not strong enough to express properties even so simple like the one that a number is odd. However, there are type systems and tools (for instance Coq, Matita, Agda, Why3) in which one can program, express properties of interest through types and verify that the execution of programs agrees with provided intents. These tools were successfully used to develop industry scale programs the behaviour of which provably agrees with the formally expressed intent (C compiler CompCert, formalised behaviour of Freescale 8-bit processors). The chances that these programs contain errors are much smaller than in case of typical programs.

AleksySchubert 03-27-2018 09:57 MET