Theory Of Types

It is imperative, if we are to understand "types", that we study what has been written about "types":

This is a beginning of such a study

First, here are are but a few of the internet resources on the subject:

the answers we find, and the understanding we develop, are shaped by the questions we ask

What can we extract from the above resources which will enhance our understanding of "types"?

Taking each resource individually:

http://planetmath.org/encyclopedia/TheoryOfTypes.html :

TypeTheory is based on the idea that impredicative definitions are the root of all evil. BertrandRussell and various other logicians in the beginning of the 20th century proposed an analysis of the paradoxes that singled out so called vicious circles as the culprits. A vicious circle arises when one attempts to define a class by quantifying over a totality of classes including the class being defined.

One descendant of TypeTheory is WvQuine?'s system of set theory known as NF (NewFoundations), which differs considerably from the more familiar set theories (ZFC, NBG, MorseKelley?). In NF there is a ClassComprehension? axiom saying that to any stratified formula there corresponds a set of elements satisfying the formula.

In the modern variants of type theory, one usually has a more general supply of types.

http://cogprints.org/4703/01/relform.pdf

Historically, Church’s formulation of type theory was much influenced by his formulations of the Lambda Calculus, which is a TheoryOfFunctions?. The 1940 article defining the logic is mainly of a syntactical character, but in the first section a brief suggestion is made concerning the intended interpretation of the system. This interpretation is to be functional. While in earlier and less precise formulations of type theory

 see Russell1908, Carnap1929

classes and relations played an important and more independent role, these now seem to have to be equated with their CharacteristicFunctions?. MultiArgumentRelations? are identified in this way with MultiArgumentFunctions?, which in their turn, following Schönfinkel1924, are equated with functions in one argument whose values are functions again.

In view of the fact that NaturalLanguage and/or and not can be used with expressions of almost all LinguisticCategories?, TypeDomains? should have a BooleanStructure?.

we can give a very simple rule for the interpretation of natural language ConjunctionDisjunctionAndNegation?: they are to be treated as n, u and c (complementation within a typed domain) respectively. Entailment between expressions of the same category is to be treated as inclusion

Simplification should lead to generalization; that is the reason why we strive for it. Thus far, my arguments for adopting a relational version of type theory were mainly concerned with the simplification and, I hope, esthetic improvement of existing semantic theories.

I have ... reasons to prefer Orey’s RelationalModels over Church’s FunctionalModel?s, there are equally good reasons to prefer ChurchsSyntax? over OreysSyntax? when it comes to choosing a logic for our purposes. In fact the latter logic, as it was defined in Orey1959, lacks the operations of application and abstraction, which are absolutely crucial for the Montague semanticist. So at this point it may seem that we can either have an applicable logic with a ComplexModelTheory? or a logic with a SimplerModelTheory? which is inapplicable. But the dilemma is only apparent. We can have our cake and eat it by taking the syntax of standard TypeTheory and evaluating it on RelationalModels?.

http://www.cs.cornell.edu/Info/Projects/NuPrl/Intro/TypeSetDomain/typesetd.html

The first chapter of MrAristotle's classical book on logic, the Organon (Logic), is Categories ; it is Aristotle's type theory. He clearly introduces the notion that some assertions make sense only when their subjects are of the right type. In translation he says,

The differentia of genera which are different and not subordinate one to the other are themselves different in kind. For example, animal and knowledge: footed, winged, aquatic, two-footed, are differentia of animal, but none of these is a differentia of knowledge.

In Nuprl terms, Aristotle is saying that if the underling types (genera) are different, say A is not equal to B, then no subtype of A, say {x:A|B}, is the same as any subtype of B, say {y:B|Q}. He goes on to say in the next sentences that if A is a subtype of B (subordinate genera of B), then we can predicate P of both A and B objects.

http://www.cs.pomona.edu/classes/cs66/Lectures/Lecture21/Lecture21_3.html

This material ...from Chapter 5 of Gamut ... is mainly relevant if we want to interpret statements of NaturalLanguage directly into a model, rather than first translating into a statement of IntensionalPropositionalLogic? (i.e., interpreting rather than compiling).

The idea is that sometimes we want to interpret a phrase as being parameterized by all possible worlds (e.g., the phrase "Mark is safe" in "John believes Mark is safe") and sometimes we want to interpret it just in the current world. "John is here and Mark is safe."

http://www.pps.jussieu.fr/~dicosmo/ResearchThemes/ISOS/ISOShomepage.html

The equivalence of types induced by the notion of isomorphisms can be used to help a user locate a function starting from the type he would give to that function. As well argued in MikaelRittri?'s and RuncimanAndToyn?s seminal papers, the type the user will come up with is not necessarily the one chosen by the library implementors, but it is very likely that it is isomorphic to it. Using the theories of isomorphisms, we can implement library browser that will retrieve functions whose type is isomorphic to the user supplied type, like the one provided with CamlLight? 0.7, Also, IsomorphicTypes? can help in designing better TypeInferenceSystems?, like the one described in JournalOfFunctionalProgramming199310

Discussion below this double line

CategoryTheory