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.

  • 1
    Well, Ranta was writing about computer languages (where typing is obviously an important concept) but computer languages aren't studied by linguists. Dec 16, 2020 at 16:49
  • I’m voting to close this question because this is a question on a concept from computer languages. Dec 16, 2020 at 16:49
  • 3
    Not everything that has the word "formal" in it is automatically off-topic for this site; neither is it just because it originates from/also has applications in other fields. The question explicitly asks about the use of this theory in linguistics; I see no problem having it here. Type-theoretic natural language semantics is a thing.
    – lemontree
    Dec 16, 2020 at 18:04
  • @JRC I think you need to specify more precisely what you're after. Are you looking for an assessment of how fruitful type theory is for linguistic applications? A list of recent papers discussing linguistic phenomena with methods of type theory? A modern textbook that covers the basics of type-logical grammar/semantics, or advanced topics?
    – lemontree
    Dec 16, 2020 at 18:09
  • 1
    Type theory predates computers by a couple of generations.
    – user6726
    Dec 16, 2020 at 19:46

1 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.

  • 4
    This is really a good answer! Thanks a lot!
    – Kelly
    Dec 16, 2020 at 20:05
  • 1
    I had a very similar experience. I tried to talk to some linguists about type theory and category theory, but they kept asking me for example words and example sentences. Finally, I gave up...
    – Emini Jask
    Dec 16, 2020 at 21:27
  • You might be interested in answering this question: What explanatory advantages does so-called “type theory” have?
    – curiousdannii
    Dec 16, 2020 at 23:01
  • @curiousdannii It appears that there is already a good answer there. Lemontree's answer is much more detailed than mine. :-)
    – Fred
    Dec 17, 2020 at 0:01
  • 1
    @Fred Thanks. This is so helpful, including the after-thought.
    – JRC
    Dec 17, 2020 at 10:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.