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

On 09/16/2014 04:37 PM, Michael Hendricks wrote:
> 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]
> <mailto:[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

So far I agree, except that you leave types out of the equation.  Do
not forget the work on Ciao.  My lesson learned is that the assertion
language is too complicated and statically proving correctness isn't
feasible for large realistic programs.  They did a lot of work getting
the concepts right though.  See also Edison's work (some of which is
in the system in the Ciao dialect of the library) to base runtime
checking on a simplified version of the assertion language.

An important lesson is that we have types and terms can satisfy a
type or can be _compatible with_ a type.  The latter means that there
is a way to instantiate the term such that it satisfies the type.

>        --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'm not so sure we have that many modes. Yes, if you include types into
the mode annotation, you have. You probably also have to accept that not
all predicates can be fully described using any simple notation. The
assertion language allows specifying arbitrary pre and post conditions.
That might be nice to have, but I don't see much value for the average
Prolog programmer.

> 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)

Hmmm.  I kind of prefer open(+Src, +Mode, --Stream) and
sort(+List, -Set) or:

   open(+Src:text, +Mode:mode, --Stream:stream)
   sort(+List:list(Type), -Set:ordered_set(Type)).

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

What I like is that you can indeed define your modes. Defining modes
without types seems dubious to me. If we want to move ahead easily, I
think we should define modes as terms satisfying or being compatible
with certain types (both pre and post). Perhaps we can still leave the
type language out of the equation and just define that a type is
represented by a Prolog term.  Leaving the exact definition of types
out of the equation avoids a lot of discussion.

> 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).

I agree that Mercuries determinism system (which is what we adopted) is
satisfactory.

	Cheers --- Jan