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

[Martin Escardo]

On 18/05/2021 22:18, Talia Ringer wrote:
>     For example, if I write a proof in Agda, using function extensionality,
>     is it a program? No. But if I write --cubical in the header of my Agda
>     program and import a suitable cubical library, then yes. I can define an
>     integer using function extensionality so that Agda will get stuck trying
>     to compute it but Cubical Agda won't (and I have done it in the cubical
>     library as an illustrative example).
> 
> 
> No wrong answers here, but I'm curious: What makes a proof in Agda using
> functional extensionality different in your mind from a function that
> takes a proof of functional extensionality as an input, and then returns
> the proof? Is the latter a program? Is the latter a program once you
> turn on --cubical, since now it has inputs? Do programs need to have
> realizable inputs?

In my preferred view of the world, computable functions don't need to
have computable inputs. (I am a K2 person.)

Many theorems are of the form "A -> B".

If you can do this, then you can do that.

I would regard a constructive proof of A -> B as a program, before I
know whether A "can be done" (or how).

Take e.g. A = function extensionality and B = integers.

Let f : A -> B be some constructive proof / program.

If I want to compute an integer from f, now I do need to supply some a:A.

This is what cubical Agda can do but Agda can't: supply the necessary
input to be able to *use* the program f to get an integer. Similarly in
Agda you can prove Univalence -> Blah, but you won't be able to supply
an input to run this proof, although you will be able to so in Cubical Agda.

By the way, here is another more concrete example of a pair of things
that are realizable but contradict each other: the univalence axiom and
the uniqueness-of-identity-proofs axiom. Cubical Agda has the former,
and Agda has the latter by default (although it can be disabled).

One more comment about (non)computable inputs: many practical programs
take a continuous stream of inputs from the the real world. Is this
stream computable? Maybe. But I've never been told what the program
generating it is, and so knowing that it exists is not a very useful
piece of information when I am writing a program to process this stream.

Martin