Re: [TYPES] Existing Work on Function Destructors or Haskell Type Spec?
Richard Eisenberg <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] 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 <[email protected]> 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?