Re: pldoc: how to specify predicates with arguments unbound.

I'm glad this conversation has come up.  Wouter and I talked about this a
couple weeks ago and it's been on my mind a lot since then.


On Tue, Sep 16, 2014 at 1:30 AM, Jan Wielemaker <[email protected]> wrote:

> At some point, I think we need a
> more advanced mode system, which I think should be:
>

I too would like a more powerful language for describing modes and
determinism.  What do we want this system to accomplish?  I have three
personal goals:

    * provide clear, concise documentation of how a predicate should be used
    * allow for runtime checks of argument instantiation and predicate
backtracking behavior
    * allow for static analysis (like check/0) to find misuses early


>   --X   X *must* be unbound on input (e.g. the stream argument of open/3).
>         Typically used for output arguments that cannot be predicted by
>         the caller and thus providing an instantiated argument will always
>         cause failure.
>    -X   X is output.  It's binding has no impact on the semantics and the
>         predicate behaves as p(NewVar), NewVar = X.  I.e., it is steadfast
>         wrt this argument.  Notably, it does *not* mean X must be unbound.
>    @X   X is examined, but not altered in any way (e.g., type checks).
>    ?X   Either -X or +X.  Can be used as a shorthand for listing 2**N
>         modes (where N is the number of ?X args).  E.g., we do not want
>         to list 8 modes for append/3.  atom_concat(?,?,?) however is
>         wrong because at least two of the arguments must be +.
>    +X   X is input.  It must have a value that is *compatible* with the
>         type.  I.e., X is a generalization of at least one instance of the
>         type.  As far as I'm concerned, this would also mean that
>         if the type is `any`, a variable satisfies.
>   ++X   X is input and bound to an instance of the type.  I.e.,
>         sort(++List, -Result) because sort cannot sort partial lists.
>

I'd like to move away from sigils (to borrow Perl's terminology) for
indicating modes.  We have a limited number of punctuation characters but
nearly limitless mode possibilities.  It's also difficult to remember the
meaning of each punctuation.  Even those who do remember the punctuation
seem to have varying interpretations of their meaning.

I suggest that we define modes similar to how we define types.  I take
error:has_type/2 as my model.  The Mercury documentation
<http://mercurylang.org/information/doc-release/mercury_ref/Insts-modes-and-mode-definitions.html#Insts-modes-and-mode-definitions>
defines a mode as "a mapping from the initial state of instantiation of the
arguments of the predicate ... to their final state of instantiation".  So
perhaps we have something like this:

:- multifile error:has_mode/3.
error:has_mode(in, before, X) :-    % like -
    nonvar(X).
error:has_mode(in, after, X) :-
    nonvar(X).
error:has_mode(out, before, X) :-    % like +
    true.
error:has_mode(out, after, X) :-
    nonvar(X).
error:has_mode(strict_out, before, X) :-     % like --
    var(X).
error:has_mode(strict_out, after, X) :-
    ground(X).
error:has_mode(mod, before, X) :-    % like :
    X = Module:Goal,
    ground(Module),
    nonvar(Goal).
error:has_mode(mod,after,X) :-
    true.
error:has_mode(strict_list,before,X) :-  % not a partial list
    is_list(X).
error:has_mode(strict_list,after,X) :-
    true.
...

This gives us human-readable names for each mode.  It also gives us a
precise definition of what each mode means.  If we forget what "out" means,
we can run listing(error:has_mode(out,_,_)) to remind ourselves.  We also
have the full power of Prolog for defining these modes.  Some data
structures, like lists or maps, have instantiation patterns that must be
defined recursively.

Perhaps we use the mode definitions like this:

%% open(in(Src), in(Mode), strict_out(Stream))
%% sort(list(List):list, out(Sorted):list)

For brevity, perhaps we make +, -, ? and : notation as aliases for in, out,
any and mod, respectively.

I think of determinism as defining the minimum and maximum number of
solutions expected on backtracking.  Fortunately the number is only 0, 1 or
many.  Because minimum must be less than or equal to maximum, we have only
6 combinations.  Those map nicely onto keywords fail, semidet, nondet, det
and multi.  We don't have a keyword for minimum=maximum=many (as in
Kuniaki's foo/2 example).


-- 
Michael
-------------- next part --------------
HTML attachment scrubbed and removed