Talk:Intuitionistic type theory

Untitled

I have extensively expanded and rewritten this page. I am happy for anybody who helps me by elimenating typos and bad expression and by inserting more references. In the past somebody rewrote parts of what I had written, changing the emphasis considerably, e.g. talking about "an" Intuitionistic Type Theory while people in the wider area usually refer to Intuitionistic Type Theory using capital letters in the same way they refer to Set Theory and not a set theory. Hence, I have changed this back. If anybody is unhappy about this, please let's discuss it here.

Thorsten 21:57, 21 May 2005 (UTC)txa

I took out the reference to Automath, while it is true that there are interactions between Type Theory and Automath it is not true that Automath is based on Type Theory. I am happy to put it back in as soon as either me or sb else comes up with a good way of saying this.

I am not so sure whether the Thompson reference is such a good idea. I know and respect Simon, but I can't say I like this book... --Thorsten 18:39, 22 May 2005 (UTC)

• I think we should start a dependent types article and move the reference there. --- Charles Stewart 20:39, 23 May 2005 (UTC)

• I did start a dependent types article, but my point re the Thompson book wasn't so much where it should be cited but rather whether it should be cited.--Thorsten 15:37, 28 May 2005 (UTC)

Article name

It's right to notice all the synonyms that have been used for this theory, but my impression is that few scholars will use Intuitionistic Type Theory to refer to the calculus, but instead talk of Martin Loef's type theory, because there are many proposed intuitionistic type theories. I'd suggest moving the page, and say that the calculus has been called these other names. --- Charles Stewart 19:03, 23 May 2005 (UTC)

I agree Martin-Loef's Type Theory is more used more often than Intuitionistic Type Theory but the latter is more descriptive and in particular doesn't depend on Per Martin-Loef being happy with it. As I tried to express in the article there are a number of variants of Type Theory, e.g. extensional vs intensional, predicative vs.impredicative. However, we also talk about Set Theory and not set theories even though also there is some variation, we may add the axiom of choice or not, we may have the continuum hypothesis and we may or not add some large cardinals but we still call it Set Theory. I think it woukd be misleading to talk about intuitionistic type theories and I haven't seen anybody using this term. --Thorsten 15:34, 28 May 2005 (UTC)

JA: I did not do an exhaustive search, but as far as I can tell, searches for a generic article on "theory of types" get directed here, in addition to which we have computation-related articles on Type systems and Type theory. If there is some sort of proprietary claim on a capitalist rendition of T², then let the interested parties go take it up with Arnold Schwarzenegger. In the meantime, we need generic lower shelf articles on type theory and intuitionistic type theory that are comparable to those on graph theory, group theory, etc. Jon Awbrey 14:53, 1 May 2006 (UTC)

There is no claim whatsoever, the capitilasation expresses that one means the Type Theory instead of any.

--Thorsten 20:58, 7 June 2006 (UTC)

Type Theory is the name of a Programming Language

Spelled with initial capitals, Type Theory refers to a functional programming language based on the same principles.

Who has added this nonsense???? I have removed it. If you want it back, please xplain.

--Thorsten 20:55, 7 June 2006 (UTC)

Explanation of term "dependent product/sum"

At first glance it would seem that the "dependent sum" is a kind of product, and yet "dependent product" refers to something else. Can we have an explanation as to why these terms were chosen? Hairy Dude (talk) 20:03, 6 June 2008 (UTC)

The terminology comes from indexed sums and products of sets. I tried to clarify. Sam (talk) 13:30, 7 June 2008 (UTC)

Use of term "Type Theory" throughout article

This question is from someone who knows very little math theory.

This article is titled "Intuitionistic type theory" and in the "See also" section has a link to another page "Type theory". Why is it that throughout the article the phrase "Type Theory" is used when the article is about "Intuitionistic type theory"?

Dougher (talk) 01:42, 9 June 2010 (UTC)

All our articles are works in progress, but this one has particularly far to go. I hadn't looked at it before, and it's in very rough shape. So no wonder you find it confusing.

The reason that the author here said simply "type theory" is that the "intuitionistic" part only relates to the proof rules available in the system. The "type theory" part is not particularly different in classical type theory than in intuitionistic type theory. It would also be somewhat repetitive to say "intuitionistic" every time; the first sentence was written by the author to allow them to say just "type theory" in the body of the article. — Carl (CBM · talk) 12:04, 9 June 2010 (UTC)

Categorical models of Type Theory

Should the functor T not be named Ty? The colon ":" is not a symbol of the Language of category theory so this should be explained; of which category is A:Ty(G) an object? Stephan Spahn (talk) 10:17, 15 May 2011 (UTC)

