[m-dev.] Inductive goals

[Peter Schachte]

Since someone has opened the floodgates for discussion of syntax...

I agree 'do' is very imperative sounding, but 'ensures' doesn't quite
have the right meaning:  it sounds like it's asking for you to make the
body true, rather than check that it's true.  Unfortunately, there's no
English word I know that means 'it is the case that'.  The tradition in
logic is to use a '.' or a ':' in that context, but neither would be
good for Mercury.  My vote would be to stay with 'do'.

The keyword 'maps' seems a bit quirky.  Why not 'in'?  It reads much
more naturally.  Also, using square brackets for what must be pairs of
values in the folding syntax runs counter to the arbitrary length of
lists.  How about using braces (tuples) instead?

I really like the 'mismatch' goal.  I assume the default mismatch goal
is 'fail', but you could make it 'true' if you wanted, or an error, as
in your example, or unifications to give final values for folds.  Nice.

Your example uses "[I, I + 1] folds [0, N]", but wouldn't 'I in 0..N' do
the same thing, and read much better?

As for functionality, you've covered mapping and folding nicely, but
filtering by using an if-else is a bit clunky.  It would fit nicely with
the proposal to add one more thing you can include in the
comma-separated list of sequences:  'when Goal'.  The semantics would be
like your example:  (Goal -> Body ; Unifs) where Unifs unifies all the
folded variable pairs.

Having "do true" on the end may be reasonably common; you could make the
'do' optional, and true the default goal.

OK, last suggestion:  as an alternative for the 'folds' syntax, how
about this:

    $X from $Start to $End by $Func

which is equivalent to {$X,Func($X)} folds {$Start,$End}

The 'to' part could be optional, with "to _" being the default.  You
could also make the 'by' part optional, with "by int.plus(1)" being the
default.  Then length becomes:

    length(List, Len) :- for _ in List, _ from 1 to Len.

and take and drop become:

    take(N, List, Front) :- for _ from 1 to N, Elt from List by
list.tail, Elt in Front.
    drop(N, List, Back) :- for _ from 1 to N, _ from List to Back by
list.tail.

Unfortunately, this still doesn't make it easy to quantify over sets,
maps, etc, but I think it's still pretty useful.  Anyway, you can always
convert from sets, maps, etc to lists and then use this stuff, and
hopefully deforestation will give you the efficiency you want.


On 22/01/14 20:58, Mark Brown wrote:
> Hi Xiaofeng,
>
> On Wed, Jan 22, 2014 at 8:35 PM, Xiaofeng Yang <n.akr.akiiya at gmail.com> wrote:
>> Hi, all.
>>
>> Though I'm not a native english speaker, but I think that the keyword 'do'
>> looks so imperative. It's a good idea to use another keyword to make it look
>> more declarative, for example, like 'for ... that P(....)' .
> Good point. As English verbs go, 'do' is about as imperative as you can get.
>
> Perhaps the right word in English is 'ensure'. As in:
>
>     for X maps Xs, Y maps Ys ensure P(X, Y).
>
> Since you're mentioning the concrete syntax, is it safe for me to
> assume you agree with the semantics and abstract syntax?
>
> Cheers,
> Mark.
> _______________________________________________
> developers mailing list
> developers at lists.mercurylang.org
> http://lists.mercurylang.org/listinfo/developers
>
>

-- 
Peter Schachte               All truth goes through three stages. First
University of Melbourne      it is ridiculed. Then it is violently
schachte at unimelb.edu.au      opposed. Finally, it is accepted as
www.cs.mu.oz.au/~schachte/   self-evident. -- Schoepenhouer
Phone: +61 3 8344 1338