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

[matthias at ccs.neu.edu]

For the relationship to the OP, skip below the line. No need to read the whole email. 


> On May 19, 2021, at 9:52 PM, Jason Gross <jasongross9 at gmail.com> wrote:
> 
> I don't understand how this semantics works; it seems to me that it
> invalidates the normal reduction rules.



The ideas that Gabriel mentioned date back to Tim Griffin (POPL ’89) and Chet 
Murthy (Cornell dissertation, ’90). They based their work on practical operators
with reduction rules that are a tad unusual if you’re stuck in “downwards is the 
way to go” mentality (thinkingCS trees here).   

So here is an illustrative example [*]: 

    f (call/cc a)  —> call/cc (\k.k (f (a (\x.k (f x))))
	where f is a value (lambda), a arbitrary 

The call/cc operator (and equivalent) exists in a bunch of programming languages. 
Spiritually, it originated with Scheme, thought Steele and Sussman introduced `catch` 
a variant of Reynolds `escape` operator (frim around the same time). The two are 
equivalent to `catch` and syntactic sugar for `call/cc`:  escape k e == call/cc (\k.e) 

You can see that the type of call/cc is Peirce’s law. 

 - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -   - - -  

But let’s pop out a level to the original question. I’ll start with how Griffin found
this idea. In ’88, I showed him `call/cc` and its type. He exclaimed: 

	“But that this can’t compute. It’s Perice’s law.” 

Then I explained the reduction rules and, as a Constable student, he had the 
predictable reaction. So he worked it all out and submitted to POPL and 
the reaction of the French types-and-logic researchers was also predictable.
Fortunately, Murthy picked up and wrote a whole dissertation. [**]

I consider this little anecdote important. It tells us that we should NOT be 
glued to the idea that what we know about the seemingly tight connection 
between logic and computation is all there is too programming. Let people 
explore programming "in the wild" and perhaps we will find a few more such 
neat surprises and perhaps we will need to expand our understanding of logic. 


— Matthias







;; - - - 

[**] To their credit, they also worked out the relationship to the translations
Thomas sketched out in an upstream post. To find this literature, Tim Griffin 
had to get to know the Rice football stadium. 


[*] The reduction rules go back to my dissertation, though as usual, a month after
turning it in, I found vastly simpler ones. Due to the printer-queue backlog at TCS, 
the simple ones were published 4 years later. See Felleisen and Hieb TCS 91 for details.
— Yes, from then in, I presented only the “evaluation context semantics” or “reduction 
semantics”or “small step semantics” (not my name) because it was easier to understand
and use for the typical POPL attendee.