Decidable extensional type checking?

The section Extensional versus intensional, as currently written, implies that, while calculating extensional types can be undecidable, a restriction of decidability can be imposed on the types used in the program or expression. But the halting problem (which is mentioned) prevents an implementation from being able to confirm the decidability of the type calculation (allowing an unbounded-time computation during compilation is a Bad Thing). This means that extensional types, which seem more flexible, rely on prudent use by the program or expression author to avoid disaster. In practice, this can only work in academic settings. I'm not sure whether these difficulties are due to the way this section is written or whether they imply that extensional types are not practical. In any case, some clarification seems to be needed. David Spector (talk) 10:50, 30 December 2011 (UTC)

.pdf of Martin-Loef's Intuitionistic Type Theory

While the Wordpress blogger who so graciously hosts the link to the .pdf in the References section did apparently receive permission to host the scan, their blog has been essentially dead since 2010. I wonder what to do in such a situation. It would be unfortunate if the link rotted; while Google gladly brings up lecture notes under that title, I don't see any other permitted, available copies of the book. I've downloaded a copy of it, but I don't really want to go through the trouble of getting permission to host it. Even if I did, we'd be left with the same problem five-ish years down the road. What to do? ArXivFever (talk) 07:03, 1 March 2012 (UTC)

What is this trying to say?

"In contrast in intensional type theory type checking is decidable, but the representation of standard mathematical concepts is somewhat more cumbersome, since extensional reasoning requires using setoids or similar constructions." (emphasis added) — Preceding unsigned comment added by 81.156.190.19 (talk) 16:05, 9 August 2015 (UTC)

There is some context in Intensional_logic, intensional definition, extensional definition, ostensive definition. See Per Martin Löf's paper on judgements.,p.3. (Also "Intensional definition is decidable" p.31) Consider also the fact that type theory is an alternative to set theory. Other civilizations have studied this, some studies of judgements are thousands of years old. Then, of course, computer science studies this as well. --Ancheta Wis   (talk | contribs) 22:36, 9 August 2015 (UTC)

After re-reading your question, here is a scheme based on the sentence you ask about:

• intensional type theory ------------------> type checking is decidable...........based on definition (linguistic statement)
• extensional reasoning (i.e. proof)-----> representation needs setoids......based on enumeration of set elements

Now since some computer languages can now use lambda expressions, intension is now part of the toolset, lending itself to automation, as opposed to brute force enumeration of the cases. --Ancheta Wis   (talk | contribs) 00:30, 10 August 2015 (UTC)

Significant Rewrite June 2018

I did a rewrite of the first 3 sections. Mostly tried to make the language accessible to people who had not studied type theory before. I did delete a few concepts, but mostly I tried to make the language easier without dumbing down the article. Mdnahas (talk) 14:07, 1 June 2018 (UTC)

1986 theory?

So, I believe I read somewhere that Nordstr ̈om Petersson Smith had the most referenced version of Martin-Loef Type Theory. If I recall correctly, it said that those three had reformulated MLTT to match Barendregt's Lambda Cube. That is, that variables were only bound by lambda and pi types. I don't think the theory behaved any differently than previous theories --- it still proved the same things as one of the earlier theories --- but the rules of inference were slightly different.

I tried to find where I read that, but couldn't find it.

I did look NPS's paper and found they had two! There is one on MLTT and one on programming with MLTT.

The first paper says "The type theory presented in this chapter was put forward by Martin-L ̈of in 1986 with the specific intention that it should serve as a logical framework." In fact, both papers say they use the theory from 1986. But 1986 is later than any theory lists currently on the wikipedia page! Is this formulation new? — Preceding unsigned comment added by Mdnahas (talk • contribs) 01:09, 5 January 2022 (UTC)

I read the NPS book ("Programming in ML Type Theory") quite closely for my doctorate and I recall no reference to Barendregt's cube. It is kind of separated into a logical framework, which is close to the lambda-Pi calculus and the calculus proper, although I don't recall it explicitly being called a logical framework. Take this all with a pinch of salt since it has been so long since I looked at the book: it's been 19 years since I defended my DPhil and that was quite a while after i finished the first draft of my dissertation. — Charles Stewart (talk) 16:26, 5 January 2022 (UTC)

Univalence in MLTT73

I'm confused about the remark regarding the univalence axiom pertaining to MLTT73 -- it seems on the face of it that a statement of the univalence axiom only pertains to the types of a fixed universe, and doesn't seem like it should need identity types that relate types of different universes. But maybe there's a detail about how MLTT73 is structured that I'm not taking into account here. Cgibbard (talk) 16:32, 8 November 2024 (UTC)