help · index · reference     Page · view · source · edit · history · print · source     Auth · login   

What is a type?

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


Is type only a label and a set combined?

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}
Here you can see the idea of Russel's paradox through the proof of Cantor's theorem in Coq.

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


Beware of paradoxes!

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


Propositions as types!

Let us see how Thorsten Altenkirch explains it.

AleksySchubert 01-09-2018 17:41 MET