Intuitionistic type theory in linguistics

Question

How important is type theory for modern formal linguistics? I am looking for modern references that build on Ranta's (Ranta, Aarne. "Type-theoretical grammar." (1994)) use of type theory for linguistics. Thank you.

Answer 1

It's really nice to know that there are some other guys who are interested in type-theoretical semantics. I will give you some advice and references that might be interesting.

First, there is a crucial difference between simple type theory that is used in the traditional Montagovian formal semantics (that is, something you would normally find in an introductory textbook on formal semantics like Heim & Kratzer (1998)) and modern type theory (that is, type theory after Martin-Löf type theory) that is now extensively applied to linguistic semantics ever since Ranta (1994). If you really want to play with type-theoretical semantics, it would be better that you can first get familiar with type theory itself. If you have a theoretical math or theoretical cs background, it would be easy. If you are a student of Linguistics, it would be a little bit difficult because modern type theory is more complicated than simple type theory. I would recommend Granström's book Treatise on Intuitionistic Type Theory, which gives you a friendly and less technical introduction to intuitionistic/constructive type theory.

Second, type-theoretical semantics is less well-known to mainstream semanticists. Most formal semantic research is still done within a classical (or old-fashioned?) Montagovian setting. Recently, more and more researchers, mainly theoretical computer scientists and some logic-oriented linguists find that type theory can offer a better mathematical foundation for linguistics semantics. There are two different branches.

1. Modern type-theoretical semantics, pursued by Aarne Ranta, Zhaohui Luo, Stergios Chatzikyriakidis, and Daisuke Bekki. They have published a lot of papers on lexical semantics and compositional semantics using modern type theory (mainly, Luo's ECC/UTT type theory and classical Martin-Löf type theory). I think Zhaohui Luo is the soul of this branch as his ECC is a widely acknowledged textbook theory and he has dedicated himself to the study of type-theoretical semantics for over ten years. Stergios was once a post-doc of Zhaohui. Bekki's theory, in particular, his type-theoretical analysis of presupposition resolution, is also inspiring.

2. Set-theoretical semantics with typed notations, pursued by Robin Cooper and his collaborators (Jonathan Ginzburg, Staffan Larson, etc). They are more interested in using typed notations to model linguistic interaction. The theory that they use is called TTR (type theory with records). It's a hybrid system because it's essentially set-theoretical but uses typed notations to increase the expressive power of the object language. You can check their websites and see their publications.

(PS: As far as I know, researchers of the two branches are now preparing textbooks or something like that for newcomers. Luo and Chatzikyriakidis are writing a book on type-theoretical semantics which I don't know when they will publish. Robin Cooper has a nice book manuscript circulated online for many years on TTR for modeling perception and linguistic phenomena related to that. You can check Robin's GitHub account.)

It is also worthwhile mentioning some other researchers such as Nicolas Asher and Christian Retoré. They also have published papers on type-theoretical semantics but not the main topic of their research.

Third, let's see whether type-theoretical semantics really fits your research. If you are interested in reasoning and related issues, I would say that type-theoretical semantics is perhaps much better than the traditional Montagovian or model-theoretical semantics. The main reason is that most proof assistants (Coq, Isabelle, ALF, ect) are developed based on type theory. So, you can easily check your analysis using these useful tools and implement your analysis if possible. However, if you just want to analyze certain linguistic phenomena, topics that linguists are normally interested in, such as the semantic interpretation of certain words, certain structures, or syntax-semantics interface, then it's not a good idea to turn to type-theoretical semantics because it is not well accepted by mainstream semanticists. A bad consequence of playing with a not well-accepted theoretical framework is that most mainstream semanticists, as far as I know, are usually unhappy to read papers using completely different frameworks and would regard you as an alien.

I hope it will help you.

Afterthought: There are some researchers, mainly mathematicians and theoretical computer scientists, who are now trying to apply homotopy type theory to linguistic semantics. But I once tried to talk to linguists, they were not quite interested and most complained that they cannot even understand this elegant theory, and cannot see why it's better than a traditional model-theoretical framework.