Talk:Type theory

Ontology

To me it is unclear what exactly is meant by "ontology" in regard to a (mathematical or logical) theory. I refer to the abstract:

"ST reveals how type theory can be made very similar to axiomatic set theory. Moreover, the more elaborate ontology of ST, grounded in what is now called the "iterative conception of set," makes for axiom (schemata) that are far simpler than those of conventional set theories, such as ZFC, with simpler ontologies. Set theories whose point of departure is type theory, but whose axioms, ontology, and terminology differ from the above, include New Foundations and Scott–Potter set theory."

In particular I think here it is not distinguished sufficiently between "theory", "axiomatization" and "ontology".Stephan Spahn (talk) 08:15, 14 May 2011 (UTC)

Question

Question - does type theory have anything to do with category theory in mathematics?

Not really. A type is a set of related things, together with a specification of the operations you can do to those things. A category is a set of related things, together with the maps (or arrows, or homomorphisms) between those things. AxelBoldt

Type theory with product types is related to Cartesian closed catagories and topos. Types are the objects, and the arrows are functions between types. See "Introduction to higher order categorical logic" by J. Lambek and P. J. Scott.

But, aren't those "operations" on types very similar to "maps" between things in categories? For instance executing "push" on a stack must not change the fundamental nature of the stack, hence is not the operation "push" a mapping (or homomorphism) between stacks?

Ok, I suppose you are right, for some types. So if we take the type "stack", we could manufacture a category out of it as follows: objects are the stacks, two stacks being considered different if they contain different things, and the morphisms between two stacks are all the sequences of push/pop operations that can get you from the first stack to the second stack.

However, this works only for type operations that take one stack and return one stack. For instance, the "stack" ADT typically has an empty? boolean operation, and a top operation which returns the top element of the stack. Those two can't be modeled in category theory. AxelBoldt

Meyer ("Object oriented software construction 2nd ed") differentiates strictly between "commands" and "queries" on an ADT. Commands change the state; queries observe but do not change the state. It would seem that an ADT plus all of its command-operations would form a category (since however a command changes the state, it cannot change the class of the object, unless we somehow also allow class-changing morphisms, which then however muddies the very concept of a "class" of objects). I feel there must also be a formalism for "queries" but it eludes me at the moment.

You also have a problem with operations that take two things and produce a new one, let's say the "add" operation for the ADT "integer". It's not clear how that should be modeled as a morphism either. AxelBoldt

Is the set of all integers a category in category theory? It intuitively seems like it would/could be. How does category theory deal with the class of all integers?

The set of integers is not a category (you could treat it as an additive category with a single object, but that is artificial). Typically, the integers are treated as one object in the category of rings.

Also, I think you can view the "create a new object from two objects" differently by switching to prefix notation instead of infix notation, e.g. to add integers 1 and 7, this is viewed as the command-operation "add" on object of type integer with state (value) "1" with an argument of "7", which changes its internal state to contain the value 8. This would then not be creating a new object, but rather changing the state of the first object. In fact, that's exactly how I implement my vector/matrix classes in C++. Would all this fit within the framework of category theory?

Ok, but then you need a copy() operation, or else you can never non-desctructively add two integers. I don't see how that could be modeled in category theory. AxelBoldt

(NOTE: see new reference added on main Type theory page)

My $0.02: Category theory and type theory are quite distinct, although not disjoint. You can imagine a type system based on category theory as an underlying formalism, but the practice of practical type system design owes much more to constructive logic and proof systems than to category theory. Anyway I've updated the type theory page with an intro. In the indeterminate future we should seriously consider breaking the type theory page into two pages, one for computer science applications and one for the mathematical foundations. user:K.lee

There is a notion of "categorical type theory". For example, see "Crole: Categories for types". Categorical type theory is basically trying to describe the type theory concepts in the category theory framework.

---

Passing through, I see the comment at the beginning of this article that it should be merged with datatype. While some of its material does belong there, I think that the applications of types to logic and computer science are sufficiently different that we want distinct articles, probably with the current names. As I said, I'm just passing through, but I'd encourage anybody trying to clean up this article to maintain this distinction. -- Toby 08:11 May 1, 2003 (UTC)

---

It's not just that values are given types but also the contexts in which they are used. For example, the if-then primitive of many programming languages has an associated (but usually implicit) type which indicates that it requires a Boolean value.

