Category talk:Type theory

Type

In my opinion, we need to split this category into the set-theoretical concept and the programming language concept(s). They basically only have the name in common. As my field is mathematical logic, I would suggest that this category be reserved for the mathematical concept, and the programming concept be merged into the existing Category:Data types or a new Cateogry:Data type theory. — Arthur Rubin (talk) 17:40, 23 August 2009 (UTC)

I think you are confusing data type with data format (common confusion given how most Wikipedia articles in this area are written, that is, without sources). The IEEE754 for instance is a data format not a data type; Real number is a data type. The type system layer (type checker or type inference) does not care how many bits are used for this and that. It's all a logic (calculus). A type is exactly the same concept in a type systems (as used in programming languages) and in mathematical logic. See for instance Types and Programming Languages or Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier, 2006, ISBN 0444520775, or even Bart Jacobs's (a computer scientist!) book Categorical Logic and Type Theory (see categorical logic for isbn), all available on gbooks. Pcap ping 01:30, 24 August 2009 (UTC)

By the way, you can read just the book review given at Types and Programming Languages, [1]. I assume you have access to jstor. Pcap ping 02:08, 24 August 2009 (UTC)

The review appeared in The Bulletin of Symbolic Logic. Do you think they would have published a review of a book on data formats?? Pcap ping 02:13, 24 August 2009 (UTC)

If it's not clear enough: type theory is more useful/applied in computer science today, in particular in programming languages, than it is in mathematics! Pcap ping 02:22, 24 August 2009 (UTC)

Actually, I wasn't confusing data type with data format. However, the mathematical concept in type theory (as well as the article you referred me to on my talk page) doesn't really include data types, either. And, if you want to assert that most of the articles in this category are the CS type, so it should predominate, we would have to verify that you didn't add articles on data types to this category. — Arthur Rubin (talk) 06:28, 24 August 2009 (UTC)

Can you explain briefly to me the difference between the mathematical and CS concept of type? Pcap ping 08:09, 24 August 2009 (UTC)

Formal methods

Also, formal methods has a very narrow meaning in computer science: applied theoretical computer science to software/hardware specification and verification; see the article for details, especially the talk page. Saying that it includes type theory is like saying that applied mathematics is the field that of all mathematics that are useful, in contrast with pure mathematics that is all useless mathematics. Does this makes sense to you?

Also, important mathematicians and computer scientists were (and some probably still are) wrongly listed in Category:Formal methods people. Alan Turing did not work on software/hardware specification and verification in the narrow meaning of the terminology as used in computer science today. He did not build Turing machines out of clay wax and prove that they met his concept! Pcap ping 01:40, 24 August 2009 (UTC)

Even the page linked from that cat doesn't list Turing as "formal methods person", but Wikipedia did. Same goes for Don Knuth. Pcap ping 01:54, 24 August 2009 (UTC)

French wiki for comparison

Although not impressive, the French wiki at lest has different articles on fr:Type (informatique) and fr:Format de données. They are less confused than many editors here. Their article on fr:Théorie des types is a stub, but at least it lists programming languages as an application! Also fr:Catégorie:Théorie des types only belongs to fr:Catégorie:Informatique théorique, an certainly not to fr:Catégorie:Méthode formelle, which has fr:Catégorie:Informatique théorique as parent. Pcap ping 02:44, 24 August 2009 (UTC)

Discussion copied from User talk:Arthur Rubin (feel free to continue it here)

As a general observation: if the Carl Hewitt affair had not gone so wrong here (for which there is plenty of blame to spread around), perhaps more than a handful of theoretical computer scientists would be editing this site, and instead of this discussion we would have had a decent article on type theory that would resemble the one on SEP, instead of the sorry affair it is here today. Pcap ping 02:49, 24 August 2009 (UTC)

