Talk:Type theory
From Wikipedia, the free encyclopedia
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)
Contents |
[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
- 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)
[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
- The Curry-Howard isomorphism between logical proof systems and type systems
- Ref: Wadler's "Programs are proofs"
- Intuitionistic Type Theory
[edit] 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
[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)
