Some linguists use a theory called "type theory"; you can see it in a few questions on this site.

Apparently it is based on the "type theory" of maths, logic, and computer science. Wikipedia's description of the specific form used by linguists, where everything is reduced to "e"s and "t"s, is very short and doesn't really explain it in a way that makes much sense to someone who isn't already familiar with it, and its maddeningly generic name means it's quite hard to find out more about it.

I can't see the sense in reducing everything in a language to either an "e" or a "t". But I presume there must be a reason for doing so. So what explanatory power and advantages does this theory have? What syntactic or semantic phenomena can type theory explain or analyse better than other theories of formal semantics? (Or even regular syntax/semantics!)

  • 2
    It appears that type theory is a phrase of art in what's known in linguistics as "Montague grammar", named after the late philosopher Richard Montague. It's an Ajdukiewicz-style categorial grammar, not really useful for describing natural language, in most cases, though Schmerling's version looks interesting.
    – jlawler
    Commented Feb 29, 2020 at 3:57
  • @jlawler Actually, categorial grammar provides the basis for Gazdar's demonstration that PSG can, after all, describe unbounded movements without transformations. That is useful to know.
    – Greg Lee
    Commented Feb 29, 2020 at 4:14
  • 1
    I know of this book on the topic, haven't read it though. Commented Feb 29, 2020 at 7:05
  • This book is the one by Schmerling that I referred to.
    – jlawler
    Commented Feb 29, 2020 at 17:33
  • 1
    Probably the best explanation I've come across is in the book by L.T.F. Gamut, Volume 2: Intensional Logic and Logical Grammar, Chapter 4, pg. 75-91. Very briefly, parts of sentences are modeled as type expressions that apply on each other in a mathematically well-defined manner. Categorical Grammar is very similar to type theory.
    – prash
    Commented Feb 29, 2020 at 17:49

3 Answers 3


I can't see the sense in reducing everything in a language to either an "e" or a "t".

Maybe this is a good place to start. Type theory (more accurately: so-called simple type theory with e and t as atomic types, which is what most linguists mean when they say "type theory") doesn't reduce everything to either e or t: It reduces everything to combinations of e and t. This may seem like nitpicking, but that's where the true power of type theory comes from: We can take existing types and build new ones from them, and there is no limit to the complexity of types we can build. Like syntax, semantics is recursive!

e and t are the atomic types that can not be decomposed any further.
e stands for "entity" and is the semantic type of terms, i.e. expressions which denote individuals: people, objects, numbers, ...
t stands for "truth value" and is the semantic type of sentences.

We can combine these types to function types: An expression of type ⟨a,b⟩ is something that takes an expression of type a as an input and outputs an expression of type b. Of course, a and b may themselves be complex, thereby allowing unlimited recursion.

  • 1-place predicates like "is-a-woman" are of type ⟨e,t⟩: You put in an individual, you get out true or false.
  • 2-place predicates like "love" are of type ⟨e,⟨e,t⟩⟩: You put in an individual, you get something where you put in another individual, and get out true or false.
  • 1-place function symbols like "father-of" are of type ⟨e,e⟩: You put in an individual, you get out another individual.

Combining a function expression of type ⟨a,b⟩ with an appropriate argument of type a yields a new well-formed expression which has type b: For example, applying the 1-place function "father-of" of type ⟨e,e⟩ to the argument "Mary" of type e leads to a complex expression "father of Mary" which is another e, and using this term as an input to the predicate "is-a-woman" of type ⟨e,t⟩ leads to the sentence "The father of Mary is a woman" which has a truth value t.

is-a-woman (father-of (Mary)) 
    |            |      |
    |          <e,e>    e
    |            |      |
    |             ------ 
    |               |    
  <e,t>             e    
    |               |    

Up until now, this is nothing special: We just described the language of first-order logic. But we can build more types:

  • Properties of properties such as "is-a-color" are of type ⟨⟨e,t⟩,t⟩: You put in a 1-place predicate like "red", you get out a truth value.
  • Predicate modifiers such as "quickly" are of type ⟨⟨e,t⟩, ⟨e,t⟩⟩, You put in a 1-place predicate like "run", you get out a new 1-place predicate, "run-quickly".

