[m-dev.] Thinking about a "Mercury Report" type document.

[Ralph Becket]

Fergus Henderson, Thursday,  8 November 2001:
> Could you be more specific about how this would differ from the Mercury
> language reference manual?

What I have in mind is something containing rather more formalism
than the reference manual, which is excellent as a programmers'
reference, but perhaps less so for a compiler writer.

For example, the new document would specify the type system in
traditional sequent calculus terms.

> The language reference manual is a fair bit bigger than 10-20 pages,
> of course ;-)

Okay, I admit that I'm perhaps being extraordinarily optimistic on
that point!  That said, the reference manual is almost entirely prose.
It would be nice for us to be able to point to a couple of pages and
say "there is the core of the Mercury type system" or "there is the
core of the mode system"; explanatory glosses would take up considerably
more space, of course.

> > The document would need at least the following:
> > 
> > A definition of the "core" mercury syntax (omitting sugar,
> > name munging, foreign language interface etc.)
> > 
> > A definition of the type system (it would be nice to include
> > type classes, but v1.0 of the document could probably omit them.)
> > 
> > A formal description of type inference for Mercury.
> 
> Well, that's enough for at least one paper, if not more -- indeed it
> is probably enough for a PhD thesis (David Jeffery's), although I guess
> we'll have to wait for the examiner's reports to be sure! ;-)

By way of not reinventing wheels, I was hoping much of it could be
culled almost directly from such documents :)

> > A definition of the inst and mode systems.
> > 
> > A formal description of mode inference for Mercury.
> 
> That's probably at least as big a job as the formal
> description of the type system.

I'm not talking about writing whole dissertations here.  This thing
should assume that the reader has at least had a course on compiler
construction, knows the lambda and predicate calculi, has a passing
familiarity with Hindley-Milner/Mycroft-O'Keefe type systems, done
a course on operational semantics etc.  It's job would not be to
explain or discuss design decisions or present clarifying examples.

> > An operational semantics for SHNF.
> 
> That one is about the right amount for a paper.  I did a bit of work
> on this with Andy Moran, working on defining a "small-step" formal
> operational semantics, but unfortunately other things intervened
> and the details got paged out of my cerebral cache...
> 
> I certainly think it would be a good idea to have more formal descriptions
> of all of these things.  But let's pick them off one at a time.

Agreed!

- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------