Talk:Type theory

Talk:Type theory/Archive 1

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.

---

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
• ... (much more)

Practical impact of type theory

• Type-aided security mechanisms (e.g., TAL, Java bytecode verification) + Proof-Carrying Code

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 interplay between types and algorithms
• A formal definition of abstract data types - precondition, postcondition, invariants

Major Rewrite in Feb. 2013

I did a major rewrite in Feb. 2013. The old page was ... not useful.

I gave _a_ definition for type theory. I tried to give its relation to its origins and similar concepts (term rewriting system, combinatory logic).

I moved the history (which was the majority of the old article) to a separate page. I moved the description of the "ST" system to its own page. (Not sure why it was here - I had not heard of it elsewhere.)

I gave a concise description of features of most type systems, although there are many many type theories with difference properties. I gave a list of the better-known features that exist in various type theories.

I compared and contrasted type theory vs. set theory as a mathematical foundation.

I listed some type theories. I improved the list of applications of type theory.

I kept sections on "Category theory" and applications in "linguistics" and "social sciences", because I didn't know anything about those subjects. I removed a section on Polymorphic types; it seemed to apply to a "type system" more than a "type theory". (There is polymorphism in type theory, but it's different and rare and I don't understand it well enough to write on it.)

On the "talk page", I removed comments on the evolution towards separate "type theory" and "type system" pages, because I think it is clear that two pages are necessary and they refer to things with two different goals - mathematical foundations vs. features of a programming language. On the "talk page", I moved comments about ST and the History to their respective talk pages.

For full disclosure: I am working with the group working on Homotopy Type Theory. I did add links to the that topic on this page. But Martin-Lof and Coquand are also working on HoTT, so it is a significant area in the field.

Michael Nahas (mdnahas) — Preceding unsigned comment added by Mdnahas (talk • contribs) 19:23, 15 February 2013 (UTC)

Nice work, so far! Cheers, —Ruud 19:55, 15 February 2013 (UTC)

Intro Paragraphs

Michael Hardy did a change to the first paragraph that I didn't like and I rolled it back. (18:10, 21 September 2013‎) But on reconsideration, I think he had a good point but I think the fix requires a more extensive change.

First, I do think we need to keep both meanings of "type theory" on this page. There is the general usage and then there is the (older) usage to Russell's fix to Frege's logic.

But keeping that, Hardy's fix was about using "type theory" to refer to the field of study or to specific formal systems. I think he's right that we want to use it for the formal systems. So how about this for an intro:

'In mathematics, logic, and computer science, a type theory is a formal system where every "term" has a "type" and operations are restricted to terms of a certain type. Some type theories can serve as alternatives to set theory as a foundation for all mathematics.'

It doesn't capture the "generally" of the previous one, but it's easier to read and captures Hardy's intention (I think). Mdnahas (talk) 17:26, 23 October 2013 (UTC)

At some points in its history, this article said:

"[ . . . ]type theory generally refers to a class of formal systems..."

That's not a good way to phrase it for several reasons.

• It fails to make it clear whether it's being used as a mass noun or a countable noun. If one says "Category theory is a subject that blah blah blah blah", then it's clear it's being used as a mass noun admitting no singular or plural. If one says "A category theory is a blah blah blah", then it's clear that it's being used as a countable noun admitting singular and plural forms, so that one might later write "Two other category theories were introduced later...", etc. Thus it is better to write

"[ . . . ]a type theory is any of a class of formal systems..."

thereby being clear that it's being used as a countable noun.

• "refers to" is usually not a good thing to say. "A giraffe refers to an animal with a long neck" is nonsense unless the giraffe speaks. "The word giraffe refers to an animal with a long neck" might make sense if it's the _word_, rather than the animal itself, that's referring to something. And it might make sense to write about the word rather than about the animal itself if one wanted to make clear that although in some fields the word "giraffe" means the unit of money used in Slobovia, nonetheless in the present article it refers to something else. But when that's not necessary, then writing about the thing the word refers to is simpler than writing about the word rather than about the thing. One should not add complications that serve no purpose. Thus it is better to write "A giraffe is an animal with a long neck".

