[m-rev.] for review: combined higher-order types and insts

[Julien Fischer]

Hi Mark,

On Sun, 31 Jan 2016, Mark Brown wrote:

> Hi,
>
> This implements the new language feature that I proposed recently
> under the heading of subtypes.
>
> Part of the change is that I've moved some code to a new module and
> also modified it. This doesn't show up in a full diff very well, so
> I've also attached the diff of just these modifications to the new
> module.

...

> Implement combined higher-order types and insts.
> 
> These allow types to be defined in the following manner:
>
>     :- type job ---> job(pred(int::out, io::di, io::uo) is det).

...

> compiler/prog_rep_tables.m:
> 	Ignore the new inst info for now.
> 
> compiler/*.m:
> 	Changes to conform to above.
> 
> doc/refernce_manual.texi:

s/refernce/reference/

> 	Document the new feature.
> 
> tests/hard_coded/functor_ho_inst.{m,exp}:
> tests/hard_coded/functor_ho_inst_2.{m,exp}:
> tests/hard_coded/functor_ho_inst_excp.{m,exp}:
> tests/hard_coded/functor_ho_inst_excp_2.{m,exp}:
> 	Test the new functionality.
> 
> tests/invalid/combined_ho_type_inst.{m,err_exp}:
> 	Test that we don't allow the new types where they are not permitted.
> 
> tests/invalid/functor_ho_inst_bad.{m,err_exp}:
> tests/invalid/functor_ho_inst_bad_2.{m,err_exp}:
> tests/invalid/functor_ho_inst_bad_3.{m,err_exp}:
> 	Test that the argument inst information is enforced as required.
> 
> tests/hard_coded/Mmakefile:
> tests/invalid/Mmakefile:
> 	Run the new test cases.

...

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 283cc4a..4cd5c1e 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi

> @@ -4554,6 +4563,24 @@ unifications; indirect attempts (via polymorphic predicates, for
>  example @samp{(list.append([], [P], [Q])} may result in an error at
>  run-time rather than at compile-time.
> 
> +Mercury also provides builtin @samp{inst} values for use with solver types:
> +
> + at example
> +any_pred is @var{Determinism}
> +any_pred(@var{Mode}) is @var{Determinism}
> +any_pred(@var{Mode1}, @var{Mode2}) is @var{Determinism}
> + at dots{}
> +any_func = @var{Mode} is @var{Determinism}
> +any_func(@var{Mode1}) = @var{Mode} is @var{Determinism}
> +any_func(@var{Mode1}, @var{Mode2}) = @var{Mode} is @var{Determinism}
> + at dots{}
> + at end example
> +
> +See @ref{Solver types} for more details.
> +
> + at node Default insts for functions
> + at subsection Default insts for functions
> +
>  In order to call a higher-order term, the compiler must know its higher-order
>  inst.  This can cause problems when higher-order terms are placed into a
>  polymorphic collection type and then extracted, since the declared mode for the
> @@ -4575,20 +4602,63 @@ but note that there is little value in doing so because there is no
>  default higher-order inst for predicates
>  therefore it will not be possible to call those terms.
> 
> -Mercury also provides builtin @samp{inst} values for use with solver types:
> + at node Combined higher-order types and insts
> + at subsection Combined higher-order types and insts
> +
> +A higher-order type may optionally specify an inst in the following manner:
>
>  @example
> -any_pred is @var{Determinism}
> -any_pred(@var{Mode}) is @var{Determinism}
> -any_pred(@var{Mode1}, @var{Mode2}) is @var{Determinism}
> +(pred) is @var{Determinism}
> +pred(@var{Type}::@var{Mode}) is @var{Determinism}
> +pred(@var{Type1}::@var{Mode1}, @var{Type2}::@var{Mode2}) is @var{Determinism}
>  @dots{}
> -any_func = @var{Mode} is @var{Determinism}
> -any_func(@var{Mode1}) = @var{Mode} is @var{Determinism}
> -any_func(@var{Mode1}, @var{Mode2}) = @var{Mode} is @var{Determinism}
> +(func) = (@var{Type}::@var{Mode}) is @var{Determinism}
> +func(@var{Type1}::@var{Mode1}) = (@var{Type}::@var{Mode}) is @var{Determinism}
> +func(@var{Type1}::@var{Mode1}, @var{Type2}::@var{Mode2}) = (@var{Type}::@var{Mode}) is @var{Determinism}
>  @dots{}
>  @end example
> 
> -See @ref{Solver types} for more details.
> +When used as argument types of functors in type declarations,
> +types of this form have two effects.
> +First, for any unification that constructs a term using such an argument,
> +there is an additional mode constraint that
> +the argument must be approximated by the inst.
> +In other words, to be mode correct a program must not construct any term
> +where a functor has an argument that does not have the declared inst,
> +if present.
> +
> +The second effect is that when a unification deconstructs a ground term
> +to extract an argument with such a declared inst,
> +the extracted argument may then be used as if it had that inst.
> +
> +For example, given this type declaration:
> +
> + at example
> +:- type job ---> job(pred(int::out, io::di, io::uo) is det).
> + at end example
> +
> +the following goal is correct:
> +
> + at example
> +:- pred run(job::in, io::di, io::uo) is det.
> +run(Job, !IO) :-
> +    Job = job(Pred),
> +    Pred(Result, !IO),          % Pred has the necessary inst
> +    write_line(Result, !IO).
> + at end example
> +
> +However, the following would be a mode error:
> +
> + at example
> +:- pred bad(job::out) is det.
> +bad(job(p)).                    % Error: p does not have required mode
> +
> +:- pred p(int::in, io::di, io::out) is det.
> + at dots{}
> + at end example
> +
> +Combined higher-order types and insts are currently only permitted
> +as direct arguments of functors in discriminated unions.

So the following would not (currently) be legal?

     :- type job(T) ---> job(T).
     :- type job == job(pred(int::out, io::di, io::uo) is det).

You also lacking (invlaid) test cases for when the arguments of combined
higher-order types and insts do not all of modes specified or when the
determinism as been omitted etc.  For example:

     :- type job ---> job(pred(int::in, io::di, io) is det).

or:

     :- type job ---> job(pred(int::in, io::di, io::uo)).


Other than that, I think the change looks ok.

Julien.