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