All the expressions in the first block only took inputs of type e: They are expressions of first order. The predicates, functions and quantifiers of first-order (~= standard) predicate logic only range over individuals.
But now we have expressions that allow predicates as arguments: We have expressions of second order. This is something new -- the language standard predicate logic does not allow for such expressions.¹ It is easy to see that we can iterate this further and get expressions of even higher order, i.e. properties of properties of properties and the like.

So here is the first advantage:

1. Standard predicate logic is too weak

Type theory has an explanatory advantage over formal semantics with standard predicate logic only, because it can account for the types of more expressions. Expressions that can not be systematically treated by standard predicate logic but by type theory include:

  • properties and relations of properties and relations (such as "is a color", "is a brighter color than")
  • predicate modifiers and adverbials (such as "quickly", "very")
  • relative adjectives (such as "small")
  • prepositions (such as "next to")
  • quantifiers like "most", "more than", "infinitely many"

These are all expressions that are perfectly common natural language expressions, but can not be systematically analzyed with first-order logic. This is of course quite a limitation overcome.

Now translating natural language into a formal language doesn't yet explain anything. But one of the goals of building up a powerful enough formal language will be that this servers as a basis for a likewise powerful semantics: If we want to give a systematic account of sentences that speakers reason about, then we need a means to adequately express these sentences in the first place, on top of which a standard semantics for typed lambda calculus encorporating higher order logic is defined.

2. Type theory can explain semantic mismatches

It should be pointed out that it is not the language of type theory which makes these expressions formalizable: Rather, it is logics of higher order which provide the formal langauge as a basis for translation, most notably higher-order logic in lambda calculus, which may be attributed the status of the de facto lingua franca of formal semantics.
The role of type theory now is to

  • 1) guide the syntax of these more powerful langauges: Complex expressions can only be built if the types of its components match, in the sense that an argument fits into the function according to their type specifications.
  • 2) give an account of an aspect of the semantics of these more powerful langauges: The type of a complex expression can be computed from the type of its component expressions. A nice feature of this semantics is that it is compositional.

The cool thing about type theory is that we can systematically calculate why, for example, combining "red" with "is a color" leads to a sentence that has a truth value², or why "Mary is quickly" is not well-formed (namely because there is a type mismatch: "quickly" expects a property as an argument but gets an entity instead).

This is is the point where one could say there is some explanatory, rather than merely a descriptive value to this theory.
This also leads us to the next advantage:

3. Type-theoretic semantics works neatly with categorial grammar

Cateogrial grammar is a syntax theory developed to be tightly connected with a semantics as outlined above. The idea is to distinguish grammatical constituents by a semantic type, or category, that simultaneously describes the expressions it can syntactically combine with and its semantic value.
For instance, the category of a transitive verb like "eat" is (s\np)/np: It is an expression that becomes a sentence when it is first combined with an object on the right ("/np") and then a subject on the left ("\np"). Determiners like "a" are of category np/n: They are missing a noun to become an NP. Here is an exemplary syntax tree in categorial grammar:

Mary    eats     an  apple
---- ---------- ---- -----
 np  (s\np)/np  np/n   n  

These categories can later be interpreted in terms of the standard type theoretic formalism.

  • From a theoretical perspective, it is desirable to have a theory of syntax and a theory of semantics in systematic interaction with each other and expressible in a unified formalism, rather than syntax and semantics somewhat drifting apart, as has often been the case in the historical development of linguistic theories.
  • Categorial grammar only has a few abstract rules; much of the syntax can be derived on the basis of the lexical items. (Whether this is indeed an advantage may be disputed.)
  • Combinatory categorial grammar (some later improvement of pure categorial grammar) is supposed to be better at dealing with non-constituent-like strings and languages with more free word order than context-free grammars are, while at same time avoiding overgeneration issues known from transformational grammars.
  • Categorial grammar is apparently straightforward to implement, in the same breath with a computation system for its type-theoretic semantics, due to its lexical nature can be trained with corpora to achieve wide coverage, and can be augmented with probabilistic components to make it more robust.


In short,

  • type theory can deal with the syntax and semantics of a number of expressions that standard predicate logic can't,
  • it can explain certain syntactic/semantic mismatches,
  • thereby in a natural way gives rise to a syntactic theory that performs well in some aspects that context-free or transformational grammars have problems with,
  • type theoretic semantics is compositional, and
  • its ontology is minimalist.


