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

[Sandro Stucki]

Talia: thanks for a thought-provoking question, and thanks everyone else
for all the interesting answers so far!

Neel: I love your explanation and all your examples!

But you didn't really answer Talia's question, did you? I'd be curious to
know where and how HoTT without a computation rule for univalence would fit
into your classification. It would certainly be a language, and by your
definition it has models (e.g. cubical ones) which, if I understand
correctly, can be turned into an abstract machine (either a rewriting
system per your point 4 or whatever the Agda backends compile to). So
according to your definition of programming language (point 3), this
version of HoTT would be a programming language simply because there is, in
principle, an abstract machine model for it? Is that what you had in mind?

Cheers
/Sandro


On Wed, May 19, 2021 at 6:21 AM Neel Krishnaswami <
neelakantan.krishnaswami at gmail.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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
> >
>