I remember, from maybe grad school, being puzzled about “semantics”.  What does this word mean?  Having gained a lot more knowledge of this topic since then, I thought I’d share a few thoughts on it, especially in the context of type theory.

“Semantics” means meaning.  In this sense, many different approaches to the study of programming languages are described as giving some form of semantics to a language.  An interpreter gives you a semantics for a language.  It shows you what these funny sequences of keywords or symbols (or more modernly, these peculiar abstract syntax trees) mean by showing how the programs execute.  If one writes an interpreter as a set of inference rules, then this is usually called operational semantics.  Hoare Logic, which is a set of inference rules for verifying that programs started in states satisfying a given precondition will (if they terminate) end in a state satisfying a given postcondition, has traditionally been dubbed axiomatic semantics.  This term “axiomatic” is maybe not too informative, but the idea that you can describe the meaning of an imperative program by explaining how it changes the state indeed gives it a reasonable claim to be a semantics.  What do programs in the language mean?  A semantics tells you.

There was a lot of interest in earlier days on giving denotational semantics to programs.  The idea is to give the meaning of a program by stating what mathematical function the program denotes.  After all, programs are intended (are they not?) to represent some class of functions as understood in mathematics.  A hallmark of denotational semantics is that it is compositional: the meaning of a bigger expression is defined in terms of the meanings of its strict subexpressions.  Notice that this is not true of operational semantics generally: we define the meaning of $(\lambda x.\, t)\ t'$ in terms of $[t'/x]t$, which is not a strict subexpression of $t$ (indeed it can be a bigger term than $t$). There was a lot of excitement, it seems, in finding denotational models of languages like lambda calculus.  More recently, it seems more common, at least in Computer Science, to take lambda calculus for granted and not be concerned with mathematical denotations of lambda terms.

Logic is, as far as I know, the earliest field concerned with giving mathematical semantics for formal languages.  There, denotational semantics of formulas is the basis of model theory.  Proof theory can also be viewed as giving a semantics of formulas, and indeed in nice situations these two semantics agree — though even for theories like first-order arithmetic, results like Goedel’s incompleteness theorem imply that no such agreement is possible: the proof-theoretic semantics (showing what formulas mean by showing how to prove them or use them in other proofs) must be weaker, in the sense of proving fewer theorems, than the denotational semantics.  But maybe this is a digression…

In type theory, there is a great tradition of giving denotational semantics for types.  In full generality, if we have a term t of type T (in some typing context G!), we would like to explain what this relation ($G \vdash t : T$) means.  Historically, it was discovered that one could use a denotational semantics for types as a proof method to show deep properties of the language, like normalization or logical consistency.  I first learned about this in Girard’s Proofs and Types, and still recommend this as a good introduction.  The historical root of this is Kleene’s realizability semantics for first-order intuitionistic arithmetic.  But one does not need to be driven by the desire to prove such metatheorems, in order to want to have a denotational semantics for types.  Here are my amazing new types!  Wouldn’t you like to know what they mean?  I can show you some typing rules, and depending on how I set them up — for example, if you give introduction and elimination rules for the types that are related in certain ways — these could to a greater or lesser extent show you what the types mean.  But a compositional semantics that says, “my funny type construct X A B means …” can be more direct, and provide guidance for crafting typing rules.  One can prove that a set of typing rules is sound with respect to the semantics, for example.

The form of such semantics I have found most useful is a realizability semantics, that tells you what a type means by specifying the set of all terms whose operational behavior is allowed by the type.  For example, in some language, the meaning of a type like “Int -> Int” could be defined to be the set of all programs which, given an Int input, either diverge or produce an Int output.  Or maybe in some other language, it is the set of all terms which, given an Int input, are guaranteed to terminate producing an Int output.  Notice that these example semantics do not say anything about the internal form of the program.  It could fail to be well-typed according to some set of typing rules.  It could do very crazy and upsetting things if not given an Int input.  The only thing the type specifies is the behavior of the term when given an Int input.  So the type describes behavior of terms, through the simple device of giving a set of terms as the meaning of a type (namely, the set of all terms whose behavior is allowed by the type).

For Cedille, I have defined such a semantics, and used it to prove logical consistency of the system.

1. I took a look at the Cedille semantics linked from this post. I’m surprised to see that you’re using sets of equivalence classes for types. How come?

2. This provides a simple concrete semantics that also justifies the conversion rule. The interpretations of P t and P t’ are exactly the same if t and t’ are beta-eta equivalent.

But maybe you could some more about what you find surprising in the choice of semantics? Perhaps you were looking for something more general, like interpreting types into some structure based on combinatory algebras? I am not opposed to such endeavors, I just wanted something concrete and simple.

