[Haskell-cafe] Formal semantics for Haskell?

[Gregg Reynolds]

ML has a formal definition[1]; why not Haskell?  Would this be a Good Thing,
or a Waste Of Time?  The Report strikes me as a hybrid of formal and
informal.  I guess that's not a problem so far, but there aren't that many
implementations; if we had dozens, how could we verify conformance?  A
formal semantics would be useful, but it would also be Fun to use Category
Theory notation in a language definition.

Such a task would be way beyond my abilities, but I have come up with an
idea for a formal semantics of IO and other non-deterministic elements of
the language that I think is kind of interesting.  It's inspired by Category
Theory and the Z specification language.   See  my (brief) blog
article<http://syntax.wikidot.com/blog:3>
.

Actually, I'm in a state of rather intense euphoria about it, so a bucket of
cold water realism over my head might be a Good Thing.  Then I could get
some sleep instead of obsessing about category theory and Haskell.  :)

I propose any formal definition include the following warning, modeled on
Knuth's warning about MetaFont:

  WARNING:  Haskell can be hazardous to your other interests.  Once you get
hooked, you will develop intense feelings about language design; semantic
models will intrude on the program texts you read.  And you will perpetually
be thinking of improvements to the programs that you see everywhere,
including those of your own design.

Thanks,

gregg


[1] The Definition of Standard ML (Revised); a preview is on Google Books
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090209/4a7a7097/attachment.htm