Greater power comes with worse tractability. In the transition to higher-order logic and type theory, we lose a number of properties that keep standard predicate logic still relatively handleable; most notably:

  • semi-decidability: There is no algorithm that detects for any valid inference in finite time that it is valid. In first-order logic we can at least detect the valid inferences (though not all the invalid ones, which is why FOL is said to be undecidable, but semi-decidable), but already for second-order logic it is not even possible to recursively enumerate all the inferenes that do hold. I.o.w., we can not possibly write a computer program that always confirms the validity of a given argument involving higher order expressions.
  • completeness: There is no syntactic proof system like natural deduction that can formally derive all the semantically valid inferences. I.o.w., just because something holds doesn't always mean we can formally prove it.
  • compactness: A valid inference may require infinitely many premises.

The computational complexity of higher order logic and type theories is one of the main concerns against them, not only for implementational purposes, but also in terms of psychological plausibility. Bluntly said, noone really understands logic and not even computers can fully handle it, so how could this be adequate as a model of how humans use natural langauge?
One can now argue against this by saying that one doesn't necessarily need full type theory, but only a fragment that may be less terrible; but defining precisely what kind of intermediate system constitutes a minimally complete theory of natural language, and determining its position on a complexity scale, is not a trivial problem.

Also, types can get big: The semantic type required to make coordination between NPs (such as "a man or woman") combine in a well-behaved manner is already as complex as ⟨⟨⟨e,t⟩,⟨⟨⟨e,t⟩,t⟩⟨⟨e,t⟩,t⟩⟩,⟨⟨⟨e,t⟩,⟨⟨⟨e,t⟩,t⟩⟨⟨e,t⟩,t⟩⟩,⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩,⟨⟨e,t⟩,t⟩⟩⟩.


¹ One may now wonder why one can't just model higher-order expressions in terms of first-order ones: For example, one may treat "is-a-color" as a 1-place first-order predicate that applies to a term "red" which serves as a first-order individual constant, just like "Mary" or "3" does. But this hack doesn't really do the trick:
For one, it doesn't do justice to the intuition that "red" is indeed not just an object, but rather a predicate that can be applied to objects, and just stipulating that there are two lexical items "red", one that behaves as a predicate and one that behaves as an object, is not a very satisfactory explanation of its syntax and semantics.
Second, even if such a trivialization does allow us to express higher-order expressions, it still doesn't allow to systematically analyze them. For example, from "Mars is red" and "Red is a color" we would want to infer that "Mars has a color". But if we assume that "red" in the second sentence is a term so that a first-order predicate "color" can be applied to it, then it can not simulataneously be a predicate in the first sentence. And if we claim that "red" and "red" in the two sentences are different expressions that aren't substitutible for one another, then we can not apply rules of inference to them to systematically derive the desired conclusion.
This limitaiton (amongst others) is precisely what is overcome by explicitly allowing for predicate and function symbols of higher order.

² Now justifying type theory because it allows us to calculate types may seem somehwat circular at first. But I think it is not illegitimate to claim that speakers do have intuitions like "Red is a color" being something they can judge as true or false, and certainly about something being off with "Mary is quickly". Type theory is one way of explaining why, and that with a really simple ontology consisting of just two basic types and one rule for composition, compared to much more heavy loaded syntax theories.


