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

[Maria Garcia de la Banda]

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

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)

I am sure there are more subtleties but I cannot remember them right now.

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

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.

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

Cheers,

Maria

   



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