History and Philosophy of Types

Tomas Petricek, University of Cambridge
http://tomasp.net | tomas@tomasp.net | @tomaspetricek

\[\definecolor{mc}{RGB}{0,32,172} \definecolor{cc}{RGB}{172,0,32}\]

What is a type?

Science is much more ‘sloppy’ and ‘irrational’
than its methodological image.

(Against Method, Paul Feyerabend)

Uses of types and type systems

  1. Detecting errors via type-checking, statically or dynamically
  2. Abstraction and support for structuring large systems
  3. Documentation
  4. Efficiency
  5. Whole-language safety

History of types

How the meaning of 'type' changes


Mathematical logic as based on the theory of types

Bertrand Russell, 1908

Avoid paradoxes of the kind:

Class of all classes that do not contain themselves as elements

Mathematical logic as based on the theory of types

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\).

Mathematical logic as based on the theory of types

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!

Simple theory of types and \(\lambda\)-calculus

Alonzo Church, 1940

  • \(\lambda\)-calculus and types as foundations of mathematics
  • Not created for ruling out invalid terms!

We refrain from making more definite the nature of the types \(\omicron\) and \(\iota\), (...) the formal theory admits a variety of interpretations.

From expression types to computation types

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.

From expression types to computation types

\(r := ~ !s\)

From expression types to computation types

\({\color{cc} r:{ref}_\rho, s:{ref}_\sigma} \vdash r := ~ !s : \color{mc} unit~\&~\{ write~\rho, read~\sigma \}\)

From expression types to computation types

What is the set of a type: \(\color{mc} unit~\&~\{ write~\rho, read~\sigma \}\)?

Types are not sets but relations!

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

Types in modern programming

  • Unsound - Dart, Type Script
  • Super sound - Idris, Agda, F*
  • Relatively sound - F# type providers

We are not getting closer to one right definition!

Philosophy of types

Against a formal universal definition


Feyerabend's epistemological anarchism

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.

Lakatos and research programmes

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.

Lakatos and concept stretching

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!

Concept stretching and functions


I turn aside with a shudder of horror from
this lamentable plague of functions
which have no derivatives.

Charles Hermite, 1893

Concept stretching and types


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

Feyerabend's epistemological anarchism

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.

Living without clear notion of 'type'


Living without clear notion of 'type'

Meaning is use

How we use types in language?

Construct interesting contexts for types!

Types as scientific entities

What can we cause with types?

We can experiment without having theory!

Summary

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

http://tomasp.net | tomas@tomasp.net | @tomaspetricek