[Haskell-cafe] The Definition of Haskell

[Jonathan Paugh]

Hello,

Many parts of the language are formally specified in papers written by SPJ, or someone else who worked closely on that feature. For example, certain modifications to the type system are described here [1].

Check out SPJ's Microsoft Research page for other papers [2]. I seem to recall reading a formal definition of Haskell Core, but can't recall whether it was in one of these papers or not.

Cheers,
Jon

[1]: https://www.microsoft.com/en-us/research/publication/practical-aspects-evidence-based-compilation-system-fc/
[2]: https://www.microsoft.com/en-us/research/people/simonpj/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fpeople%2Fsimonpj%2F

On December 17, 2017 1:53:06 PM CST, Todd Wilson <twilson at csufresno.edu> wrote:
>On Sat, Dec 16, 2017 at 9:14 PM Brandon Allbery <allbery.b at gmail.com>
>wrote:
>
>> Dunno about safety results, but
>> https://www.haskell.org/onlinereport/haskell2010/ exists (next
>revision
>> expected in 2020 iirc).
>>
>
>Although this can be considered a definition of the language, it is by
>no
>means a formal definition of the static and dynamic semantics of the
>language in a form amenable to representation in systems like Coq,
>where
>metatheory might be checked.
>
>On Sat, Dec 16, 2017 at 9:22 PM Baojun Wang <wangbj at gmail.com> wrote:
>
>> SPJ may answered part of it in his talk Escape from the ivory tower:
>> https://www.youtube.com/watch?v=re96UgMk6GQ&feature=share from about
>29
>> minutes.
>>
>
>Nice talk; thanks for the reference. To summarize: formalization, which
>is
>a lot of work, leads to standardization and the reluctance to change
>the
>language, and one of Haskell's strong points is that it is constantly
>evolving.
>
>I see SPJ's point, but he makes another point in the same video, which
>is
>that Haskell has a small, internal core language to which everything
>must
>elaborate, so this would seem to make formalization even more
>attractive:
>formalize and prove safety for the core language once and for all, and
>then
>specify the elaborations and check their properties modularly, which
>should
>work well even in the face of language evolution.

-- 
Sent from my Android device with K-9 Mail. Please excuse my brevity.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171217/2bae1f7d/attachment.html>