[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 [email protected] (+39) 333 6757668 > On Mar 19, 2018, at 2:52 PM, Zachary Palmer <[email protected]> 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
