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

[Fergus Henderson]

On 23-Jan-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> (1) Solver types in Mercury
> 
> Solver types are provided to support the implementation of constrained
> types such as constrained integers, partial orders and so forth.
> Implementation of solver types inevitably involves some impure coding
> behind the scenes to implement constraint stores and the like.

I don't agree that solver implemenations must inevitably involve impure coding.
But this is not important for your proposal.

> The syntax for solver type definitions will be as follows:
> 
> :- solver type <typename>
> 	where initialisation is <initpred>, unification is <unifypred>.
> 
> Calls to <initpred> are inserted during mode analysis to convert
> variables free >> any where necessary.
> 
> Calls to <unifypred> are used to unify variables of the solver type (the
> only mode is <unifypred>(in(any), in(any)) is semidet.)
> 
> Any view of values of the solver type must be provided by predicates in
> the solver type's defining module.

Sounds fine.

> TODO:
> - Support the new syntax.
> - Record the <initpred> and <unifypred> info somewhere in the HLDS.
> - Get mode analysis to schedule calls to <initpred> and <unifypred>.
> - I think that's it.

At some point the compiler needs to check that <initpred> and <unifypred> have the
right type, mode, and determinism.

> (2) Herbrand types in Mercury
> 
> Herbrand types are a special kind of solver type supporting Prolog
> style unification.
> 
> The syntax for Herbrand type definitions will be as follows:
> 
> :- herbrand type <typename> ---> <du constructors>.

I think it would be nice if we could come up with a less jargonish term
than "Herbrand".

> Scheduling of the Herbrand unification X = f(Y, ...) (for some data
> constructor f) works as follows:
> 
> inst(X) | inst(Y, ...) | scheduled goals
> --------+--------------+----------------
> free    | some or all  | init_Herbrand(V), ...,   [for each free V in Y, ...]
>         | free         | construct X = f(Y, ...)
> --------+--------------+----------------
> any     | some or all  | init_Herbrand(V), ...,   [for each free V in Y, ...]
>         | free         | construct Z = f(Y, ...)  [for some new variable Z  ]
>         |              | unify(X, Z)

This will lead to poor performance.  In the case of X = f(Y, ...) where
X has static inst "any", but is bound at run-time, we should not need
to allocate any heap space.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------