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

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

> Do not forget the work on Ciao.  My lesson learned is that the assertion
> language is too complicated
>

Yes, they've done some great work.  Unfortunately, as I understand it, they
confound modes and types.  I believe those two are orthogonal and should
kept independent.

I agree that Ciao's approach is too complicated.


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


As an aside, I think I've failed to see how compatibility with a type is
useful as a mode.  Maybe some examples will help me see what I'm missing.
 Using your notation, we have four possibilities for an input argument:

  +X
  ++X
  +X:type
  ++X:type

The first two are equivalent since all values are compatible with the
implicit "any" type.  They both allow variables, as you mentioned.  Of
course, since they both allow variables, one could have written any of: X,
+X, ++X, -X.  So a user gets no benefit from mode annotation without a type.

+X:type also accepts a variable since a free variable is a generalization
of all types.   That leads me to see no distinction between: X:type,
+X:type and -X:type.

++X:type does not allow a free variable so there's no overlap with other
mode annotations.  Since this is the only mode annotation that's distinct
from the others, why don't we call it + instead?

Maybe +X:type implicitly requires nonvar(X)?


> I'm not so sure we have that many modes. Yes, if you include types into
> the mode annotation, you have.


Maybe we don't have as many modes as I think, but defining them as I
described gives us space to learn that as we go.

My sloppy "list" mode was a bad example because it blurs the distinction
between modes and types.  I intended that mode to describe the
instantiation pattern where free variable are prohibited the end of a term
chain.  It may be better defined like:

is_proper(X) :-
    var(X),
    !,
    fail.
is_proper(X) :-
    atomic(X).
is_proper(X) :-
    X =.. [_,_,T],
    is_proper(T).



> You probably also have to accept that not
> all predicates can be fully described using any simple notation.


I agree.  If we try to cover all possible predicates, our notation becomes
far too complex.


> 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 mostly agree.  The average Prolog programmer doesn't define new clauses
for error:has_type/2 either.  She uses the ones defined in the library or
uses sugar like library(typedef) to handle the details.

However, by having well-defined pre- and post-conditions, the average
programmer does get runtime mode checking (a simple addition to
library(mavis)).  That seems valuable.



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

Sure.  That's just a disagreement on whether we spell the mode "in" or "+"
:-)

Defining modes without types seems dubious to me.


I'm surprised to hear that.  I think the SWI-Prolog documentation does a
great job of using modes without types where the types would be too
complicated.  format(+Format,:Args) and with_output_to(+Output,:Goal) come
to mind.

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