I also changed the link to "formal systems" into a link to "formal system", formatting it as [[formal system]]s. That way the read sees the plural, "formal systems", as a clickable link, and when one clicks on it one goes to the article titled "formal system" (without the final "s"). That is appropriate because the plural, with the final "s", is a redirect page pointing to the article whose title is singular. Generally Wikipedia articles are supposed to be singular except when there's a specific reason for them to be plural. Michael Hardy (talk) 00:31, 24 October 2013 (UTC)

Good points, all. What do you think of my proposed new first paragraph:

'In mathematics, logic, and computer science, a type theory is a formal system where every "term" has a "type" and operations are restricted to terms of a certain type. Some type theories can serve as alternatives to set theory as a foundation for all mathematics.'

Mike Mdnahas (talk) 18:24, 24 October 2013 (UTC)

Type itself deserves its own page

The notion of type as its own object of study is extremely important -- we cannot understand type theory without first understanding the different notions of what a type is, and then, how it can be applied as a concept to form the fundamental basis of several formal systems.

The Stanford Encyclopedia of Philosophy has its own article and discussion around "What Is A Type?": https://plato.stanford.edu/entries/types-tokens/. I think this is worth its own page and that material should be shifted around to support this extremely fundamental concept. Atasato (talk) 22:59, 8 June 2018 (UTC)

Lead paragraph

I rolled back changes made to the intro paragraph by DesolateReality. They added a link to the "computational logic" page, which does not contain a definition of computational logic. They did add that some type theories can work as "a programming language and a calculus for category theory." The "programming language" is possibly worth including. For the "calculus for category theory", I don't think that's worth including in the intro paragraph. It might be worth adding a section to the page if DesolateReality can do that.

Mdnahas (talk) 00:10, 2 January 2019 (UTC)

References

List of types

Skimming through this article, the only actual type I saw mentioned was nat. I think it would a good addition to the article to add a sentence/paragraph/section listing the most well known types. Joel Brennan (talk) 20:46, 9 July 2019 (UTC)

That sounds nice. I'd also love to see some basic set-theory examples done in type theory. E.g., I remember my teacher writing "the set of letters" on the blackboard and then creating subsets of "letters drawn with straight lines", which contained A, E, F, H ... and "letters drawn with curves", which contained C, O, S, ... She then talked about elements in the intersection: B, D, G, ... It was a great example for subsets and intersection. We should also do union. (And point out that set theory lets you union anything, no matter how unrelated, like letters and animals. Mdnahas (talk) 13:44, 21 January 2020 (UTC)

Rewrite in Oct. 2020

I extended the sections basic concepts summarizing and linking in the most central lemmata from Barendregt's framework and moved in the section decision problems from type systems and added a section about "interpretations of type theory", so that the main hooks should now be present. As "type theory" in general is broader, the disadvantage is, that the lemma now leans a bit more towards typed lambda calculus, but it already did so before. -- Cobalt pen (talk) 23:19, 9 October 2020 (UTC)

Rewrite in Dec. 2021

The previous changes to this webpage made it very technical and unintelligible to most readers. (The first definition was "a term is opposed to a type", which is not English or, at least, not modern English!) This page needs to be accessible to people who are not graduate students in math / computer science. I added an "introduction" section that is very simple. It includes "Knuth lies", that is, simplifications that help the reader to understand the basics of the ideas, even if they may learn later that the details are more complicated.

The introduction talks about (1) basics of terms, types and computation, (2) Barendregt's "pure type system" (a.k.a. lambda calculus or the "functional core"), and (3) some common types. I think it has all the basic ideas needed. The text could use some cleanup, especially to make the math/symbols correct.

I organized and cleaned up the rest.

I added a "technical details" section for all the graduate-student language.

TODO:

• It needs a lot more citations.
• We should combine and clean up "external links" and "further reading".

Mdnahas (talk) 18:10, 29 December 2021 (UTC)

I am extremely glad that you care about this and put the effort in, because I shared your troubles with this page. One thing to keep in mind, though, is that Wikipedia is not a textbook. We should definitely aim for a middle-ground encyclopedic style which is also good to learn from, by laying things out sensibly and making good use of linking. 185.214.220.196 (talk) 19:38, 8 February 2022 (UTC)

42nd Conference...

