Re: [isabelle] Monadic do notation for Isabelle



On Tue, 18 May 2010, Brian Huffman wrote:

On Mon, May 17, 2010 at 3:27 AM, Christian Sternagel
<christian.sternagel at uibk.ac.at> wrote:
I would like to be able to write, e.g.,

do {
 let xs = [Some 0, Some 1, None];
 x <- xs;
 y <- xs;
 let r = do {
   m <- x;
   n <- y;
   Some (x + y)
 };
 return [r]
}

which is an admittedly contrived example. My first thought, was to give "do"
an optional argument (the name of the monad that should be used), as in

do List { ... do Option { ... } ... }

I can see that your parse_translation might need to read information
from the current theory, but I don't see why it would have to *modify*
the current theory. The parse_translation for case syntax (function
case_tr in HOL/Tools/Datatype/datatype_case.ML) probably uses all the
relevant techniques that you would need to implement your generic
monadic syntax: it reads information about constructors from theory
data, and translates the case branches (built with the "_case1" and
"_case2" syntactic constructors) into the appropriate case
combinators. It does not modify any theory data during parsing.

I'm not sure how your current parse_translation is implemented, but
here's the approach I would take: First, define some syntactic
constructors for the do-syntax, similar to how the case syntax is
defined in HOL.thy:

nonterminals dobinds

syntax
 "_do1" :: "'a => dobinds" ("_")
 "_do2" :: "[pttrn, 'a, dobinds] => dobinds" ("_ <- _;/ _")
 "_do_syntax" :: "[string, dobinds] => 'a" ("do _ {_}")

Then define a parse_translation for "_do_syntax" that would parse the
list of "_do2" and "_do1" constructors, then choose an appropriate
monad instance based on the value of the string argument (obtaining
the table of monad instances from the theory data).

Alternatively you could omit the "string" argument to "_do_syntax" and
look up the monad instance based on the type of the last statement of
the do-block (except I'm not sure whether the type information would
be available yet). Or you could do a lookup based on what the
top-level constant of the last statement is, e.g. a term of the form
[_] indicates the list monad, and Some _ indicates the option monad.

This is going in the right direction.

Also note that Scala "for" comprehensions are officially explained as a certain syntax translation on untyped expressions, which are later run through the regular type-inference.

If it turns out that you do need type information for your tanslation you can organize it like that:

  * The translation functions (advanced parse translations etc.) only take
    care of producing proper binders.

  * Further transformations within the type-checking phase are done by
    your own "check" operation, which is installed via Syntax.add_term_check

The latter gives you an opportunity to participate in a simultaneous process to infer full type information. The regular Hindley-Milner type inference is only one part of that. This relatively new and advanced abstract syntax technology is still not use very much, but could open a chance to get things really right that did not work so well with plain old macros (aka translations).


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.