Re: [TYPES] Why are ACM conference registrations so expensive now?

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Adam,

I don't think there is any easy way to avoid the complexity of online 
presentations. Our conferences are usually in America or Europe, and it 
can be very difficult to get visas in a timely way for people from 
countries like Brazil or India. So if we want them to be able to both 
present and answer audience questions, then we need some kind of live 
connection.


Best,
Neel

On 14/12/2023 15:39, Adam Chlipala wrote:
[ The Types Forum, 
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


On 12/14/23 6:52 AM, Gabriel Scherer wrote:
1. Ensure that an online attendance option remains available in the 
future

for cheap. ICFP'23 had free online attendance through Youtube, will this
option remain available in the future? Will it possible to follow the
POPL'24 talks remotely for free and ask questions? Will speakers be 
allowed

to talk remotely if necessary, at no cost?
   (This is important for our colleagues that cannot afford the plane 
in the

first place, and for people who wish to reduce travel.)


I don't know if I'm the odd one out, but I just want to add a 
dissenting voice here: I think it's far from clear that "online 
attendance" is valuable enough to justify the cost of complex 
technical flows.  I'm used to telling my students that the point of 
the conference is the hallway track, not watching talks.  I'd suggest 
to people who can't make the conference to read papers (or prefixes 
thereof) instead of watching videos.  Videos produced by authors on 
their own time could also work a lot better than conflating the 
physical conference with the opportunity to record videos.


In other words, suggesting that people watch more online videos, in a 
world where online videos are already providing so much distraction 
from "real work" or just going for a walk outside, may make a net 
negative impact on the world, at the same as our conferences are 
applying significant financial cost and volunteer effort to provide 
what may actually be a net negative.  The cost-benefit analysis could 
work out if we really fine-tune the technical flow and don't spend 
(almost?) hours per conference delaying sessions to fix AV issues, but 
at least until we get there

[TYPES] Why are ACM conference registrations so expensive now?

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi,

I just registered for POPL, and the total cost was over 2000 USD. This 
seems really high, and it seems something that has gotten a lot worse 
over the last year or two. For example, ICFP a few months ago was 1500 
USD, and POPL last year was 1375 USD.


Does anyone know what factors have been driving up the cost of our 
conferences up so quickly? I'm worried we're making our events 
inaccessible to anyone but the best-funded researchers and institutions.


Best,
Neel

[TYPES] Semantics of modes in logic programming?

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

I'm interested in the semantics of mode systems in logic programming, 
especially (a) mode systems more sophisticated than simple input or 
output modes, and (b) denotational semantics of logic programs with modes.


Uday Reddy's 1992 paper "A typed foundation for directional logic 
programming" (https://urldefense.com/v3/__https://www.cs.bham.ac.uk/*udr/papers/directional.pdf__;fg!!IBzWLUs!RIsOJV9x2aZaYUcdxebrICDz_vREN4r14OX46bY1vpRhC6gHz6PZnsDR9JcDg9vQSGbGNvsoOfl3Kks_ocdKMUcJyqKwVlveYJZj8Q$ ) 
gives a beautiful mode system based on classical linear logic, and he 
shows it has a lot of really great operational properties.


I'd be especially interested in a denotational (especially categorical) 
semantics for this language, but want to cast the net broadly in this 
question.


Thanks!

Best,
Neel

[TYPES] ETAPS bars Russian researchers from attending

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

