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.<br>
<br>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) <a href="http://syntax.wikidot.com/blog:3">blog article</a>.<br>
<br>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. :)<br>
<br>I propose any formal definition include the following warning, modeled on Knuth's warning about MetaFont:<br><br> 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.<br>
<br>Thanks,<br><br>gregg<br><br><br>[1] The Definition of Standard ML (Revised); a preview is on Google Books<br>