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

[Talia Ringer]

Somewhat of a complementary question, and proof to the world that I'm up at
330 AM still thinking about this:

Are there interesting or commonly used logical axioms that we know for sure
cannot have computational interpretations?

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

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear Sandro,
>
> Yes, you're right -- I didn't answer the question, since I was too
> taken by the subject line. :)
>
> Anyway, I do think that HoTT with a non-reducible univalence axiom is
> still a programming language, because we can give a computational
> interpretation to that language: for example, you could follow the
> strategy of Angiuli, Harper and Wilson's POPL 2017 paper,
> *Computational Higher-Dimensional Type Theory*.
>
> Another, simpler example comes from Martin Escardo's example upthread
> of basic Martin-Löf type theory with the function extensionality
> axiom. You can give a very simple realizability interpretation to the
> equality type and extensionality axiom, which lets every compiled
> program compute.
>
> What you lose in both of these cases is not the ability to give a
> computational model to the language, but rather the ability to
> identify normal forms and to use an oriented version of the equational
> theory of the language as the evaluation mechanism.
>
> This is not an overly shocking phenomenon: it occurs even in much
> simpler languages than dependent type theories. For example, once you
> add the reference type `ref a` to ML, it is no longer the case that
> the language has normal forms, because the ref type does not have
> introduction and elimination rules with beta- and eta- rules.
>
> Another way of thinking about this is that often, we *aren't sure*
> what the equational theory of our language is or should be. This is
> because we often derive a language by thinking about a particular
> semantic model, and don't have a clear idea of which equations are
> properly part of the theory of the language, and which ones are
> accidental features of the concrete model.
>
> For example, in the case of name generation – i.e., ref unit – our
> intuitions for which equations hold come from the concrete model of
> nominal sets. But we don't know which of those equations should hold
> in all models of name generation, and which are "coincidental" to
> nominal sets.
>
> Another, more practical, example comes from the theory of state. We
> all have the picture of memory as a big array which is updated by
> assembly instructions a la the state monad. But this model incorrectly
> models the behaviour of memory on modern multicore systems. So a
> proper theory of state for this case should have fewer equations
> than what the folk model of state validates.
>
>
> Best,
> Neel
>
> On 19/05/2021 09:03, Sandro Stucki wrote:
> > 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
> > <mailto:neelakantan.krishnaswami at gmail.com>> wrote:
> >
> >     [ The Types Forum,
> >     http://lists.seas.upenn.edu/mailman/listinfo/types-list
> >     <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
> >     <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
> >      >
> >
>