Talk:Type theory

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

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

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