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

[Julien Fischer]

On Wed, 7 Mar 2007, Ondrej Bojar wrote:

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

Maybe, but (having thought about it) I'm not particularly convinced by
it.

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

I find both the proposals quite ugly.

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