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

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

Hi, all!  I have a couple things I've been trying to find to no avail 
for a while, so I thought I'd ask the help of the list.

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?

Second, I've also had little luck finding a formal type specification 
for Haskell.  The 1999 workshop paper "Typing Haskell in Haskell" by 
Mark Jones seems to be the closest thing I could find with search 
engines, and that's basically a Literate Haskell file. Does anyone know 
of an inference rule-style type system specification for the language?

Thanks for your time!

Best,

Zach