formal semantics

Ramana Kumar

23 Aug 2012 23 Aug '12

12:23 p.m.

Dear Haskell Cafe I'm looking for information on past and current attempts to write semantics for Haskell. Features I'm particularly interested in are: - formal - mechanised - maintainable - up to date Of course, if nothing like that exists then partial attempts towards it could still be useful. My ultimate aims include: 1. Make it viable to define Haskell formally (i.e. so mechanised semantics can take over the normative role of the Haskell reports). 2. Write a verified (or verify an existing) Haskell compiler (where verified means semantics preserving). Cheers, Ramana

Attachments:

attachment.html (text/html — 709 bytes)

Show replies by date

Kristopher Micinski

25 Aug 25 Aug

6:48 a.m.

On Thu, Aug 23, 2012 at 12:23 PM, Ramana Kumar wrote:

...

Dear Haskell Cafe

I'm looking for information on past and current attempts to write semantics for Haskell. Features I'm particularly interested in are:

formal mechanised maintainable up to date

Of course, if nothing like that exists then partial attempts towards it could still be useful.

My ultimate aims include:

Make it viable to define Haskell formally (i.e. so mechanised semantics can take over the normative role of the Haskell reports). Write a verified (or verify an existing) Haskell compiler (where verified means semantics preserving).

Cheers, Ramana

Ramana, If you look through the Haskell reports, you'll see that the language is typically explained by its desugaring to a "core" language which has the semantics you'd "expect," in the sense that it's a call by need abstract machine implemented by means of graph reduction in form of the STG machine. Thus, you typically want to think about the semantics of "core Haskell," in which you might try understanding the semantics of the STG machine. You can certainly look at the classic article [1] that describes the behavior, at a high level. You might ask whether the high level description of the STG machine really "makes sense," at which point I'd direct you to a number of other articles (the one that sticks in my memory, but I haven't really read deeply, is [2]). It sounds, however, that you are looking for a more full description of the language's semantics in a formal manner, going from "real" Haskell to core Haskell, I feel such a reduction must surely exist but I'm not sure I can recall one. If you were to write a verified compiler, you would need a semantics for the STG machine and show that it obeyed the rules you'd expect (a call by name semantics), and then compose your proof for that with your reduction of real Haskell to core Haskell.. kris [1] "Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine," Simon L. Peyton Jones, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3729 [2] "The Spineless Tagless G-machine, naturally," Jon Mountjoy, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.8726

Gershom Bazerman

9:33 a.m.

On 8/25/12 6:48 AM, Kristopher Micinski wrote:

...

Thus, you typically want to think about the semantics of "core Haskell," in which you might try understanding the semantics of the STG machine.

Along those lines, there's Pirog and Biernacki's "A Systematic Derivation of the STG Machine Veriﬁed in Coq": http://www.cs.ox.ac.uk/files/3858/pirog-biernacki-hs10.pdf Googling for that to find the pdf also led me to this page of the Haskell Wiki, which has some good resources, but is, I'm sure, incomplete: http://www.haskell.org/haskellwiki/Language_and_library_specification Perhaps as material is assembled on the state of Haskell semantics, it can be added there as well to help others in the future. Cheers, Gershom

Kristopher Micinski

11:41 a.m.

On Sat, Aug 25, 2012 at 9:33 AM, Gershom Bazerman wrote:

...

On 8/25/12 6:48 AM, Kristopher Micinski wrote:

...
Thus, you typically want to think about the semantics of "core Haskell," in which you might try understanding the semantics of the STG machine.

Along those lines, there's Pirog and Biernacki's "A Systematic Derivation of the STG Machine Veriﬁed in Coq": http://www.cs.ox.ac.uk/files/3858/pirog-biernacki-hs10.pdf

Googling for that to find the pdf also led me to this page of the Haskell Wiki, which has some good resources, but is, I'm sure, incomplete: http://www.haskell.org/haskellwiki/Language_and_library_specification

Perhaps as material is assembled on the state of Haskell semantics, it can be added there as well to help others in the future.

Thanks for the pointers, Gershom, it seems reasonable that such a thing would exist, but I hadn't been aware of it, kris

Jay Sulzberger

2:44 p.m.

On Sat, 25 Aug 2012, Kristopher Micinski wrote:

...

On Thu, Aug 23, 2012 at 12:23 PM, Ramana Kumar wrote:

...
Dear Haskell Cafe

I'm looking for information on past and current attempts to write semantics for Haskell. Features I'm particularly interested in are:

formal mechanised maintainable up to date

Of course, if nothing like that exists then partial attempts towards it could still be useful.

My ultimate aims include:

Make it viable to define Haskell formally (i.e. so mechanised semantics can take over the normative role of the Haskell reports). Write a verified (or verify an existing) Haskell compiler (where verified means semantics preserving).

Cheers, Ramana

Ramana,

If you look through the Haskell reports, you'll see that the language is typically explained by its desugaring to a "core" language which has the semantics you'd "expect," in the sense that it's a call by need abstract machine implemented by means of graph reduction in form of the STG machine.

Thus, you typically want to think about the semantics of "core Haskell," in which you might try understanding the semantics of the STG machine.

You can certainly look at the classic article [1] that describes the behavior, at a high level. You might ask whether the high level description of the STG machine really "makes sense," at which point I'd direct you to a number of other articles (the one that sticks in my memory, but I haven't really read deeply, is [2]).

