Semantics using ML

To: types@theory.LCS.MIT.EDU
Subject: Semantics using ML
From: Mitchell Wand <wand@corwin.ccs.northeastern.edu>
Date: Mon, 26 Jun 89 20:38:46 EDT
Sender: meyer@theory.LCS.MIT.EDU
To: jcm@polya.stanford.edu
Cc: types@theory.LCS.MIT.EDU

   Date: Tue, 20 Jun 89 19:55:39 EDT
   To: types@THEORY.LCS.MIT.EDU
   Reply-To: "John C. Mitchell" <jcm@POLYA.STANFORD.EDU>
   From: "John C. Mitchell" <jcm@POLYA.STANFORD.EDU>
   Subject: Semantics using ML
   Sender: meyer@THEORY.LCS.MIT.EDU

   Date: Tue, 20 Jun 89 16:03:21 EDT

   I am thinking about using ML in my "programming language theory"
   course next fall to teach denotational semantics. Roughly, I am
   tentatively planning to have students write semantic domains as
   datatype definitions, semantic clauses as recursive functions
   (pattern matching on constructors), and provide realistic program
   syntac using the "yacc" feature. (This would follow an introduction
   to typed lambda calculus and models; I don't want to give the idea
   that denotational semantics is just a style of ML programming.)

   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).

   John


I've done something similar, using my SPS (Semantic Prototyping System)
package (written in Chez Scheme, but probably easily ported to other
dialects).  This provides typechecking for Scheme programs and Scott-Strachey
style semantic definitions.  It also includes built in LL(1) parser
generation, without using lex/yacc/etc.

My impression is that this is very useful for the students.  Among other
things, I no longer need to check whether their semantics are compositional!

Doing it in ML, as you suggested, does sound like an obvious thing to do.
There are only 2 more things to watch for (beside the obvious cart/horse bug
you mention).  First, the error messages and overall documentation, as of SML
version 0.22, were cryptic.  Second, the scanner package in 0.22 was
imperative rather than functional in style, which did not suit my purposes, so
I wrote a functional-style scanner generator for Chez SPS.  I've not looked at
the yacc package in 0.33; if it relies on yacc-style actions rather than being
functional, that might make things go less smoothly than the straightforward
correspondence you point out.

Advertisement:  SPS is described in my paper in 1984 SIGPLAN Compiler
Construction conference.  It has recently been enhanced to include on-board
scanner and parser generation (with a considerable increase in speed!), so it
is not dependent on lex/yacc.  It runs under Chez Scheme (which runs on Suns &
Vaxes), but ought to be easily portable to other dialects.  I would be happy
to send E-mail copies to whoever would like it.

--Mitch

Mitchell Wand
College of Computer Science
Northeastern University
360 Huntington Avenue #161CN
Boston, MA 02115

CSNet:  wand@corwin.ccs.northeastern.edu