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

Il 16/09/2014 16:37, Michael Hendricks ha scritto:
> 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

I think it is called 'failure' in swi prolog modes.

> and multi.  We don't have a keyword for minimum=maximum=many (as in
> Kuniaki's foo/2 example).

Please don't forget the need to specify the determinism info for
meta_predicate arguments. In our code we use something like that:

:- meta_pred(first_match(nondet(0), det(0))).

This would be fundamental for our big shared dream to have a static mode
checker for prolog code. In our experience our first enemies are
unexpected failures and unexpected nondets.

This is so true that if I could write Prolog code prefixing goal that
might fail or that might generate multiple solutions with some prefix
and after that I'll get a crash where a non prefixed goal fails or leave
a choice point I would be more than happy to manually add the missing
prefixes to all our code (this would help also the readability of the
clauses and the involved algorithms).

Of course the reverse (i.e. add a det/1 wrapper to all other goals), is
too heavy (also with term_expansion/2 due to runtime penalties).


-- 
Abramo Bagnara