It sounds, however, that you are looking for a more full description of the language's semantics in a formal manner, going from "real" Haskell to core Haskell, I feel such a reduction must surely exist but I'm not sure I can recall one.

If you were to write a verified compiler, you would need a semantics for the STG machine and show that it obeyed the rules you'd expect (a call by name semantics), and then compose your proof for that with your reduction of real Haskell to core Haskell..

kris

[1] "Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine," Simon L. Peyton Jones, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3729 [2] "The Spineless Tagless G-machine, naturally," Jon Mountjoy, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.8726

I do not know Haskell. It looks to me as though there are several pieces of the mechanism: 1. There is, once the extensions are specified, a particular Type System, that is, a formal system with, on the syntactic side, at least, assumptions, judgements, rules of inference, terms lying in some lambda calculus, etc.. 2. The Type Inference Subsystem, which using some constraint solver calculates the type to be assigned to the value of Haskell expressions. 3. The machine which does "reduction", perhaps "execution", on the value of Haskell expressions. This is, by your account, the STG machine. There is a textual version of Haskell's Core. If it were executable and the runtime were solid and very simple and clear in its design, I think we would have something close to a "formal semantics". We'd also require that the translation to STG code be very simple. I think I have now mostly just repeated what you said. oo--JS.

Kristopher Micinski

3:17 p.m.

...

I do not know Haskell. It looks to me as though there are several pieces of the mechanism:

1. There is, once the extensions are specified, a particular Type System, that is, a formal system with, on the syntactic side, at least, assumptions, judgements, rules of inference, terms lying in some lambda calculus, etc..

That's right. Extensions get complex too, however, and can't be necessarily easily dismissed (not to imply you were doing so), RankNTypes, for example,

...

2. The Type Inference Subsystem, which using some constraint solver calculates the type to be assigned to the value of Haskell expressions.

Yes, that's right, for core haskell this is typically damas milner (let bound) polymorphism

...

3. The machine which does "reduction", perhaps "execution", on the value of Haskell expressions. This is, by your account, the STG machine.

Yes, notably graph reduction allows sharing, which is an important part of Haskell's semantics,

...

There is a textual version of Haskell's Core. If it were executable and the runtime were solid and very simple and clear in its design, I think we would have something close to a "formal semantics". We'd also require that the translation to STG code be very simple.

Yes, that's right. The translation to STG (or something like it, another core language) can be found in many books and articles, But others here have also specified some good references for executable versions of Core. Still unsure if the translation from Haskell to Core has been verified, I would suspect not, as I haven't heard of any such thing. kris

Ramana Kumar

3:33 p.m.

On Sat, Aug 25, 2012 at 8:17 PM, Kristopher Micinski

...

wrote:

...

Still unsure if the translation from Haskell to Core has been verified, I would suspect not, as I haven't heard of any such thing.

If it is only Core that has semantics, then it wouldn't make sense to verify the translation from Haskell to Core. Rather, the translation itself would be the semantics of (sugared) Haskell.

Jay Sulzberger

3:38 p.m.

On Sat, 25 Aug 2012, Kristopher Micinski wrote:

...

...
I do not know Haskell. It looks to me as though there are several pieces of the mechanism:

1. There is, once the extensions are specified, a particular Type System, that is, a formal system with, on the syntactic side, at least, assumptions, judgements, rules of inference, terms lying in some lambda calculus, etc..

That's right. Extensions get complex too, however, and can't be necessarily easily dismissed (not to imply you were doing so), RankNTypes, for example,

I suspected that some of these extensions might cause Haskell expressions to be hard to type. One thing I am not clear on is whether any standard extensions require modifications to (internal) Core.

...

...
2. The Type Inference Subsystem, which using some constraint solver calculates the type to be assigned to the value of Haskell expressions.

Yes, that's right, for core haskell this is typically damas milner (let bound) polymorphism

Ah, yes, thank you. I almost believe in Hindley-Damas-Milner but have not yet attempted the standard initiation course.

...

...
3. The machine which does "reduction", perhaps "execution", on the value of Haskell expressions. This is, by your account, the STG machine.

Yes, notably graph reduction allows sharing, which is an important part of Haskell's semantics,

Ah, thanks!

...

...
There is a textual version of Haskell's Core. If it were executable and the runtime were solid and very simple and clear in its design, I think we would have something close to a "formal semantics". We'd also require that the translation to STG code be very simple.