If you would like to read up more, I would recommend Gamut (see prash's comment); its chapter on type theory is essentially a more detailled exposition of what I outlined here. The book is rather technical, but provides accessibly written introductory motivations and comments on the introduced formalisms, and that combination makes it a pretty good resource IMO.
Partee, ter Meulen & Wall (1990), "Mathematical methods in linguistics", in their chapter on "English as a formal language" also give an introduction to type-theoretic semantics, explaining the type system directly starting with typed lambda calculus.

That being said, everything I wrote here is based on my rather old-school linguistics education; it may well be that some of the alleged advantages and possible shortcomings of type theory and categorial grammar by now have been overcome by better theories; and on the other hand I'm sure research over time has given rise to more phenomena being explained in terms of type-theoretic semantics. For the latter, the book linked by András Kovács in the comments looks promising.

  • 2
    About the other semantic types you mention unfortunately I don't know, but my guess would be that the e,t, type system is too coarse-grained to be able to capture that, so this would be a possible shortcoming, and not really useful in a fine-grained analysis of a language's grammatical features. The purpose of e,t type theory from what I've seen seems to be more to give a very general, theoretically "aesthetic" account of how composing expressions works on the interface between syntax and semantics, not really for a detailed analysis of a language's grammatical and semantic features. Commented Mar 1, 2020 at 22:52
  • 1
    @Atamiri Thanks for that info. Can you give me a literature pointer on these more well-behaved variants? I only know they exist, not what they look like exactly. This is part of what I wanted to capture in the disclaimer below the downsides list; do you think the possibility of rescuing of HOL is not clear enough from that paragraph and should be reformulated? Commented Mar 1, 2020 at 22:57
  • 1
    @Atamiri Thanks! I'll look into it and probably extend that disclaimer paragraph. Commented Mar 1, 2020 at 23:14
  • 1
    @curiousdannii Addendum to subcategorization: Type theory can describe subcategorization on the level of the syntactic category of the arguments, but with just e,t as atomic types, not for semantic features like "animate". In addition, the linear order of the functor and its arguments is not systematically recognized in type theory; this is something that categorial grammar (which is primarily a syntactic theory) resolves. Commented Mar 1, 2020 at 23:17
  • 2
    The adverb "very" modifies adjectives, but for some reason, we don't have *"Very red is a color". Why do you suppose that is? Could it be that the "red" that can occur as subject is not actually an adjective at all, but rather a noun? There is nothing in traditional grammar that prevents a word occurring as both adjective and noun.
    – Greg Lee
    Commented Mar 2, 2020 at 3:27

Type theory avoids the paradoxes in set theory that were discovered early in the last century, e.g. Russell's paradox. It is not the only way to avoid the paradoxes. It is often used in the formal development of higher order logics. I am not aware of any reason to use it for linguistics, other than the popularity of Montague grammar, which does use higher order logic.

"e" is short for "entity", which is the semantic counterpart of an argument to a predicate, and "t" is short for "truth value", which is the semantic counterpart of a predication. Semantic logic theories use those independently of whether they use type theory.

The notation <e,t> is used for the type of a one place function which has arguments of type e and values of type t. For instance "Socrates is mortal" is a predication of type t (it is true or false), one argument of type e ("Socrates"), and a predicate of type <e,t> ("is mortal"). Semantic functions may also have arguments of complex types, so that functions of much more complex types can be described. Another basic type "w" is often added for "possible world" to incorporate modality into the description.

What explanatory advantage does all this have? In my opinion, none at all. It has considerable descriptive value, though. Some interesting and intricate semantic descriptions have been given using Montague Grammar.

  • 1
    I added some more to my answer. I had trouble showing angle brackets, though. There are some extra asterisks that don't belong.
    – Greg Lee
    Commented Feb 29, 2020 at 21:53

There are many “type theories.” In mathematics, Russell used a simple one to resolve paradoxes in set theory, but there are now other ways to get rid of them. Relevant to linguistics is Church’s “simple theory of types” which is basically just typed λ-calculus. This formalism is very useful since higher-order logic can be embedded in it. Furthermore it has been shown that as a formal logic it’s complete. So the emphasis is on “λ-calculus” rather than types. It has been used to resolve figurative constructions such a metaphors and metonymy in computational linguistics.

  • 2
    There may be many type theories, but I'm asking specifically about the one that reduces everything to es and ts, and what explanatory advantages for linguistics it has compared to other theories of syntax semantics, formal or otherwise. Resolving paradoxes in set theory isn't really relevant to that. Merely being able to resolve metaphors doesn't seem like much of an advantage, unless you're saying this is the only theory applied to computational linguistics that can do that?
    – curiousdannii
    Commented Mar 1, 2020 at 12:27
  • It's no great surprise that type theory is complete, but is it consistent? First order predicate logic is both complete and consistent.
    – Greg Lee
    Commented Mar 2, 2020 at 3:33
  • 1
    It actually is a great surprise since HOL can be easily embedded in it. And yes, it’s consistent, no sane theory of formal logic can be inconsistent.
    – Atamiri
    Commented Mar 2, 2020 at 9:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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