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

Mark Brown mark at csse.unimelb.edu.au
Tue Mar 6 19:21:14 AEDT 2007

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

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.


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

More information about the developers mailing list