[TYPES] What's a program? (Seriously)

[Neel Krishnaswami]

Dear Talia,

Here's an imprecise but useful way of organising these ideas that I
found helpful.

1. A *language* is a (generalised) algebraic theory. Basically, think
    of a theory as a set of generators and relations in the style of
    abstract algebra.

    You need to beef this up to handle variables (e.g., see the work of
    Fiore and Hamana) but (a) I promised to be imprecise, and (b) the
    core intuition that a language is a set of generators for terms,
    plus a set of equations these terms satisfy is already totally
    visible in the basic case.

    For example:

    a) the simply-typed lambda calculus
    b) regular expressions
    c) relational algebra

2. A *model* of a a language is literally just any old mathematical
    structure which supports the generators of the language and
    respects the equations.

    For example:

    a) you can model the typed lambda calculus using sets
       for types and mathematical functions for terms,
    b) you can model regular expressions as denoting particular
       languages (ie, sets of strings)
    c) you can model relational algebra expressions as sets of
       tuples

2. A *model of computation* or *machine model* is basically a
    description of an abstract machine that we think can be implemented
    with physical hardware, at least in principle. So these are things
    like finite state machines, Turing machines, Petri nets, pushdown
    automata, register machines, circuits, and so on. Basically, think
    of models of computation as the things you study in a computability
    class.

    The Church-Turing thesis bounds which abstract machines we think it
    is possible to physically implement.

3. A language is a *programming language* when you can give at least
    one model of the language using some machine model.

    For example:

    a) the types of the lambda calculus can be viewed as partial
       equivalence relations over Gödel codes for some universal turing
       machine, and the terms of a type can be assigned to equivalence
       classes of the corresponding PER.

    b) Regular expressions can be interpreted into finite state machines
       quotiented by bisimulation.

    c) A set in relational algebra can be realised as equivalence
       classes of B-trees, and relational algebra expressions as nested
       for-loops over them.

   Note that in all three cases we have to quotient the machine model
   by a suitable equivalence relation to preserve the equations of the
   language's theory.

   This quotient is *very* important, and is the source of a lot of
   confusion. It hides the equivalences the language theory wants to
   deny, but that is not always what the programmer wants – e.g., is
   merge sort equal to bubble sort? As mathematical functions, they
   surely are, but if you consider them as operations running on an
   actual computer, then we will have strong preferences!

4. A common source of confusion arises from the fact that if you have
    a nice type-theoretic language (like the STLC), then:

    a) the term model of this theory will be the initial model in the
       category of models, and
    b) you can turn the terms into a machine
       model by orienting some of the equations the lambda-theory
       satisfies and using them as rewrites.

    As a result we abuse language to talk about the theory of the
    simply-typed calculus as "being" a programming language. This is
    also where operational semantics comes from, at least for purely
    functional languages.

Best,
Neel

On 18/05/2021 20:42, Talia Ringer wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hi friends,
> 
> I have a strange discussion I'd like to start. Recently I was debating with
> someone whether Curry-Howard extends to arbitrary logical systems---whether
> all proofs are programs in some sense. I argued yes, he argued no. But
> after a while of arguing, we realized that we had different axioms if you
> will modeling what a "program" is. Is any term that can be typed a program?
> I assumed yes, he assumed no.
> 
> So then I took to Twitter, and I asked the following questions (some
> informal language here, since audience was Twitter):
> 
> 1. If you're working in a language in which not all terms compute (say,
> HoTT without a computational interpretation of univalence, so not cubical),
> would you still call terms that mostly compute but rely on axioms
> "programs"?
> 
> 2. If you answered no, would you call a term that does fully compute in the
> same language a "program"?
> 
> People actually really disagreed here; there was nothing resembling
> consensus. Is a term a program if it calls out to an oracle? Relies on an
> unrealizable axiom? Relies on an axiom that is realizable, but not yet
> realized, like univalence before cubical existed? (I suppose some reliance
> on axioms at some point is necessary, which makes this even weirder to
> me---what makes univalence different to people who do not view terms that
> invoke it as an axiom as programs?)
> 
> Anyways, it just feels strange to get to the last three weeks of my
> programming languages PhD, and realize I've never once asked what makes a
> term a program 😅. So it'd be interesting to hear your thoughts.
> 
> Talia
>