[m-dev.] Re: [HAL-dev] Adding Herbrand types to Mercury

[Ralph Becket]

Maria Garcia de la Banda, Wednesday, 28 January 2004:
> 
> > The syntax for solver type definitions will be as follows:
> >
> > :- A solver type <typename>
> > 	where initialisation is <initpred>, unification is <unifypred>.
> 
> I quite like making explicit in the type definition the fact that
> <typename> is a solver type. However, I am not that sure about using
> the "where ..." instead of type classes. Recall that in HAL a type is
> a solver type if it is an instance of the typeclass solver(T)  which
> has the init(TT:(new -> old)) is det method and inherits the T::(old
> -> old) = T::(old -> old) is semidet method from the eq/1 class.

I think in the long run making it a type class thing might well be more
elegant.  Just for the first cut, however, it seems simpler to do it
this way and treat solver types as something special (which they are!)

> I am not sure how the initpred would work. I mean, can one simply use
> init/1 in a literal and then trust the compiler to substitute the call
> to the appropriate initpred? What would happen for types which do not
> have an initpred (run-time error?)

The compiler will insert calls to <initpred> wherever a solver type
variable with inst free (new in HAL) is required to have inst any (old
in HAL).  There's nothing to stop the user from calling <initpred>
explicitly, but I can't offhand think why the user would do such a
thing.  Only solver types have <initpred>s and each solver type has its
own <initpred>; different types' <initpred>s will have different (fully
qualified) names, so there shouldn't be any ambiguity.

> This makes things quite different (some simpler some not):
> 
>  * checking that initpred and unifypred have the proper type,mode,det,
>    etc is as usual for methods.
>  * recording the initpred and unifypred is easy since it is again done
>    through the usual type class.
>  * higher order types (or those which include higher order as arguments)
>    cannot be instances of the eq/1 class (and therefore cannot be of
>    solver/1 either)
>  * predicates that use the init/1 and (the particular mode of) =/2
>    will have a solver(T) or eq(T) constraint in their type.
>  * since the need for init(T) and (the particular mode of) =/2 is only
>    detected during mode analysis, a new phase after mode analysis is
>    needed to infer class constraints.
>  * solver types cannot be renamings (need to be instances of a type class)

So in the proposed scheme for Mercury the roughly analagous points are

* the <initpred>s and <unifypred>s are noted specially rather like types
  that have their own equality and/or comparison predicates;

* conceivably (partly) higher order types could be given an equality
  relation since the user defines what equality is;

* since calls to <initpred> and <unifypred> are inserted automatically,
  the programmer doesn't need to specify any type class constraints on
  predicate signatures where solver types are concerned - type inference,
  I think, works as normal;

* equivalence types can be solver types, but not the other way round (at
  least, an equivalence would have to be handled by the solver type
  implementer using forwarding predicates etc.)

> > RathAer than make a special case of having an "internal" view of the
> > solver type (e.g. an int or a c_pointer or whatever) vs an "external"
> > view (i.e. the solver type itself), solver type implementors will have
> > to define their own conversion functions, e.g.
> > 
> > :- func convert(<internaltype>) = <solvertype>.
> > :- mode convert(out)            = in(any)  is det.
> > :- mode convert(in)             = out(any) is det.
> 
> Not sure what you mean here. I mean, are we considering two different types?
> Because HAL assumes both types are the same, however, they are treated
> differently depending whether the compiler is inside/outside the module that
> defines it.

The idea is that the compiler just assumes that any solver type is
implemented as a foreign type.  It may be the case that it is
implemented as an ordinary Mercury type, but that aspect has to be
handled via an explicit cast function as above, which the programmer
puts in her code at places where "conversion" between the solver type
and the actual representation type is required.  This means that the
compiler doesn't have to treat types differently depending upon which
part of the program it's compiling.  It may well turn out to be a better
idea to do things the HAL way, but that's on my "things to improve"
list!

> As a result:
> 
>  * the convertion only affects the mode
>  * the mode of a solver type within the defining module is always assumed to
>    be bound to one of its outmost functors, but it might not be ground. For
>    example, consider a solver which combines other two solvers with type
>                    f(solvertype1,solvertype2)
>    Whithin the defining module, variables with that type should be bound to 
> f/2,
>    but might actually be f(any,any), and thus non-ground.

I was thinking that solver types would be handled entirely through
combinators rather than data constructors.  This simplifies the compiler
at the cost of making the solver writer do a little extra work.  But
since solvers are only going to be written infrequently, and by experts,
this doesn't seem too bad.

>  * Within the defining module, the solver type is not considered to be
>    initable (since it is assumed to be bound).
>  * Within the defining module the instance of the solver/1 method =/2
>    is not used unless explicitely indicated by the user (since the mode
>    will be such that the usual bound = bound is semidet automatically
>    generated by HAL must be used instead.

These special cases don't arise in my outline, which is a plus.

> I think this needs a bot more of thinking-discussion because I bet I am
> forgetting things.
> 
> Other question regarding solver types:
> 
>   * What about delay? I think our odifications have been mostly
>     integrated into Mercury already, but things like type classes and
>     user syntax must be handled.

I haven't considered the whole delay thing in any depth.  That's pretty
high on my list of considerations, however.

I'm not sure what you mean by user syntax.

> Ooops, Alejandro is up, got to go, we should discuss all this tomorrow at the
> HAL meeting in detail.

Righto!  I hope A feels better soon,

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------