Home » forums » LtU Forum

Type Theory Glossary

As a subject, garbage collection has a nice glossary that can be used as a reference while reading the literature. Do type systems/type theory have a comparable online glossary?

I haven't come across one, but it seems like a it could be valuable resource.

By naasking at 2015-05-04 13:15 | LtU Forum | previous forum topic | next forum topic | other blogs | 4590 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Crowd-sourcing

Assuming the answer is "no" (at least I know of no such thing, but maybe the index of the TAPL is close to this idea), could we crowd-source its construction? I would be glad to contribute questions and answers.

One thing that would need to be clearly defined (or clearly not defined) in the scope of what "type system" means in this context. Your use-case would be "reading the literature" (I assume the academic literature on static and dynamic type systems), but the terminology is different from what practitioners use ("generics" vs "parametric polymorphism", etc.), and some topics would need to expose several competing definitions ("untyped" for example). The best would probably to have no "type system" entry at all -- less general terms tend to be less controversial, even less so if the technical meaning is prioritized.

By gasche at Mon, 2015-05-04 15:38 | login or register to post comments

I would love for this to be

I would love for this to be crowdsourced and would contribute also. Maybe the LtU community could start a wiki devoted to PL topics...starting with types? Or we could contribute a page to Wikipedia as a comprehensive index to type system terms?

By Sean McDirmid at Mon, 2015-05-04 22:39 | login or register to post comments

Alternatively,

Alternatively, we could make use of Wikipedia's sister project Wikibooks. Original research still isn't allowed, but there's less red tape about common knowledge within a field, noteworthiness, and whatnot, and less restrictive format. Wikibooks has a support infrastructure already, which is shared by all the wikibooks on the project.

We'd want to work out a scope (and title, of course), structure, and outline for the book, keeping in mind that the structure of a book can make a huge difference in how readily it can be added to over time.

[Addendum: of interest, Subject:Computer programming.]

By John Shutt at Tue, 2015-05-05 02:08 | login or register to post comments

Trinitarianism

Computational trinitarianism comes in handy. I look up logic concepts at the Stanford Encyclopedia of Philosophy and category theory concepts at nLab.

By Ross Angle at Mon, 2015-05-04 20:38 | login or register to post comments

Jargon traps

Unless you have some prior training in the field, with these (and wikipedia for that matter) you'll quickly find yourself stuck in jargon cycles. It would be cool to have a glossary for Programming Language Theory that (in addition) provided definitions using ordinary language and/or mainstream programming language jargon as a "rosseta stone" for the wider audience - including next generations of young people who have yet to go through training in these artificial languages.

By chrisoliver at Tue, 2015-05-05 01:42 | login or register to post comments

nLab...

... is where leading category theory researchers take their own synthetic notes, as they say themselves. Being didactic is by far not their goal, though I guess it happens sometimes — and I often look up stuff there. I don't mean to criticize them, it's just not the easiest intro.

For CT, one needs a textbook at least to get started. After referring to some other book by Peter Smith (on Gödel's theorem), I have enormous hopes for what he's writing on category theory. He's an amazing writer. (I had a specific question, looked at chapter twenty-something without having ever read anything else from the book, and got a useful and insightful answer).

http://www.logicmatters.net/categories/

By Blaisorblade at Sat, 2015-05-09 07:38 | login or register to post comments

Survey papers

Are there any good recent survey papers for programming languages as a whole or aspects? I know we have a "research papers" section, but it hasn't been updated in a while, as far as I know.

By Matt M at Mon, 2015-05-04 21:05 | login or register to post comments

What about the difference

What about the difference between working on better type systems for programmers vs. type theory research? It seems like the two topics have diverged a lot and it might be worth forking a body of knowledge (types for programming language designers vs. types for type theorists).

By Sean McDirmid at Sat, 2015-05-09 10:44 | login or register to post comments

It seems like the two

It seems like the two topics have diverged a lot and it might be worth forking a body of knowledge (types for programming language designers vs. types for type theorists).

I'm thinking PL designers would be more likely than type theorists to approve of this fork. (There's been a quote floating around for many years, with a slew of variations and no agreed-upon attribution, that the difference between theory and practice is small in theory but large in practice.)

By John Shutt at Sat, 2015-05-09 12:14 | login or register to post comments