(For all his faults Hewitt wrote some decent articles on topics of sufficiently interest, e.g. domain theory, which is pretty much the same article today as he wrote it, besides the treatises he then wrote on his own research. Contrast that with the unreadable stuff produced by the "professional Wikipedian" Wvbailey on random access machine, which spends plenty of time defending his work -- compare that article with the presentation of a RAM in S. Barry Cooper's book for instance.) Pcap ping 03:05, 24 August 2009 (UTC)

Even so, type theory in mathematics is completely different than in theoretical computer science, so should have different articles and categories. — Arthur Rubin (talk) 05:47, 24 August 2009 (UTC)

And which articles should appear in the mathematical category but not in the CS one? Pcap ping 05:59, 24 August 2009 (UTC)

Probably mathematical structure, ordered pair, setoid?, possibly principal type, System F, tuple (if split), unit type (I don't understand it in either context), and, of course, the parent article, type theory, which doesn't refer to computer science types at the moment. — Arthur Rubin (talk) 06:10, 24 August 2009 (UTC)

Let me see, you're missing quite a few things here, so I'll have to go over them:

• Ordered pair is a particular case of tuple thus product type, so I don't see how it isn't of interest to computer science, although one often needs higher-arity tuples in CS, so you might have a case that a computer scientist need not read ordered pair, although that a really a splittist view. The same goes for splitting tuple. I think the tuple article is good exactly because it covers all aspects, including the relationship between the notions in set and type theory. I understand however that some of the stuff may be distracting to you as a mathematician. But it's usually easy to filter out: it's in separate sections etc.
• As for System F (aka universal types), there's an entire chapter about it as a theory in TaPL, and another on implementing it (which I've added to System_F#Further_reading).
• Setoids are of interest in Martin-Löf type theory, and there are some academic programming languages (or rather proof assistants) based on it (since all programs in that theory are terminating). Did you see that setoid has an external link for an implementation in Coq? No offense, but I think you don't have enough experience in the are of functional programming to make a judgment of what's not interesting to CS, given that you don't understand what unit type is for (I'd be happy to clarify the article by the way, I worked on ti recently and I thought it was accessible)...
• Topics that would be of interest only to mathematicians are Russel's ramified type theory and New Foundations (why aren't those in the cat, by the way?). Even with these, there aren't a lot of articles in the math-only that category, so I think it's normal to keep the bulk of the stuff in Category:Type theory. If you feel it's really necessary, add Category:Type theory (mathematics) and put in it only those topics of interest to you. Probably the best thing to do is to make it a {{distinguished subcategory}}, i.e. those items should appear in the main Category:Type theory too. I don't think Category:Type theory (computer science) is necessary.
• It's true that type theory as it stands it caters almost entirely to mathematicians. I don't mind if you renamed it to type theory (mathematics) to make way for type theory (computer science), although this would be pointless at the moment since we don't have a CS-based (and by that I mean LICS perspective; type system is too PLT oriented. Sørensen and Urzyczyn are both theoretical computer scientists, but their book is not focused on some CS application of type theory; and neither is Bart Jacobs Categorical logic and type theory book. There's plenty of material from which to give a purely theoretical view of type theory from the (LI)CS perspective, but I'm not volunteering to write one at the moment. Give how little material we actually have on type theory as whole on this wiki I think splitting the main article wold be a mistake however. Until I added the connection the STT stuff in that article made no mention of simply typed lambda calculus, although there are plenty of books written by mathematicians that cover that aspect.
• By the way, you can't tell from our article on the Curry–Howard correspondence (because it's too basic), but all the corners of the lambda cube have significant correspondents in (intuitionistic) logic, which again appear to be of no interest to you. I see it's actually covered at Curry–Howard_correspondence#General_formulation, but just not using the terminology I searched first searched for. By the way, does that explain unit type from your perspective?
  • I hope you're not bent on splitting that article too because Hugo Herbelin wrote the general view and you don't care about it.
• My general impression that's not worth my time contributing to this wiki is only strengthened by the fact that I had to explain all that. At least I hope that something good will come out of it... Pcap ping 07:33, 24 August 2009 (UTC)

Restart

Stupid question: It seems like in math type theory refers to a formal system, with axioms and such. What's the interpretation of type theory in CS? Is it to do with data types in programming languages? --Robin (talk) 13:56, 24 August 2009 (UTC)

Part of the problem is that in English "data type" is rather misleading, which is why PL theorists avoid the "data" prefix. E.g. an important book in this area is called Types and Programming Languages (by no means the first, but it's the most popular in this century). See its "capsule history". The types from most typed programming languages are types in the sense of a typed lambda calculus, which were first introduced (in a modern formulation) by Church in simply typed lambda calculus (1940 or so, not his original untyped calculus). A modern type system is essentially a souped-up version of that. One can formulate three fundamental problems in a type system (roughly in order of difficulty -- in some systems some of these can be proven equivalent) see for the formal details:

• type checking -- relevant to compilation/execution of typed programming languages in general
• type reconstruction -- mostly used in functional programming: ML (always), Haskell (inference not always possible), Scala
• type inhabitation -- relevant to automated theorem provers and proof assistants, e.g. Coq, via Curry-Howard isomorphism

So, what was initially a programme to lay (new) foundations for mathematics has been (since the 1970s or so) expanded/highjacked by computer scientists due to these applications. (Too bad people like User:Sam Staton aren't active here anymore. They could explain this more concisely and convincingly than I can.) Pcap ping 14:44, 24 August 2009 (UTC)

By the way, abstract data types (which unlike "data type" is a well defined concept; see initial algebra) are existential types in type theory; at topic not yet covered on this wiki... Seminal paper by Mitchell and Plotkin. The topic is a bit esoteric, but it's (graduate) text book topic nowadays, chapter 24 in TaPL... Pcap ping 14:57, 24 August 2009 (UTC)

Actually, I now see your point, but you need to write a description of the category. {{catmain|Type theory}} won't do, as our article doesn't cover types in computer languages, and the lede of that article doesn't really go into enough detail to describe the category. Perhaps the category description can eventually filter into the article, but it's not there yet. — Arthur Rubin (talk) 16:38, 24 August 2009 (UTC)

Thank you for your patience! (I know I'm far from a good pedagogue when it comes to theoretical matters.) Since I've made the effort to synthesize this explanation, do you think that it would be a good idea to rewrite the type theory#Type system section along the lines of the above? (And perhaps rename that section to "types in computer science" too?) I suspect that the current version of that section is rather uninformative to most mathematicians (you can conclude that CS is a bunch of slogans from it, heh). Pcap ping 17:50, 24 August 2009 (UTC)