https://lawrencecpaulson.github.io/2023/03/08/Fun_Semantics.html

[utterances-bot]

The semantics of a simple functional language

https://lawrencecpaulson.github.io/2023/03/08/Fun_Semantics.html

[jonsterling]

Nice article and examples! I'm curious, who has promoted the myth that you need dependent types to do semantics? I've never heard it before, and I was a bit surprised since it doesn't make any sense anyway (for exactly the reasons you describe: 1970s!).

[lawrencecpaulson]

Probably a chance remark on FaceBook, but from a major figure. Especially in the USA, people do a lot of semantics in Coq.

[jonsterling]

I see! I would say this would be an extreme minority view among semanticists, even those of us who use dependent types or use Coq. Most people know that the first step to using Coq effectively is to avoid dependent types as much as possible and treat it like HOL. (This has more to do with the downsides of Coq's particular version of dependent type theory than with dependent type theory itself.)

[lawrencecpaulson]

I've heard something like that before! But in that case, why not just use HOL itself, or Isabelle/HOL? And what does Lean do differently?

[jonsterling]

It's a good question... I think that a lot of the kinds of projects PL semanticists people do in Coq these days would benefit from the use of Isabelle/HOL. There are a few reasons why nonetheless some people prefer to use systems based on dependent type theory, aside from sheer familiarity:

1. The informal/everyday mathematical vernacular has much more in common with dependent type theory than with HOL-style formalization. Aside from dependency in general (which appears all the time in ordinary mathematics, but can always be rewritten to avoid dependency), one of the big differences from HOL-style formalization is that in informal mathematical vernacular, there are no types: there are just sets, but these sets behave like a dependent type theory (it is unfortunate that the terminology of "types" is likely to lead to a lot of talk across purposes) — so someone who wishes to work with the sets of everyday mathematical vernacular may find dependent type theory to be a more natural way to do this than other formalizations of the idea of a set, e.g. those of HOL which add a new and unfamiliar layer of simple types that doesn't occur in the informal vernacular. It is of course possible to work with a single type, and develop a theory of sets in HOL (e.g. the formalization of ZFC), but this is an encoding that renders in an indirect way what dependent type theory renders in a direct style.

2. Many people are trying to work constructively, for a variety of reasons; some want to work constructively for what I perceive to be silly ideological reasons, and others want to work constructively because we are actually making use of the generality of constructive mathematics as a way to give much simpler proofs of classical results. For instance, if you prove some basic theorems of commutative algebra constructively, you can instantiate them in a certain topos and obtain much more sophisticated results of algebraic geometry for free — e.g. safely passing from ordinary modules to sheaves of modules, etc. This is the way that I use constructive mathematics. Anyway, this has absolutely nothing at all to do with dependent type theory, but the only mature tools that allow you to work constructively are dependent-type theoretic. If there were a version of Isabelle/IHOL with infrastructure and libraries as mature as those of Isabelle/HOL, many of us would be using it. But it remains unclear to me whether such a thing can exist, because many of the very wonderful aspects of the Isabelle/HOL approach to things really depend fundamentally on having a global choice operator. It becomes much harder to work in logic over simple types when you don't have global choice. You have to deal with partial operations much sooner and more explicitly than ever, and this is not easy.

---

Finally, regarding Lean, there's many differences between Lean's type theory and Coq's, but one of the big points is that Lean aims to have more definitional equalities than Coq. In some cases, this can mitigate the suffering that comes from dependency... But I have been thinking that adding more definitional equality isn't exactly the solution I want for a variety of reasons (though I don't have more to say about this now).

[lawrencecpaulson]

That's interesting, thanks! I would just make a few points in response.

1. It is never necessary to eliminate dependency; just avoid making everything a type.

2. I believe it is never necessary to resort to ZF unless you are formalising axiomatic set theory itself or require its specific techniques, like transfinite recursion.

3. The natural typed set theory that comes with higher-order logic works perfectly well for expressing a lot of the mathematical vernacular. Just as Russell and Church intended.

4. You can develop intuitionistic higher-order logic without choice, with only definite descriptions ("unique choice").

[nomeata]

Connor McBride has taken up the challenge and presents an Agda version of this formalization: https://github.com/pigworker/Samizdat/blob/main/ExampleSemantics.agda

[nomeata]

And here are two formalizations with Lean:

• One by Kyle Miller
• One using aesop (Lean’s version of auto) by Anand Rao.

Both not too shabby!

[theohonohan]

Perhaps this is off-topic, but I like the mention of an "airline reservation system"—presumably it is a stock example of a complex concurrent distributed system. It has a 1960s flavour, but at the same time I suppose it reflects a level of complexity and functionality which may remain a benchmark for large software projects. Does it reflect the current level of civilization, with more intricate systems to come in the future, or does it (like the 19th C railroad) represent a now more-or-less unchanging "converged" technology and social need which is likely to persist as a model and point of reference?

[gabriel-fallen]

@theohonohan

About five years ago I participated in development of an "airline reservation system". In Haskell. I don't work there for many years but the system is deployed to production, still running and I did successfully use it to find and book tickets on a couple of occasions.

From my experience there are three major challenges.

1. Integration with legacy GDS system. It's still extremely challenging for me to find any non-obscene words to describe this part. Imagine a bastard of COBOL and SQL — yeah, that's the "native tongue" of a GDS. Thousands of poor tech support specialists still have to read and write it every day to this day! That's horrible. The language makes you actually appreciate their "new and shiny" XML Web Services API. If only it covered all the necessary functions and queries...

2. Currencies. If your system is international, you really don't want to add EURs to JPYs without conversion. At an official conversion rate _for the date of transaction__. And other minor details you really want to get right unless you lose someone's money. Possibly lot of them.

3. Rules of the game are constantly changing. You need to calculate the cost of a route but that depends on interline agreements, promotions and other conditions currently set by the airlines involved. It can depend on the dates of the flights, number of passengers and luggage places, roundtrip or not, and so on and so forth... Meaning you have to essentially evaluate programs that you load at runtime and change regularly.

So no, I don't think it's a "solved problem", not in the real world. These systems get as complex as pretty much anything else.