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