The ETAPS website (https://urldefense.com/v3/__https://www.etaps.org__;!!IBzWLUs!HUevd2N5Ms-2WYC1sMdH93ef4xxRy4BjZ9KD0I8SPwLGGpv-Rk7u_Emgl9qMMyLGK4ex90o0Cm0$ ) has the following text on its 
front page:


The ETAPS association strongly condemns the war against Ukraine 
launched by President Putin. It is an intolerable breach of 
international law and a crime against humanity, unfolding in Europe 
now. Therefore, until further notice, ETAPS 2022 cannot accept 
registrations from affiliates of Russian research institutions or 
companies.


While I'm as opposed to illegal wars of aggression as anyone else, this 
feels like a serious mistake.


There are many Russians (such as Jetbrains corporation) who have taken 
the serious personal risk of publically opposing the war, and barring 
them from our conferences due to their nationality feels wrong to me.


It may well be that the financial sanctions regime means that 
registration payments cannot be accepted, but that is quite different 
from barring them personally.


What do the rest of you think?

Best,
Neel

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

[Neel Krishnaswami]

ourse, what we don't get that we might expect is a canonicity property: we
now have "fake" proofs of (A \/ B) that cannot be distinguished from "real"
proofs by normalization alone, you have to interact with them to see where
they take you. (Or, if you see those classical programs through a
double-negation translation, they aren't really at type (A \/ B), but
rather at its double-negation translation, which has weirder normal forms.)




On Wed, May 19, 2021 at 5:07 PM Jason Gross  wrote:


[ The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Non-truncated Excluded Middle (that is, the version that returns an
informative disjunction) cannot have a computational interpretation in
Turing machines, for it would allow you to decide the halting problem.
More generally, some computational complexity theory is done with
reference
to oracles for known-undecidable problems.  Additionally, I'd be
suspicious
of a computational interpretation of the consistency of ZFC or PA 
would having a computational interpretation of these mean having a type
theory that believes that there are ground terms of type False in the
presence of a contradiction in ZFC?

On Wed, May 19, 2021, 07:38 Talia Ringer 
wrote:


[ The Types Forum,

http://lists.seas.upenn.edu/mailman/listinfo/types-list

]

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.krishnasw...@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 mi

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

[Neel Krishnaswami]

[ 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 
<mailto:neelakantan.krishnasw...@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

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

[Neel Krishnaswami]

[ 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 

Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Jeremy,

One approach to closure conversion which I like very much is
the observation that when you defunctionalize a normalization-
by-evaluation algorithm, you get a translation into an explicit closure
representation.

I learned this from Chapter 3 of Andreas Abel's habilitation thesis [1],
where he abstracts NbE from domains to partial applicative structures,
and then shows that a closure calculus forms a partial applicative
structure.

This might be too operational for you, but since the line between
operational and denotational approaches can get pretty blurry, perhaps
it is of interest.

[1] 

Best,
Neel

On 01/10/18 20:14, Jeremy Siek wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I’m interested in finding literature on proofs of correctness of closure 
conversion
applied to the untyped lambda calculus with respect to a denotational semantics.
(Bonus for mechanized proofs.)

I’ve found papers that are a near miss for what I’m looking for, such as:
* closure conversion proofs for the STLC (Chlipala PLDI 2007)
* closure conversion proofs based on operational semantics
(Minamide, Morrisett, and Harper POPL 1996, and many more)
* correctness proofs using denotational semantics for compilers that
don’t do closure conversion, but instead compile to a machine that
supports closure creation (the VLISP project and many more).

Thanks in advance for pointers!

Best regards,
Jeremy

Re: [TYPES] System F and System T names

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

1. In "The system F of variable types, fifteen years later", Girard
remarks  that there was no particular reason for the name F:

   However, in [3] it was shown that the obvious rules of conversion for
   this system, called F by chance, were converging.

There may be another explanation in his thesis, but I haven't read it
since unfortunately I am not fluent in French.

2. However, since I am semiliterate in German, I did take a look at
Gödel's paper "Über eine noch nicht benüzte Erweiterung des finiten
Standpunktes", where System T (and the Dialectia interpretation for it)
was introduced. He names this system in a parenthetical aside:

  Das heisst die Axiome dieses Systems (es werde T genannt) sind formal
  fast dieselben wie die der primitiv rekursiven Zahlentheorie [...][1]

However, the previous page and a half were spent talking about the type
structure of system T, so it is reasonable to guess that T stands for
"types". But, no explicit reason is given in print.

Best,
Neel


[1] "This means the axioms of this system (dubbed T) are nearly
the same as those of primitive recursive number theory [...]"

On 06/04/18 12:07, Alejandro Díaz-Caro wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Type-theorists,

Does anyone know where do the names System "F" and System "T" comes from? I
am not asking who introduced those names (Girard System F, and Gödel System
T), but what the "F" and the "T" means.

Kind regards,
Alejandro

Re: [TYPES] What algebra am I thinking of?

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Phil,

I learned about this from Martin Escardo, and he told me the observation
about monoidal closure is in Lawvere's paper "Metric Spaces, Generalized
Logic, and Closed Categories".

One further observation I have not seen written down anywhere is that
the natural numbers also support a trace (ie, feedback) operator, since
it is also the case that x + y ≥ z + y if and only if x ≥ z.

This means that the Geometry of Interaction construction can be applied
to the natural numbers, which yields a preorder of pairs of natural
numbers (n,m). In this case, two objects have a map between them if
one object is greater than the other, viewing each object (n, m) as the
signed integer n - m.

As a result, I've sometimes wondered if the Int construction got its
name as a bit of a joke!

Best,
Neel


On 27/03/18 21:02, Philip Wadler wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]



Thanks to all for further replies, and especially to Neel for his
observation about monus and monoidal closure. Neel, is this written down
anywhere? Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 27 March 2018 at 13:39, Neel Krishnaswami <nk...@cl.cam.ac.uk> wrote:


On 27/03/18 15:27, Philip Wadler wrote:

Thank you for all the replies, and for reminding me of bags,

rigs/semirings, and modules.

In a rig, what corresponds to the notion of monus?
_∸_ : ℕ → ℕ → ℕ
m  ∸ zero  =  m
zero  ∸ (suc n)  =  zero
(suc m) ∸ (suc n)  =  m ∸ n
Is monus defined for every rig? (While zero and suc are defined in every
rig, it's not immediately obvious to me that definition by pattern
matching
as above makes sense in an arbitrary rig.) What are the algebraic
properties of monus?



The natural numbers Nat, ordered by , form a posetal symmetric
monoidal closed category. Here, the objects are the natural
numbers, and Hom(n, m) = { ∗ | n ≥ m }

The tensor product is given by:

   x ⊗ y ≜ x + y

The monoidal closed structure arises from saturating subtraction:

   y ⊸ z ≜ z - y

It's easy to show that Hom(x ⊗ y, z) = Hom(x, y ⊸ z) since
x + y ≥ z if and only if x ≥ z - y.

(This is all given in Lawvere's paper "Metric Spaces, Generalized
Logic, and Closed Categories".)

So it seems like the natural thing to do would be to say that a rig
has a monus when it is monoidal closed with respect to its addition,
defining x ≥ z to hold when there exists a y such that x = y + z.

Best,
Neel



--
Neel Krishnaswami
nk...@cl.cam.ac.uk




The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Re: [TYPES] What algebra am I thinking of?

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On 27/03/18 15:27, Philip Wadler wrote:


Thank you for all the replies, and for reminding me of bags,
rigs/semirings, and modules.

In a rig, what corresponds to the notion of monus?
   _∸_ : ℕ → ℕ → ℕ
   m  ∸ zero  =  m
   zero  ∸ (suc n)  =  zero
   (suc m) ∸ (suc n)  =  m ∸ n
Is monus defined for every rig? (While zero and suc are defined in every
rig, it's not immediately obvious to me that definition by pattern matching
as above makes sense in an arbitrary rig.) What are the algebraic
properties of monus?


The natural numbers Nat, ordered by , form a posetal symmetric
monoidal closed category. Here, the objects are the natural
numbers, and Hom(n, m) = { ∗ | n ≥ m }

The tensor product is given by:

  x ⊗ y ≜ x + y

The monoidal closed structure arises from saturating subtraction:

  y ⊸ z ≜ z - x

It's easy to show that Hom(x ⊗ y, z) = Hom(x, y ⊸ z) since
x + y ≥ z if and only if x ≥ z - y.

(This is all given in Lawvere's paper "Metric Spaces, Generalized
Logic, and Closed Categories".)

So it seems like the natural thing to do would be to say that a rig
has a monus when it is monoidal closed with respect to its addition,
defining x ≥ z to hold when there exists a y such that x = y + z.

Best,
Neel



--
Neel Krishnaswami
nk...@cl.cam.ac.uk

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

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.