Talk:Type theory/Archive 1

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)

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)

"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)

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)

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)

Pungent criticism

• moved from the top:

This is one of the worst articles I have ever seen at Wikipedia. Jargon, name-dropping, shotgun topics. Horrible. If I were competent on the topic I would fix it, but unfortunately I came to this site because of my lack of competence. I probably have seen worse entries, but I can't think of them now. —Preceding unsigned comment added by 71.111.238.252 (talk) 15:15, 27 May 2009 (UTC)

"Type"

I lost track. Why is it called "type" theory? In which relation does type theory stand to set theory? The introduction says

• type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general.

Is there a list of all type theories? Thanks, --Abdull (talk) 21:09, 6 September 2010 (UTC)

Logical Types

Query--Excuse my butting in, but for 2 1/2 years we have needed a definition of Logical Types which is a part of Double Bind (see the section titled Theory of Logical Types). If anyone types in "Logical types" they get reverted to Type theory, but no layperson is going to understand what you are talking about. At least the first paragraph or two should be comprehensible for laypeople, one would hope. Can you do that? Any questions on your part about logical types in double binds? talk to me. --Margaret9mary (talk) 00:55, 16 December 2010 (UTC)