Yes, that's right. The translation to STG (or something like it, another core language) can be found in many books and articles,

This is good. I will look at the references given in this thread. The account at http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/T... is, I think, one part of what I was looking for.

...

But others here have also specified some good references for executable versions of Core. Still unsure if the translation from Haskell to Core has been verified, I would suspect not, as I haven't heard of any such thing.

kris

This part of the project I am less interested in, due to my fear, I am an old Lisper, that the luxuriant syntactic undergrowth might be hard to hack through. If we had an executable Core, which might have to be extended (after perhaps some subtraction) with a simple notation for type annotations, and the rest of the apparatus, I think this would be very useful. Even though we would not gain one of the claimed advantages of rigor-all-the-way, that is, better bug suppression for ordinary Haskell as she is spoke. oo--JS.

Kristopher Micinski

3:53 p.m.

On Sat, Aug 25, 2012 at 3:38 PM, Jay Sulzberger wrote:

...

This is good. I will look at the references given in this thread. The account at

http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/T...

is, I think, one part of what I was looking for.

The book I recommend (although now I feel like a bad person because I haven't read all of it :-(.., is "The Implementation of Functional Languages," http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/... I remember finding it quite approachable, although for the immediate need of trying to implement *Haskell* in a verified environment, it might not be immediately helpful, it's really good background reading on the subject that will be imperative should you want to do such things (and written around the time when Haskell was congealing, so should be representative-ish of the attitudes underlying Haskell's design at the time: graph reduction, compiling pattern matching, translating high level lamda languages to core semantics). kris

Jay Sulzberger

4:27 p.m.

On Sat, 25 Aug 2012, Kristopher Micinski wrote:

...

On Sat, Aug 25, 2012 at 3:38 PM, Jay Sulzberger wrote:

...
This is good. I will look at the references given in this thread. The account at

http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/T...

is, I think, one part of what I was looking for.

The book I recommend (although now I feel like a bad person because I haven't read all of it :-(.., is "The Implementation of Functional Languages,"

http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/...

I remember finding it quite approachable, although for the immediate need of trying to implement *Haskell* in a verified environment, it might not be immediately helpful, it's really good background reading on the subject that will be imperative should you want to do such things (and written around the time when Haskell was congealing, so should be representative-ish of the attitudes underlying Haskell's design at the time: graph reduction, compiling pattern matching, translating high level lamda languages to core semantics).

kris

I have read the book to page 12. So far I am swimming in waters known to me. I think you are right: It looks to be slow and careful, and thus just right for me. oo--JS.

Aaron Tomb

12:12 p.m.

Hi, Last summer, as part of the Summer of Code, David Lazar formalized a significant portion of Haskell 98 in the K framework. You can find the code here: https://github.com/davidlazar/haskell-semantics And there's a talk about it here: http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskel... I think David is working from essentially the same goals you have in mind. Aaron On Thu, Aug 23, 2012 at 9:23 AM, Ramana Kumar wrote:

...

Dear Haskell Cafe

I'm looking for information on past and current attempts to write semantics for Haskell. Features I'm particularly interested in are:

formal mechanised maintainable up to date

Of course, if nothing like that exists then partial attempts towards it could still be useful.

My ultimate aims include:

Make it viable to define Haskell formally (i.e. so mechanised semantics can take over the normative role of the Haskell reports). Write a verified (or verify an existing) Haskell compiler (where verified means semantics preserving).

Cheers, Ramana

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ramana Kumar

3:31 p.m.

Thanks much Kristopher, Gershom, and Aaron, for the excellent pointers. (Keep them coming, anyone else - maybe we can update the wiki..) I will look into them in more detail soon. On Sat, Aug 25, 2012 at 5:12 PM, Aaron Tomb wrote:

...

Hi,

Last summer, as part of the Summer of Code, David Lazar formalized a significant portion of Haskell 98 in the K framework. You can find the code here:

https://github.com/davidlazar/haskell-semantics

And there's a talk about it here:

http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskel...

I think David is working from essentially the same goals you have in mind.

Aaron

On Thu, Aug 23, 2012 at 9:23 AM, Ramana Kumar wrote:

...
Dear Haskell Cafe

I'm looking for information on past and current attempts to write semantics for Haskell. Features I'm particularly interested in are:

formal mechanised maintainable up to date

Of course, if nothing like that exists then partial attempts towards it could still be useful.

My ultimate aims include:

Make it viable to define Haskell formally (i.e. so mechanised semantics can take over the normative role of the Haskell reports). Write a verified (or verify an existing) Haskell compiler (where verified means semantics preserving).

Cheers, Ramana

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

4653

Age (days ago)

4655

Last active (days ago)

List overview

Download

11 comments

5 participants

participants (5)

Aaron Tomb
Gershom Bazerman
Jay Sulzberger
Kristopher Micinski
Ramana Kumar