Talk:Type theory

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Mid Priority  Field: Foundations, logic, and set theory

Contents

[edit] 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)

[edit] 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)

[edit] TODO

[edit] Major historical developments

[edit] Practical impact of type theory

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

[edit] Connections to constructive logic

[edit] Related topics

[edit] 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)

[edit] 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)

[edit] 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)


[edit] 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)

[edit] "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)

[edit] 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)

[edit] 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)