[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