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

[Filippo Sestini]

Hello,

To address your second request, as far as I know there is no
single, comprehensive formal specification of (GHC) Haskell's
type system. In the view of some of its creators [6], one reason
is that full formalization somewhat hinders language evolution
and experimentation.

Rather, many of Haskell's constituent pieces have been
individually described over the years in the various research
papers introducing them. Examples from the type system are [1] for
GADTs, and [2] for closed type families.

Moreover, the GHC implementation of Haskell is based on a core
intermediate language, also known as GHC Core or System FC, to
which the entire language must elaborate. System FC and its
subsequent extensions have been formally specified [3, 4, 5]. In a
sense, a definition of Haskell's type system can be (partially)
inferred from the way it desugars to System FC.

[1] Vytiniotis, Weirich, Peyton Jones, Simple unification-based type inference for GADTs, 2006
[2] Eisenberg, Vytiniotis, Peyton Jones, Weirich, Closed Type Families with Overlapping Equations, 2014
[3] https://github.com/ghc/ghc/tree/master/docs/core-spec
[4] Sulzmann, Chakravarty, Peyton Jones, Donnelly, System F with type equality coercions, 2007
[5] Weirich, Hsu, Eisenberg, System FC with Explicit Kind Equality, 2013
[6] Hudak, Hughes, Peyton Jones, Wadler, A History of Haskell, 2007

Regards

-- 
Filippo Sestini
sestini.filippo at gmail.com
(+39) 333 6757668

> On Mar 19, 2018, at 2:52 PM, Zachary Palmer <zpalmer2 at swarthmore.edu> wrote:
> 
> [ 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