• My surprise is not because it’s different from what you discussed in the post, or that it’s not more general, but that it seems more complex than necessary.

If you defined the reducibility candidates to be the sets of closed terms that respect beta-eta equivalence, I think the clauses of the interpretation could be simplified.

In other words, a reducibility candidate T would satisfy the property that for all closed terms t and t’, if t and t’ are beta-eta equivalent, then t ∈ T implies t’ ∈ T.

This requirement may be not quite right in your setup, since you seem to be mixing annotated and unannotated terms into one metalanguage type. That surprised me too.

• OK, I took another look at your semantics. You are restricting beta-eta equivalence and equivalence classes to (unannotated) closed terms of the pure lambda calculus. So I think my proposed formulation of respect should work as-is. Reducibility candidates would be respectful sets of closed terms of the pure lambda calculus.

3. Oh, now I can see an obvious point to your question: in the post I am talking about interpreting types as sets of terms, while in the Cedille semantics I interpret them as sets of beta-eta equivalence classes of terms. This shows that really I should be saying we have some interpretation of terms, and then interpret types as sets of those term interpretations. The term interpretation could be into some combinatory algebra, for example, and this would fit what I did concretely in the Cedille semantics, as beta-eta equivalence classes of terms form a combinatory algebra.

4. I noticed some problems in the paper that should be easy to fix:
– You don’t have a judgment to check against a kind (not synthesize), but your rule to apply a type element to a kind element uses it anyway.
– Your rule to apply a type-level function to a kind element looks wrong. It has an equivalence premise between the domain and codomain of the function. I think this should be comparing the kind of the argument to the domain, but as written, they’re syntactically equal.
– Typesetting glitches in a paragraph on page 5.

5. Hi, Matt. Thanks for the fixes for the document. I will incorporate these.

About this question of whether to interpret types as beta-eta closed sets of (closed) terms, or sets of closed-beta-eta equivalence classes of terms: in fact, we need the latter, and I am glad for your question as I can explain why. Suppose we have some type P of kind Unit -> *, where let us suppose we have unit as the sole normal-form inhabitant of type Unit. If we interpret types the way you are suggesting, the meaning of this P will be some function F from the set of closed terms beta-eta equivalent to unit, to a reducibility candidate (i.e., a semantic type).

This semantics will allow functions F which do not respect beta-eta equivalence. For example, we could have an F which returns the empty set when given unit, but returns the set of all normalizing terms when given ((\ x . x) unit). Just saying that semantic types are beta-eta closed does not prevent functions over those types from being incompatible with beta-eta equality.

The solution adopted in my paper solves this problem, because F is not presented with a term, but rather a beta-eta equivalence class of terms.

Notably, if one wants to make an extensional version of Cedille (which we thought quite a bit about but did not seriously attempt yet), the semantics would need to say that F respects not just beta-eta equivalence, but rather extensional equality at the domain type.

• > This semantics will allow functions F which do not respect beta-eta equivalence…

You are right. I thought it went without saying that you’d need to replace equality of equivalence classes with equivalence of terms throughout the development. Not replace it with (syntactic) equality of terms. Since equality is often used implicitly in math, this takes a bit of thought. In particular you’d need to restrict to respectful metalanguage functions too.

There must be a way to fix the rest of the semantics when using respectful sets of terms, because classically, beta-eta-respectful sets of terms and sets of beta-eta equivalence classes of terms are isomorphic. Working out the details of the semantics using respectful sets is an exercise in transporting the development across the isomorphism.

If this seems more complicated to you than equivalence classes, OK. A nice thing about avoiding equivalence classes is that I think you can also avoid the choice function. I think you’d need to avoid equivalence classes to get a constructive metatheory. But of course that’s not important for many people. I don’t want to twist your arm.

By the way, if you add any non-lambda to the set of realizers, like a primitive unit, you probably ought to give up on untyped eta expansion. (\x. unit x) is not the same as unit, because the former ought to be undefined or erroneous. Once you have typed function extensionality, you get typed eta expansion.

> Notably, if one wants to make an extensional version of Cedille (which we thought quite a bit about but did not seriously attempt yet), the semantics would need to say that F respects not just beta-eta equivalence, but rather extensional equality at the domain type.

Yup. So if you decide to stick with equivalence classes, you can avoid PER semantics too. You’d just allow types to use equivalence classes for various equivalence relations, not always beta-eta.

I’ve gotten used to using things like sets of terms and PERs on terms. A nice thing about them is that they’re closer in style to the judgments used in the rules. For example, with PER semantics, the meaning of the judgment (t = t’ : T) is simply to apply the pair (t,t’) to the PER for T.