[TYPES] Existing Work on Function Destructors or Haskell Type Spec?

[Neel Krishnaswami]

On 19/03/18 13:52, Zachary Palmer wrote:
> 
> The first is prior work involving typed function destructors other than 
> application.  Cloud Haskell seems close, as the runtime essentially 
> allows a restricted form of transmission of lambdas over a network and 
> that requires the closures to be serialized.   I can't help but think, 
> though, that there's some core theory I'm missing on the topic.  Is 
> anyone familiar with any work of that sort?

I do not know what a "function destructor" is, but the theoretical
account of the ability to send functions over the network that is
closest to what Cloud Haskell is doing is given in Tom Murphy's
PhD thesis, "Modal Types for Mobile Code" [1].

The Static type constructor in Cloud Haskell corresponds to the
box modality in Murphy's ML5 language. One point worth noting is
that the intro/elim forms for the "static/unstatic" keywords in Cloud
Haskell dont't quite work right -- it doesn't preserve typability under
eta-expansion.

That is, if e has the type Static a, there's no way to show that e is
equal to static (unstatic e), because static (unstatic e) will not in
general be well-typed (for instance, if e is an ordinary variable).

A solution to this problem would be if CH had a let-style eliminator of
the form

     let Static x = e in e'

which takes a term e of type Static a and binds it to a variable x which
is known to be static. Then you could write the eta-expansion

     e --> let Static x = e in (static x)

which would be well-typed. The loss of eta isn't fatal, but it
hinders equational reasoning and optimization quite a bit.

Interestingly, the rule used in Cloud Haskell is actually the one that
logicians first tried when trying to give a proof theory for the box
modality, but cut-elimination didn't work properly with it. Eventually
people moved to a let-style eliminator (see Davies and Pfenning's "A
Judgemental Reconstruction of Modal Logic"), which works better.


Best,
Neel

[1] https://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-code.pdf

FYI, he and his coauthors also wrote some conference papers about this
system, but due to the page count restrictions I found them a bit
dense. His thesis is really the most readable account.