[Haskell-cafe] The Definition of Haskell

[Li-yao Xia]

Hi Todd,

The GHC repository includes a PDF, with its source, formalizing the Core 
language (no proofs); the rules are notably written in the parseable 
.ott format.

https://github.com/ghc/ghc/blob/master/docs/core-spec

Li-yao


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:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>