This is a detail peculiar to languages that have phrases that do not represent values. What you call "contexts" can usually be desugared into function values of appropriate type. Hence the semantics of if/then/else in ML are equivalent to a function of type bool -> (unit -> 't) -> (unit -> 't) -> 't. Anyway, I think that it's best to add this sort of information later in the article rather than earlier---it's hard enough to explain functional type systems clearly to a layperson, without getting into imperative languages. (The article as a whole does need a lot of work, BTW, and I can never find time to do it. If you want to add information about imperative languages and types of contexts, go for it.) k.lee

Also, sets are not always a suitable model for types. For example, when a type system allows recursive types, they cannot be modelled (in the standard way, at least) as well-founded sets. Consider the type of infinite lists of integers:

 List ::= Cons Int List

Considered as a set we would have

 List = Int * List

which is non-well-founded.

Malcohol 14:14 18 Jul 2003 (UTC)

AFAIK a recursive type is usually defined as the least set denoted by the closure of the unfolding(s) of the type definition, in much the same way that Church numerals are defined as the least set containing zero and closed under the successor function. A recursive infinite type (i.e., one that has no finite instances) is a little more complicated, but with the right formal acrobatics you can still define it as a set. I don't see why it matters whether this set is well-founded or not. The values belonging to a type need not be finite or even countable.

Of course, there could still be exotic type systems in which sets do not serve as an appropriate semantic foundation, but this article doesn't have to account for every bizarro type system out there, not in the first few paragraphs anyway. k.lee

Well, try giving a simple set-based meaning to types whose inductive definitions contain negative occurences of the induction type variable. David.Monniaux 06:37, 24 Jul 2004 (UTC)

Type theory vs Set theory

with classifying entities into "sets" called types.

I added quotes around "sets" in that sentence. Zermelo-Fraenkel set theory and type theory are two different ways of solving the paradoxes of naive set theory, as far as I know. That's why types are not, in general, "sets" in the mathematical sense. David.Monniaux 06:37, 24 Jul 2004 (UTC)

TODO

Major historical developments

• Bertrand Russell and Alfred North Whitehead
• Lambda calculus type systems
• Polymorphic type inference (ML programming language; Hindley-Milner polymorphism)
• subtyping
• Object-oriented static typing (grew out of abstract data type and subtyping)
• F-bounded polymorphism and efforts to combine generic w/ oo polymorphism
• Set-constraint-based type systems
• module systems
• Type-driven proof systems (e.g., ELF)
• ... (much more)

Practical impact of type theory

• Typed programming languages
• Type-driven program analysis and optimization
• Type-aided security mechanisms (e.g., TAL, Java bytecode verification)

Connections to constructive logic

• The Curry-Howard isomorphism between logical proof systems and type systems
• Ref: Wadler's "Programs are proofs"
• Intuitionistic Type Theory

Related topics

• The notion of abstract data types
• The relationship between types and object-oriented programming
• The interplay between types and algorithms
• A formal definition of abstract data types - precondition, postcondition, invariants
• The relationship between types and effects
• Type safety

Type Theory

This article is not about Type Theory it is about Type Systems. I suggest to move the page to "Type Systems" and put in a page on Type Theory, which nowadays usually refers to Martin-Loef's Type Theory and not to Russell and Whitehead's Type Theory, which is a stratification of set theory. Thorsten

I second this. I find it shocking to read an article titled Type Theory that does not mention either the lambda-calculus or the Curry-Howard correspondence. Cjoev

Type theory is discussed under “Intuitionistic_type_theory”. I'm not sure why.

