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

[Richard Eisenberg]

I had this same query several years ago and also was surprised not to find much. Beyond the Jones paper, you may also be interested in Karl-Filip Faxén's "A static semantics for Haskell", JFP'02. You might also find use in my entry into this sparse field, in the extended version of my HS'14 paper "Promoting Type Functions to Type Families in Haskell". That paper doesn't focus on the type theory, but we needed to write down typing rules on the way to our main proof result. You can find the extended version here: https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1017&context=compsci_pubs <https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1017&context=compsci_pubs>

I hope this helps!
Richard

-=-=-=-=-=-=-=-=-=-=-
Richard A. Eisenberg, PhD
Asst. Prof. of Computer Science
Bryn Mawr College
Bryn Mawr, PA, USA
cs.brynmawr.edu/~rae <http://cs.brynmawr.edu/~rae>

> On Mar 19, 2018, at 9:52 AM, Zachary Palmer <zpalmer2 at swarthmore.edu> wrote:
> 
> 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?