[m-rev.] for review: add `any_is_bound' pragma

[David Overton]

On Thu, Jul 17, 2003 at 11:39:49PM +1000, Fergus Henderson wrote:
> On 17-Jul-2003, David Overton <dmo at cs.mu.OZ.AU> wrote:
> > 
> > This change adds a new pragma `any_is_bound(t/n)' which tells the compiler
> > that for type t/n the inst `any' should be considered to be equivalent to a
> > bound inst i where i contains all the functors of the type t and each argument
> > has inst `any'.  This is required to allow us to represent HAL's `old' inst
> > using `any'.
> 
> Why not write out the `bound(...)' insts explicitly?

That's what the HAL compiler has done in the past, but it's not always
possible.  E.g. for a polymorphic predicate

	:- pred p(..., T::out(any)).

we want the `any' inst to be treated as `bound(...)' for some types and
`any' for others.

> 
> > In HAL, `old' is like `any' if the type is an instance of a
> > particular type class (`solver/1').  However, for types that are not instances
> > of `solver/1', `old' needs to be treated as though it is `bound'.
> 
> Does this mean that the mode system in HAL behaves differently depending on
> which type class instance declarations are in scope?

HAL requires the solver class instance for a type  to have the same scope
as the type: it must be defined in the same module as the type and if
the type is exported then the instance must also be exported.

> 
> > This change also provides a new Boolean option
> > `--default-any-is-bound' which, when set, assumes that `any' is
> > always equivalent to `bound', except for types t/n for which a `:-
> > pragma any_is_not_bound(t/n)' declaration exists.  We plan to use
> > this option when compiling HAL code because it allows us to use
> > existing non-solver types (e.g. types defined in the Mercury
> > standard library) without having to explicitly add a `:- pragma
> > any_is_bound' declaration for each type.
> 
> Compiler options that affect the language semantics should be avoided
> where possible.  I would rather make --default-any-is-bound be the
> default, and then there's no need for the compiler option or the
> `any_is_bound' pragma.

Okay.  That works well for us.

> As for the `any_is_not_bound' pragma, well, I don't really like the name.
> Also, I'd rather explicit syntax as part of the type declaration,
> rather than a separate pragma.  For example, perhaps something along
> the lines of `:- solver type ...' instead of `:- type ...'.

Okay, I'll do that.

An extension to this that we would like is for it to be possible to
declare an abstract type to be a solver type, but have its
implementation to be an ordinary "non-solver" discriminated union type
(or foreign type).  E.g.

	:- interface.
	:- solver type foo.

	:- implementation.
	:- type foo ---> ....

However, we probably want a special syntax for the implementation too,
e.g. something like

	:- solver_implementation type foo ---> ....

so that the compiler knows that the `solver' annotation hasn't just been
accidentally left off.

Oh, and another useful extension would be e.g.

	:- herbrand type foo ---> ....

which is equivalent to

	:- solver type foo ---> ....
	:- pragma reserve_tag(foo/0).

but perhaps I'll leave that for a later change.


David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------