The reference " Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2016). "Cubical Type Theory: a constructive interpretation of the univalence axiom" (PDF). 42nd Conference on Very Important Topic. arXiv:1611.02108. doi:10.4230/LIPIcs.CVIT.2016.23 (inactive 2022-03-05)." is misleading: the " 42nd Conference on Very Important Topic" and the doi "doi:10.4230/LIPIcs.CVIT.2016.23" do not exist, they are just "place holder" for this document's template (Lipics). — Preceding unsigned comment added by 158.93.6.10 (talk) 14:08, 8 March 2022 (UTC)

We might be able to fix the humorous citation (to a conference some 20 years in the future) with a specific reference to the preprint https://arxiv.org/pdf/1611.02108.pdf, but striking the placeholder, and replacing "42nd conference ..." with

• Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. 21st International Conference on Types for Proofs and Programs, May 2015, Tallinn, Estonia. pp.262, ff10.4230/LIPIcs.TYPES.2015.5ff. ffhal-01378906v2f .

The Types home https://sites.google.com/view/thetypesconferences/home documents the existence of the conferences, which almost occur on a yearly basis, but which since have been interrupted by the COVID-19 pandemic. The most recent home, COST (European Cooperation in Science and Technology) is a pan-European intergovernmental framework. The specific meeting cited,

2015 Types meeting in Tallinn, Estonia, 18 - 21 May is part of

LIPICS Vol. 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015), May 18-21, 2015 - Tallinn, Estonia. Tarmo Uustalu (Ed.).

The background notes explain the delay in publication as a way for the authors to include some feedback from their peers. Thus the mismatch between the date of the conference and LIPICS volume with the article, which still might not completely match the arXiv preprint. --Ancheta Wis   (talk | contribs) 16:01, 8 March 2022 (UTC)

Proposed Change to Descriptions of the ‘if’ Construct

In the article, 'if' has the following description:

• if a b c : (Π a : bool . B → C → if a B C)

This appears to me inaccurate. If the definition above is considered correct, then `if a b c a b c : if a B C,` which is not, I think, the intended meaning. I propose that the above description is replaced by the 2 following:

• if : (Π a : bool . B → C → if a B C)
• if a b c : if a B C

The first gives the type of the `if` function itself, and the second gives its type when applied to arguments. Scholar596440 (talk) 14:44, 19 July 2023 (UTC)

I second this :-) BalinKingOfMoria (talk) 19:49, 19 July 2023 (UTC)

And it seems like a pretty straightforward typo to me, so I can't imagine your fix would be controversial. As per WP:JUSTDOIT, I think you're safe to go ahead make the change! BalinKingOfMoria (talk) 19:51, 19 July 2023 (UTC)

Thanks! Scholar596440 (talk) 19:56, 19 July 2023 (UTC)

Purpose of "Introduction"?

Aside from it being a right mess, it seems that the Introduction section begins with a treatment of simply typed lambda calculus, which already has its own page, and then lists a grab-bag of types which have varying levels of universality among type theories. This makes me wonder, what is really the goal of this article? I quite like the general sections (differences from set theory, interpretations, list, applications) because they deal with general type theories instead of a specific one. I would move (and rewrite!) most of the introduction to the STλC article; since I'm a new editor I thought I'd probe for opinions before being bold. Tectoskepsis (talk) 22:37, 17 January 2024 (UTC)

Tectoskepsis, generally encyclopedia articles should be able to stand on their own to a reasonable degree—a rule of thumb is to provide sufficient context to the reader. Mathematics articles may be the most difficult to do this for on the whole site, but I still think it's important to do so. I encourage your improvement of the article, but a summarized context is important to maintain in some form, in my opinion. — Remsense诉 22:50, 17 January 2024 (UTC)

Makes sense, thank you Remsense! (I've been reading your opinions at the Teahouse, and I appreciate the clarity of your thought!) Tectoskepsis talk 15:38, 18 January 2024 (UTC)

I don't think Frege published Russell's paradox in 1884

I'm reluctant to jump in and edit a page that has had such careful curation, but the second sentence of the History section starts, "Russell's paradox (first described in Gottlob Frege's The Foundations of Arithmetic)". As far as I know, this is false. Zermelo was apparently aware of the paradox in 1899. Hope someone will fix, or provide a reference. Thanks, Natkuhn (talk) 23:38, 3 May 2024 (UTC)