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

[Ondrej Bojar]

Mark Brown wrote:
>>:- pred mypred(myextraarg::in)
>>     `with_type` folding_predicate(T)
>>     `with_inst` folding_predicate.
>>
>>It would be quite useful to allow the annotations in type and inst 
>>definitions, too:
>>
>>:- type extra_folding_predicate(Extra, T)
>>     == (pred(Extra) `with_type` folding_predicate(T)).
> 
> This isn't using "with type" in the same sense as above.  X `with_type` T
> means (loosely) that the type of X is T, but that doesn't hold in this case.

I'm not sure I see your point. For both cases, I think

X:   a predicate
T:   type of the predicate's arguments (i.e. higher level type of the predicate)

What is maybe confusing is the "with" in the annotation functor?

Or maybe you read the declarations this way:

 >>:- pred mypred(myextraarg::in)
 >>     `with_type` folding_predicate(T)
 >>     `with_inst` folding_predicate.

Declare a predicate mypred to have the type (myextraarg + args of 
folding_predicate(T).

While here you read:

 >>:- type extra_folding_predicate(Extra, T)
 >>     == (pred(Extra) `with_type` folding_predicate(T)).

Declare a type extra_folding_predicate(Extra, T) to be
*the type of* predicate with args (Extra+args of folding_predicate(T)).
...and you're missing the *the type of* in the formal version of the declaration.

Well, you're right that these are different, so maybe something like 
`and_append` should be used in the second case instead of `with_type`.

I don't care. I can surely live with the little inconsistency you've spotted.

O.

> 
> Cheers,
> Mark.
> 
> --------------------------------------------------------------------------
> 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
> --------------------------------------------------------------------------
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------