That article (which I've only skimmed) seems to be about one type theory. But Type Theory, particularly as practiced by computer scientists in the context of programming languages (I am such a person, but a young one), is really the study of "type theories", which are sort of abstract versions of the type systems of programming languages. Since the mathematical/scientific field of study called "Type Theory" is about the methodology of defining type theories, their semantics, their properties, and their relationships to one another; in that sense it could more accurately be named "Type Theory Theory". Cjoev 02:15, 21 January 2006 (UTC)

Type Theory with capital letters is a constructive foundation of Mathematics, an alternative to Set Theory. In Computer Science the study of type systems of programming languages is also called type theory without capitals. The two subjects are not unrelated, since concepts from Type Theory sometimes find their way into programming practice, eg. our Epigram project. --Thorsten 22:48, 23 January 2006 (UTC)

Proposed renaming of "Datatype" article

It has been proposed on Talk:Datatype that the article Datatype be renamed Type system (which is currently a redirect) to more accurately reflect its subject. If that happens, it seems that things like Pierce's definition of type system and the simple typing example should move there, freeing up this article for more formal and/or more abstract type theory material and discussions of type theory not directly related to programming languages, such as logical frameworks, foundational type theory, and all the things I'm forgetting. I've made some edits in anticipation of the presence of a comprehensive Type Systems article. (Anyone watching this page should vote at Talk:Datatype on whether the move is a good idea.) Cjoev 21:45, 20 February 2006 (UTC)

Typeful Programming

I have added the article typeful programming to wikipedia, after having read "A Gentle Introduction to Haskell98" by Paul Hudak, John Peterson and Joseph H. Fasel. Would some of you please look at the article and see wether it should be merged into some other article. Velle 15:30, 3 April 2006 (UTC)

Bateson and NLP

Russell's theory of types is used by Bateson (for example see Talk:Double bind) and NLP (see Neurological levels). This article needs to provide a simple account of Russell's theory of types that makes sense to anthropologists and psychologists, not just mathematicians and computer scientists. By all means include the technical stuff, but don't start there. --RichardVeryard 14:47, 9 January 2007 (UTC)

"Other" Uses??

This page is about type theory in computation. For other mathematical constructions, see Intuitionistic type theory.

Pardon me, but what the hell happened here? Intuitionistic type theory is the kind of type theory that comes up in computation! Typed lambda-calculi including System F and the Calculus of Constructions are used as models for type systems of programming languages and for tons of other purposes thanks to the Curry-Howard correspondence. I've been studying computer science for twelve years now and I've never had any use for types in the sense of Russell, only types in the sense of Girard and Martin-Lof. Cjoev 00:43, 13 July 2007 (UTC)

Since nobody has shown up to call me an idiot since I wrote the above, I've gone ahead and rewritten the introduction. Cjoev 18:34, 7 August 2007 (UTC)

Nagel quotation

The property of being a perfect square can be significantly predicated of both cardinals and ratios of cardinals; but the property of being odd (or even) is not defined for the ratios. We are thus unable to answer the question whether 2/3 is odd or even. (Nagel 1951).

It is not obvious to the casual reader what the Nagel quotation has got to do with type theory. Unless someone puts in a helpful explanation, I shall delete it. --RichardVeryard 12:28, 8 August 2007 (UTC)

It's relevant to the section on type systems, but unless the quote is famous for some reason I think we can easily express a similar idea ourselves without the quote. — Carl (CBM · talk) 13:45, 8 August 2007 (UTC)

The question is not whether it is relevant, but whether its relevance is obvious to people who don't already know a fair bit about type theory. My concern is that this article needs to be meaningful to non-mathematicians, given that type theory is invoked in the social sciences. --RichardVeryard 16:25, 8 August 2007 (UTC)

I say remove it. — Carl (CBM · talk) 17:53, 8 August 2007 (UTC)

Yes, as it stands now it's kind of floating free -- but I have a dim (very dim) recollection that at some prior time in the life of this article it made mmore sense, but I can't find anything in the history -- perhaps I read it elsewhere. Zero sharp 21:31, 14 August 2007 (UTC)

I have now removed the Nagel quotation from the article, and included it at the head of this discussion for the record. --RichardVeryard 08:44, 15 August 2007 (UTC)

Criticism

There is no real criticism of theory of types here. It is simply assumed that it is necessary to have it, and no alternatives are considered. Ernestrome (talk) 21:02, 28 April 2008 (UTC)

Axiom of Infinity

"Remark. Infinity is the only true axiom of ST and is entirely mathematical in nature. It asserts that R is a strict total order, with a domain identical to its codomain. If 0 is assigned to the lowest type, the type of R is 3."

OK, where did the 3 come from? Even if it's guaranteed to be true, tossing it out there without any explanation will just confuse any naïve readers.

I also don't think it is true, at least not with the definitions implied. I'm not entirely sure how you adapt the Kuratowski ordered pair to type theory, or how relations are intended to be defined here, or how ordered triplets and cartesian products (assuming the most obvious definition of relations) are adapted. But it seems to me that, if a and b are in type 0:

G = 0x0 (cartesian product) >= 1 (because however you define it, it doesn't contain elements of type 0)

R = <0, 0, G> (definition of relation)

R = <0, <0, G>> (definition of triple)

<0, G> = {{0}, {0, G}} (Kuratowski) >= 3 (it contains things that contain Gs, so it has to be 2 higher than G)

R >= <0, 3> = {{0}, {0, 3}} (Kuratowski) >= 5 (as above)

I could be wrong about wrong about all of this--but if so, it's only because the article is confusing and misleading to anyone who knows set theory but not type theory. --76.200.102.13 (talk) 08:37, 25 February 2009 (UTC)

With Kuratowski ordered pairs, but a type-level cartesian product, you do in fact get 3. It's because of this that, historically, people added another axiom specifying a type-level ordered pair, which gives you 1. But ST alone doesn't give you any particular answer unless you come up with either constructions or axioms for all of the relevant parts. (How could it?)

So, this needs to be fixed, but I'm not sure how. --75.36.134.30 (talk) 15:10, 26 February 2009 (UTC)

Pungent criticism

• moved from the top:

This is one of the worst articles I have ever seen at Wikipedia. Jargon, name-dropping, shotgun topics. Horrible. If I were competent on the topic I would fix it, but unfortunately I came to this site because of my lack of competence. I probably have seen worse entries, but I can't think of them now. —Preceding unsigned comment added by 71.111.238.252 (talk) 15:15, 27 May 2009 (UTC)

History section

This has only scratched the surface; it could eventually be spun off into its own article, I suppose. I've hidden the following text, because I don't have the (re)sources (e.g. Quine, Tarski) to go further:

Quine reports that Ramsey 1931 urged the "dropping of the ramification and the axiom of reducibility"; Quine opines that "Russell's failure [was] due to this failure to distinguish between propositional functions as notations and propositional functions as attributes and relations.[Quine's commentary before Russell 1908 in van Heijenoort 1967:151-152. Ramsey 1931 The foundations of mathematics and other logical essays, edited by Richard Bevan Braithwaite (Paul, Trench, Trubner, London; Harcourt, Breace, New York); reprinted 1950 (Humanities Press, New York)]."

This is from Hans Riechenbach (1947, reprinted 1980) Elements of Symbolic Logic, Dover Publications, Inc, New York, ISBN:0-486-24004-5

"Although Russell on another occassion,³ suggested the extension of his theory [type theory + axiom of reducibility - ramified types] to a theory of levels of language, this extension ws actually carried through by Ransey⁴, to whom we own the distinction of logical and semantical antinomies, and by Tarski⁵ and Carnap⁶. The ramified theory of types was then dropped¹. An interesting attempt to replace the theory of types by weaker formtion rules was constructed by Quine², whose system employs certain ideas of von Neumann.

³ In his introduction to L. Wittgenstein, Tractatus Logico-Philosophicus, Harcourt, Brace, New York, 1922, p. 23

⁴ F.P. Ramsey, The Foundations of Mathematics, Harcourt, Brace, New York, 1931, p. 20

⁵ A. Tarski, 'Der Wahrheitsbegriff in den Formalisierten Sprachen,' Studia Philosophica, Leopoli, 1935

⁶ R. Carnap, Logical Syntax of Language, Harcourt, Brace, New York, 1937 (German edition, Vienna, 1934)

¹ Cf. B. Russell in his Introduction to the second edition of the Principles of Mathematics, Norton, New York, 1938 [ sic! ]

² W. Quine, Mathematical Logic, New York, 1940, Norton, § 24 and § 29.

Observe Riechenbach's bizarre out-of-sequence history -- Russell had published his 2nd edition to Principia Mathematica in 1927, not 1938. And he has dropped the ramified theory by 1910-1913 with his axiom of reducibility augmented with the "matrix" notion, which he further augments in the 1927 edition (after being exposed to Wittgenstein, cf his references on page xlv-xlvi). He drops the axiom of reducibility but at the loss of "infinite well ordering" as he states at the very end of his 1927 introduction (page xlv). Bill Wvbailey (talk) 16:36, 21 September 2009 (UTC)

"Type"

I lost track. Why is it called "type" theory? In which relation does type theory stand to set theory? The introduction says

• type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general.

Is there a list of all type theories? Thanks, --Abdull (talk) 21:09, 6 September 2010 (UTC)

Logical Types

Query--Excuse my butting in, but for 2 1/2 years we have needed a definition of Logical Types which is a part of Double Bind (see the section titled Theory of Logical Types). If anyone types in "Logical types" they get reverted to Type theory, but no layperson is going to understand what you are talking about. At least the first paragraph or two should be comprehensible for laypeople, one would hope. Can you do that? Any questions on your part about logical types in double binds? talk to me. --Margaret9mary (talk) 00:55, 16 December 2010 (UTC)

Theory ST

Unfortunately the reference to ST has neither link nor citation. I have a copy of Mendelson's 1964 textbook, which does not appear to have any information about ST, nor do I find it searching the Web or in other articles or books I know.

Can someone help with this reference? Also could someone describe the place of ST in the history of the subject? Crisperdue (talk) 18:36, 15 February 2011 (UTC)

I found something that may be of use. I make no pretensions at having read this chewy article, but I’ve skimmed it. In Kurt Goedel: Collected Works Volume II Publications 1938-1974, Oxford University Press, NY, ISBN-13 978-0-19-51472-6(v.2.pbk) there's a paper by Goedel titled "Russell's mathematical logic (1944)" (pages 119-141). This is prefaced with an "Introductory note to 1944" by Charles Parsons (pages 102-118). On page 126 we find this, together with footnote 17, and later expansion in pages 136-138:

"In the second edition of Principia, however, it is stated in the Introduction (pages xl and xli) that "in a limited sense" also functions of a higher order than the predicate itself (therefore also functions defined in terms of the predicate, as e.g., in p'k ∈ k) can appear as arguments of a predicate of functions, and in Appendix B such things occur constantly. This means that the vicious circle principle for propositional functions is virtually dropped. This change is connected with the new axiom that functions can occur in propositions only "through their values", i.e., extensionally, which has the consequence that any propositional function can take as an argument any function of appropriate type, whose extension is defined (no matter what order of quantifiers is used in the definition of this extension). There is no doubt that these things are quite unobjectionable even from the constructive standpoint (see page 136 [from pages 136-138 Goedel expands on the simple type theory, bringing up the notion from Frege "that a propositional function is something ambiguous (or, as Frege says, something unsaturated, wanting supplementation and therefore can occur in a meaningful proposition only in such a way that this ambiguity is eliminated (e.g. by substituting a constant for the variable or applying quantification to it). The consequences are that a function cannot replace an individual in a proposition . . ." [etc, etc] ]) provided that quantifiers are always restricted to definite orders. The paradoxes are avoided by the theory of simple types,¹⁷ which in Principia is combined with the theory of orders (giving as a result the "ramified hierarchy”) but is entirely independent of it and has nothing to do with the vicious circle principle (cf. page 147).

[Here Goedel launches into "the vicious circle principle proper". . ..]

" ¹⁷ By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: "a has property φ", "b bears the relation R top c", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399)."(p. 126)

The Type theory article's history reflects this development, with the "matrix" business. But I haven't taken the topic beyond Wittgenstein, e.g. to the papers of Ramsey 1926 and Tarski 1935. In his paper Goedel also discusses more about the "no type theory", "the zig-zag theory" etc. which may be useful. In general this appears to be a very valuable article both for its own content and its history. Here are the Ramsey and Tarski references:

Ramsey, Frank P. 1926 "The foundations of mathematics," Proceedings of the London Mathematical Society (2) 25, 338-384, reprinted in Ramsey 1931, 1-61"

Ramsey, Frank P. 1931 The foundations of mathematics and other logical essays, edited by Richard B. Braithwaite (London: Kegan Paul).

Tarski, Alfred 1935 "Der Wahrheitsbegriff in den formalisierten Sprachen," Studia philosophica (Lemberg), 1, 261-405; German translation by L. Blaustein of Tarski 1933a)

1935a is from the Polish (The concept of truth in the languges of deductive sciences), English translation by Joseph H. Woodger in Tarski 1956, 152-278.

1956 Logic, semantics, metamathematics: Papers from 1923 to 1938, translated into English and edited by Joseph H. Woodger (Oxford: Clarendon Press).

The question I have as I type this, is, is any of this in the public domain so I don't have to tromp through the snow up the hill to the local college library. Bill Wvbailey (talk) 20:33, 16 February 2011 (UTC)

---

I just noticed that in two sections or so above this one, the "History section" cites these same references, plus a few more (coming from Reichenbach's text). So my take on it is this: these references are "solid" and probably as good as it gets unless someone has recently written a "survey text" about (the history of) type theory. In other words, there may not be much out there but these primary sources. Bill Wvbailey (talk) 20:44, 16 February 2011 (UTC)