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

[Julien Fischer]

On Tue, 6 Mar 2007, Mark Brown wrote:

> On 06-Mar-2007, Ondrej Bojar <bojar at csse.unimelb.edu.au> wrote:
>> 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).
>
> I read it as "terms of the form mypred(E), where E has type myextraarg,
> will have type 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.
>
> No, I just don't think that `with_type' means the same as `+'.
>
> I read this as:
> 	- the two sides of `==' are the same type, and
> 	- the right hand side, because of the annotation, has type
> 	  folding_predicate(T).
>
> The difference between the two declarations is that in the pred declaration,
> the thing whose type is being defined (namely, the identifier mypred) is
> _inside_ the left hand side of the with_type term, but in the type
> declaration it is _outside_ the with_type term.  That's why the same pattern
> works in the first case but not the second.
>
>>
>> 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`.
>
> 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.

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