[m-rev.] for review: Clearly explain what part of partial instantiation isn't supported.

[Julien Fischer]

On Fri, 14 Mar 2014, Paul Bone wrote:

> For review by anyone, this should be considered rather than my previous
> patch on the same topic.
>
> ---
>
> Clearly explain what part of partial instantiation isn't supported.
>
> In (at least) two places we say that partial instantiation doesn't work or
> isn't supported.  This has raised confusion so this patch attempts to
> explain what exactly is unsupported and why.
>
> doc/reference_manual.texi:
> library/list.m:
> LIMITATIONS:
>    As above.
>
> library/list.m:
>    Delete deprecated modes.
>
>    Move partial instantiation states and modes into a private interface
>    section.  Note all of the instantiation states are partial, some can be
>    safely used for subtyping so I've left those where they are.
>
> LIMITATIONS:
>    Include Zoltan's explanation of why this doesn't work for our future
>    selves and others.
> ---
> LIMITATIONS               | 26 ++++++++++++++++---
> doc/reference_manual.texi |  8 +++---
> library/list.m            | 63 +++++++++++++++++++++++++++++++----------------
> 3 files changed, 69 insertions(+), 28 deletions(-)
>

...


> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index a7a34b2..fc6bbfc 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
> @@ -2540,9 +2540,11 @@ can do so by simply defining them using a mode declaration:
> These two modes are enough for most functions and predicates.
> Nevertheless, Mercury's mode system is sufficiently
> expressive to handle more complex data-flow patterns,
> -including those involving partially instantiated data structures.
> -(The current implementation does not handle
> -partially instantiated data structures yet.)
> +including those involving partially instantiated data structures, data
> +structures with ``free'' @emph{holes} in them.

I suggest:

    i.e.@: data structures with ``free'' @emph{holes} in them.


> +(In the current implementation, partially instantiated data structures are
> +unsupported due to a lack of alias tracking in the mode system.  For more
> +information please see the @file{LIMITATIONS} file distributed with Mercury.)
>
> For example, consider an
> interface to a database that associates data with keys, and provides
> diff --git a/library/list.m b/library/list.m
> index 102edb6..91d25fc 100644
> --- a/library/list.m
> +++ b/library/list.m
> @@ -34,32 +34,23 @@
>
> %-----------------------------------------------------------------------------%
>
> -    % Some declarations for complicated modes using lists.
> -    % (Note that partial instantiation is not currently supported.)
> -
> +    % These instantiation states and modes can be used for instantiation
> +    % state subtyping.
> +    %
> +    % They could also be used for partial instantiation but partial
> +    % instantiation does not work completely.  Mercury's mode system does
> +    % not attempt to perform alias tracking.  Therefore filling in the
> +    % 'holes' of a partially instantiated data structure may not work as
> +    % expected, when this appears to work it is only by chance.  Furthermore
> +    % partial instantiations are not supported on the Erlang backend at all.
> +    % Additionally most existing code is not instantiation state polymorphic
> +    % (for example the standard library itself).
> +    %

I don't think this explanation belongs here.  (If here, why not everywhere else
we define such insts?  e.g. in the maybe module etc.)  I think the confusion
you refer to above could be resolved in this case simply by deleting the
reference to partial instantiation entirely.  (If you really want to keep it
then replace the above with pointer to the LIMITATIONS file.)

> :- inst list_skel(I) ---> [] ; [I | list_skel(I)].
> -:- inst list_skel == list_skel(free).
> :- inst list(I) == list_skel(I).
>
> :- inst non_empty_list ---> [ground | ground].
>
> -:- mode in_list_skel  == list_skel >> list_skel.
> -:- mode out_list_skel == free >> list_skel.
> -:- mode list_skel_out == list_skel >> ground.
> -
> -    % These more verbose versions are deprecated.
> -    % They exist only for backwards compatibility,
> -    % and will be removed in a future release.
> -:- mode input_list_skel  == in_list_skel.
> -:- mode output_list_skel == out_list_skel.
> -:- mode list_skel_output == list_skel_out.
> -
> -    % These modes are particularly useful for passing around lists
> -    % of higher order terms, since they have complicated insts
> -    % which are not correctly approximated by "ground".
> -:- mode list_skel_in(I)  == list_skel(I) >> list_skel(I).
> -:- mode list_skel_out(I) == free >> list_skel(I).
> -
> %-----------------------------------------------------------------------------%
>
> :- pred list.is_empty(list(T)::in) is semidet.
> @@ -3305,5 +3296,35 @@ public static List_1 det_tail(List_1 lst)
> ").
>
> %-----------------------------------------------------------------------------%
> +
> +%
> +% Private interface for definitions that are available but hidden from
> +% documentation.
> +%
> +
> +:- interface.
> +
> +    % Some declarations for complicated modes using lists.
> +    %
> +    % See our comment above regarding incomplete  support for partial
> +    % instantiation.
> +
> +:- inst list_skel == list_skel(free).
> +
> +:- mode in_list_skel  == list_skel >> list_skel.
> +:- mode out_list_skel == free >> list_skel.
> +:- mode list_skel_out == list_skel >> ground.
> +
> +    % These modes are useful for passing around lists of higher order terms,
> +    % since they have complicated insts which are not correctly approximated
> +    % by "ground".
> +    %
> +    % These could be made public (not deprecated) however I prefer to
> +    % encourage the in(list_skel(I)) and out(list_skel(I)) style syntax.
> +    %
> +:- mode list_skel_in(I)  == list_skel(I) >> list_skel(I).
> +:- mode list_skel_out(I) == free >> list_skel(I).
> +
> +%-----------------------------------------------------------------------------%
> :- end_module list.
> %-----------------------------------------------------------------------------%

Shift this hidden interface section so that it occurs just after the first `:-
implementation' declaration in the module (as with other such hidden interfaces
in the library).

Cheers,
Julien.