[Haskell-cafe] The Definition of Haskell
lysxia at gmail.com
Mon Dec 18 03:13:46 UTC 2017
The GHC repository includes a PDF, with its source, formalizing the Core
language (no proofs); the rules are notably written in the parseable
On 12/17/2017 02:53 PM, Todd Wilson wrote:
> On Sat, Dec 16, 2017 at 9:14 PM Brandon Allbery <allbery.b at gmail.com
> <mailto: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
> <mailto: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.
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
More information about the Haskell-Cafe