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

[Mark Brown]

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.

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