[Prev][Next][Index][Thread]

Semantics using ML



To: John C. Mitchell <jcm@polya.stanford.edu>
Cc: types@theory.LCS.MIT.EDU

    I am thinking about using ML in my "programming language theory"
    course next fall to teach denotational semantics. ...

    Since this is such an obvious idea, I was wondering if anyone
    had tried this before, and had any advice or software to
    "share" (as they say out here in CA).

Perhaps it's a minor point, but having taught denotational semantics
in both T (a dialect of Scheme) and Alfl (a non-strict functional language 
similar to SASL) I found the non-strict semantics of Alfl to facilitate the 
teaching, for most of the standard reasons.  For example, in denotational 
semantics we typically write things like:

  E [[e0 where x = e1]] env = E [[eo]] env'
                              where env' = env[ E[[e1]]env' / x]

Note the recursive definition of env'.  In a functional language this
would look something like:

  env' = update env "x" (E e1 env')

which in a strict language such as ML or Scheme would diverge, whereas 
in a non-strict language such as Alfl, Miranda, or Haskell would not.
Of course, one can usually get around these problems in a strict language,
but there's something to be said for using the semantic equations almost
verbatim.  Thus I would recommend using Miranda, LML, or, if implementations 
are available in time, Haskell.

  -Paul