Monads and the meaning of imperative language – also, some musing

Monads and the meaning of imperative language — the delicious alpheccar does a lovely job of introducing denotational semantics without saying enough to scare you off, and shows how exceptions (or even assert) in imperative languages are, at bottom, the Maybe monad. This point generalises (apparently – I know enough to believe it could be true, but not enough to assert that it isn’t untrue) to “any formal description of control flow in an imperative language will be monadic in nature.” Gorgeous.

The stuff about defining domains (and that being the hard part) is resonating with me just now; I’ve spent the day nailing down definitions of sets describing a particular aspect of my pet specification language, CspCASL, and it’s not trivial. And this is the easy part: not proper “domains”, just sets without much internal structure. Markus does that, for the model semantics. Anyway, yay language design.

Formally describing languages is hard. That’s why it doesn’t happen much yet, which is one reason our current languages situation is so messy. My hand-waving prediction: it’s hard but not intractable, and we’re getting better and better at it; in time it’ll be a sufficiently managable problem, with sufficiently good tool support, that languages which aren’t formally described will stagnate in comparison to the new languages then appearing. Naturally, from where I’m standing I see the increasing convergance of computer languages (sounds like a dumbing-down term but I’m really just trying to cover both programming and specification) with full-blown mathematical logic in all its various and colourful forms. Mathematics is the language for describing things formally; a computer program is by necessity a formal description of something, therefore this convergance seems like it will be a good thing – again, from where I’m standing. Whether or not it appears that way because where I’m standing is a good place to get a view of what’s going on, or just because that’s all you can see from here, remains to be seen. ;-)

3 Responses to “Monads and the meaning of imperative language – also, some musing”

  1. January 18th, 2008 | 1:36 pm

    Exceptions in general are better captured by ErrorT than Maybe, I think. Maybe is just either “yup, this went off without a hitch” or “oops, an error occurred”.

    Incidentally, it seems that Haskell not being formally specified might be why it has seen so many useful extensions – but with its designers intending to do that, and having the denotational semantics in mind all along, the extensions that have survived are the ones that seem to have the best grounding in theory (apart from the FFI, which is just an engineering necessity).

    Of course it’s my opinion that computer science is just a branch of applied mathematics. :)

  2. January 18th, 2008 | 2:47 pm

    Applied? Surely you mean pure? ;-)

    And sure on ErrorT – but unless I’m mistaken, the post is describing Maybe?

    I spoke with Peter about the formal specification thing and he agreed. ML has a formal spec and seems to be less of a blooming ground for new stuff, but OTOH there are some cool things going on there. At AngloHaskell last year I met Dan Licata, a PhD student at CMU who was doing an internship with SPJ at MSR (TLAs FTW!), and a lot of his work is in this sphere, eg Dependent ML. Nice guy, too. http://www.cs.cmu.edu/~drl/

  3. January 20th, 2008 | 7:56 pm

    Applied in the sense that it is done with the expectation that it will have applications outside mathematics, rather than just the vague hope that it will.

    Ah yes, “Abort or Z” is like Maybe Z. This is what comes when you don’t bother to RTFA :)

    Ooh, dependent types. I’m looking forward to hacking Agda/Cayenne in the coming term. :) (I didn’t realise the former was an implementation of the latter until just now.)