[m-dev.] feature request: allow `with_type` and `with_inst` in type and inst definitions

[Ondrej Bojar]

Julien Fischer wrote:
>> Something like this would make more sense:
>>
>> :- type extra_folding_predicate(Extra, T) `apply` Extra
>>     == folding_predicate(T).
>>
>> That is, a term of type extra_folding_predicate(Extra, T) that has an
>> argument of type Extra will have type folding_predicate(T).  We would
>> require that all type variables to the right of `apply` also appear to
>> the left of it.
>>
>> I wouldn't have any objection to allowing type declarations of this form.
> 
> I can't see this sort of thing actually ever being that useful.

The motivation remains the same as for my original notation proposal:

Say there is a standard library that defines:

:- type comparison_pred(T) == pred(T, T, comparison_result).

And say there is a different library that makes use of it:

:- pred array__bsearch(array(T), T, comparison_pred(T), maybe(int)).

And finally, say the user wants to implement a bunch of such comparison 
predicates, that all need an extra argument (or worse, a couple of extra arguments).

:- pred my_comparator_one(extra1, extra2) `with_type` comparison_pred(X).
:- pred my_comparator_two(extra1, extra2) `with_type` comparison_pred(X).

"Wouldn't it be nice if" ;-) the user could declare the type of his preditaces?

% my notation:
:- type my_comparison_pred(T)
      == pred(extra1, extra2) `with_type` comparison_pred(T).

% Mark Brown's suggestion, if I am able to write is correctly:
:- type my_comparison_pred(T)
     `apply` (extra1, extra2) == comparison_pred(T).

O.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------