In Montague semantics every expression has a semantic type, which fixes the kind of thing it
denotes: an individual ($e$), a truth value ($t$), a world ($s$), or a function from denotations
of type $a$ to denotations of type $b$ ($\langle a,b\rangle$). An intension, of type
$\langle s,a\rangle$, is a function from worlds; Montague's intensional logic has no type $s$ of
its own, and the two-sorted type theory of Gallin adds it. Later work adds sorts for degrees,
cardinalities, and events and states. Each type has a domain of possible denotations, built from
a set of individuals and a set of worlds, and the domain of a type that ends in $t$ is a Boolean
algebra, pointwise. A computation type is the type of a computation with an effect, such as
reading an environment or returning one of a set of alternatives, and its domain is the effect's
carrier of its result's domain.
Ty.Domain is reducible: a denotation of type ⟨e,t⟩is an E → Prop to every tactic and
instance, and the Boolean algebra of a type that ends in t is mathlib's Pi instance.
Ty.Domain.completeBooleanAlgebra builds that algebra by recursion on a type known to be
conjoinable, for statements about a type that is not concrete. The reader's carrier is the
function type itself, not ReaderT, and the carrier of alternatives is Set, not SetM, so that
a domain is a function type or a set to instance search; their map, unit and application are
therefore explicit. A set of alternatives is not conjoinable: two sets of alternatives coordinate
alternative by alternative, through the modes, and not by intersection.
The semantic types are the entities e, the truth values t, the worlds s, and the
functions fn a b (⟨a,b⟩) of two-sorted type theory (Gallin 1975), in which Montague's
intensions ⟨s,a⟩ are the functions from worlds (Ty.intens), together with the degree sort d
(Heim 2001, Wellwood 2015), the cardinality sort n (Sudo 2016, Scontras 2014,
Little et al. 2022), and the eventuality sort v (Davidson 1967, Parsons 1990).
Kratzer's type s of events, of which actions and states are subkinds (Kratzer 1996), is v,
not the worlds s, as are Hanink and Koontz-Garboden's states (Hanink & Koontz-Garboden 2025);
events and states are distinguished within it (Yu et al. 2023), not as two types. A
computation type comp f a is a computation with the effect f whose result is of type a
(Bumford & Charlow 2026).
The effects of computation types (Bumford & Charlow 2026): the reader of an environment of a
type, a computation that reads a value of that type, as an intension reads a world, and
indeterminacy, a computation with a set of alternative results, as an indefinite has.
The carriers of the sorts beyond Montague's entities and indices, the scale of degrees and
the eventualities, which are empty unless a model supplies them.
The type e denotes in E, t in Prop, d in the scale of degrees, n in ℕ, v in
the eventualities, s in W, ⟨a,b⟩ in Ty.Domain a → Ty.Domain b, so that an intension
⟨s,a⟩ denotes in W → Ty.Domain a, and a computation type in its effect's carrier.
The carrier of an effect: a computation that reads an environment of type ι is a function
from its denotations, and an indeterminate computation is the set of its alternatives.
An effect's application ⊛ of a computed function to a computed argument
(Bumford & Charlow 2026): the reader reads one environment for both, and indeterminacy applies
every alternative function to every alternative argument.
An effect's join μ (Bumford & Charlow 2026), flattening a computation of a computation: the
reader reads one environment for both, and indeterminacy unions the sets of alternatives.
A denotation in the Montague type system is a semantic type together with an M-computation
in the domain of that type. M := Id is the pure Heim & Kratzer 1998 carrier; effectful
denotations supply M.
The domain of a conjoinable type carries the pointwise complete Boolean algebra
(Partee & Rooth 1983). At a concrete type it is the instance Pi.instCompleteBooleanAlgebra finds
statically.