Tomas Petricek, University of Cambridge
http://tomasp.net | tomas@tomasp.net | @tomaspetricek
\[\definecolor{mc}{RGB}{0,32,172} \definecolor{cc}{RGB}{172,0,32}\]
Science is much more ‘sloppy’ and ‘irrational’
than its methodological image.(Against Method, Paul Feyerabend)
Source: Lecture notes from Types lecture
Bertrand Russell, 1908
Avoid paradoxes of the kind:
Class of all classes that do not contain themselves as elements
Base formulas have type \(0\)
Formula that uses a formula of
type \(n\) has a type \(n+1\).
We must interpret “I am lying” as “There is a proposition of order \(n\) which I affirm and which is false”. This is a proposition of order \(n+1\).
It is unnecessary, in practice, to know what objects belong to the lowest type (...). In practice, only the relative types of variables are relevant.
Types are not sets of values!
Alonzo Church, 1940
We refrain from making more definite the nature of the types \(\omicron\) and \(\iota\), (...) the formal theory admits a variety of interpretations.
John McCarthy, Tony Hoare, 1970s
McCarthy’s theory was developed by Hoare, who proposed that data types in PLs could be understood as sets of data values.
\(r := ~ !s\)
\({\color{cc} r:{ref}_\rho, s:{ref}_\sigma} \vdash r := ~ !s : \color{mc} unit~\&~\{ write~\rho, read~\sigma \}\)
What is the set of a type: \(\color{mc} unit~\&~\{ write~\rho, read~\sigma \}\)?
Express meaning of high-level types as relational,
extensional constraints on the behaviour of compiled code
Source: Nick Benton: What we talk about when we talk about types
We are not getting closer to one right definition!
Should there be a clear definition of type?
To 'clarify' the terms does not mean to study the additional properties of the domain in question, it means to fill them with existing notions from the entirely different domain of logic.
Science consists of multiple competing mutually inconsistent research programmes.
Hard core and protective
belt of auxiliary assumptions
[Core assumptions] are not to be blamed for any apparent failure. Rather, the blame is to be placed on the less fundamental components.
A new counterexample of a previously inconceivable form is discovered
In their critical zeal [the refutationists] stretched the concept of polyhedron, to cover objects that were alien to the intended interpretation.
We do not notice it & we cannot unthink it!
I turn aside with a shudder of horror from
this lamentable plague of functions
which have no derivatives.Charles Hermite, 1893
I turn aside with a shudder of horror from
this lamentable plague of type systems
which have no soundness proof.Anonymous on Hacker News, 2015
What is the correct scientific method?
To those who look at the rich material provided by history, it will become clear that there is only one principle that can be defended under all circumstances. It is the principle: anything goes.
How we use types in language?
Construct interesting contexts for types!
What can we cause with types?
We can experiment without having theory!
Precise answers “hamper the growth of knowledge”
and “deflect the course of investigation into narrow
channels of things already understood”.
For more see a short blog post on the topic
And also longer essay on the topic