hi & a feq queries

[Donald Syme]

Hi,

This is my first message to the list so please forgive me if this 
isn't quite the right place to send these queries. (Also, is
there an archive of this list??)

I'm using Mercury as the target language for generating executable code from 
formal specifications in higher order logic.  Mercury is absolutely superb
for this task - my thanks to everyone who's worked on it for doing 
such a great job.  
 
I have a few queries.  None of these are holding up my work but
I thought I'd ask anyway.  [ I'm afraid I'm using 0.7, so these may have 
been addressed in 0.7.3.  I couldn't get 0.7.3 to compile out of the
box on my linux system, so I went with the stable 0.7... ]

  - I'm surprised Mercury doesn't seem to support data values that
    are conditionals, e.g. "if <goal> then 1 else 2".  I've had to
    create a function and apply itt o a dummy argument to get this effect,
    e.g.  apply((func(X) = Y :- if <goal> then Y = 1 else Y = 2), dummy)

    Is there an easier way of doing this?  For starters, can I say 
    something like

         (func = Y :- if <goal> then Y = 1 else Y = 2)

  - The definition of a "switch" wrt. mode analysis seems a little strict.
    For example, the natural translation of pattern matching from 
    functional languages produces switches like the following:

        Functional                           Mercury
      match x with                         (x = [], ... 
         [] -> ...                        ; x = [h], ...
       | [h] -> ...                       ; x = [h1,h2|t], ...)
       | [h1,h2 | t] -> ...

    The existence of two patterns headed by "cons" ("." in Mercury) 
    means the mode analysis doesn't believe this is a switch.
    Shouldn't Mercury look beyond the first head operator and
    detect the structural difference in the terms further down?

  - Functional programming switches with default patterns seem
    difficult to translate into Mercury, e.g.

        Functional                           Mercury
      match x with                         switch(x = [] -> ... 
         [] -> ...                              ; ??? -> ...)
       | _ -> ...                             

    I can, of course, manually put in "x = [h|t]" but
    to do this automatically requires a lot of work on my part: I
    must unwind the type-structure of "x" and work out the missing 
    constructors.  I could put in "x \= []" but then Mercury doesn't
    recognise the construct as a switch (actually I haven't tried this - I'm
    just basing things off the reference manual).

    I can see it would be fair to say "well, that's just your problem
    for trying to translate that sort of thing", but it would seem
    realistic to consider a general functional-language-style pattern
    matching construct in Mercury, in both the predicate and
    expression languages.

  - Mercury rejects the following, which is the natural translation of
    the axiom
            "both p x <=> (match p with (y,z) -> (x = y or x = z))"

    :- module junk.
    :- import_module std_util.
    :- pred both(pair(X,X) :: in, X :: out) is multi.
    both(P,X) :-  call((pred(V1 :: in) is multi :- V1 = (Y-Z), (X = Y; X = Z)),
                       P).

    on the grounds that "X" is being bound "under a negation".
    However it accepts the beta-equivalent

    both(P,X) :-  P = (Y-Z), (X = Y; X = Z).
 
    Since the predicate is applied immediately, couldn't Mercury 
    check the body in a positive logical context?  Perhaps this could
    be generalised to some kind of monotonicity analysis, or is
    this not appropriate?
    
    This is, of course, no big deal - I can treat direct application
    of lambda expressions as a special case in my code generation...
    It's just that I was surprised.


Many thanks, 
Don Syme

-----------------------------------------------------------------------------
At the lab:                                          At home:
The Computer Laboratory                              Trinity Hall
New Museums Site                                     CB2 1TJ
University of Cambridge                              Cambridge, UK
CB2 3QG, Cambridge, UK
Ph: +44 (0) 1223 334688                              Ph: +44 (0) 1223 563783
http://www.cl.cam.ac.uk/users/drs1004/
email: drs1004 at cl.cam.ac.uk
   "You've been chosen as an extra in the movie
              adaptation of the sequel to your life"  -- Pavement, Shady Lane
-----------------------------------------------------------------------------