David Corfield dependent types

  • x:AB(x):Typex: A \vdash B(x):Type

Dependent sum

  • x:AB(x):Type\vdash \sum_{x:A} B(x) : Type

Terms are pairs (a,p)(a, p) where a:Aa:A and p:B(a)p: B(a). Can capture ‘The As which are B’ when B(x)B(x) is a property.

Dependent product

  • x:AB(x):Type\vdash \product_{x:A} B(x) : Type

Terms are maps ff from AA such that f(a):B(a)f(a) : B(a).

Philosophical issues

Material constitution

Much discussion has occurred about how one can say there is only one thing in cases where there are two descriptions, such as a statue and a lump of clay (see SEP: Material constitution).

The lump exists on Monday, but not yet the statue. It is worked on Tuesday into a statue. The statue doesn’t exist on Monday, while the lump of clay does. They must be different. Then does the sculptor hold two things after forming the statue.

Can we say that the type statue is a dependent sum – The lumps of clay which are formed for artistic effect (maybe this should be modified to allow statues of other substances).

Then a term of type Sculpture is a pair (a,p)(a, p) where a:lumpofclaya: lump of clay and p:Art(a)p:Art(a) is a warrant that aa is formed for artistic effect.

When we say ‘X holds y’ we have X typed as person and y typed as object (space-time continuent). ‘X holds this statue’ means X holds the underlying object.

As with mathematical examples where the type theoretic reasoning carries with it proof terms, terms in ordinary language should do the same. If I say ‘this statue’, I should be prepared to answer the challenge ‘Why do you call it a statue?’ My term is being projected onto its second component, and I’m asked to construct something to fill that place.

Compare this to 2 as natural number, integer, rational, real, complex number.

Last revised on October 26, 2014 at 07:38:47. See the history of this page for a list of all contributions to it.