[m-dev.] Fw: Re: [HAL-dev] Re: Revisiting `any' and inst casts for solver types

[Ralph Becket]

Sorry, I meant to forward this to Mercury developers.

----- Forwarded message from Ralph Becket <rafe at cs.mu.oz.au> -----

Subject: Re: [HAL-dev] Re: Revisiting `any' and inst casts for solver types
From: Ralph Becket <rafe at cs.mu.oz.au>
Date: Thu, 27 May 2004 16:38:21 +1000
To: hal-developers at bowman.csse.monash.edu.au
Reply-To: Ralph Becket <rafe at cs.mu.oz.au>
Organization: Mercury group, Melbourne University

Peter Stuckey, Wednesday, 26 May 2004:
> [...]
> 
> Now
> 
> 
> CfloatVar = pair(NNCfloat1, NNCfloat2)  
> 
> represents that semantically
> 	CfloatVar = NNCfloat1 - NNCfloat2
> 	
> Now a GROUND cfloat may not be made up of two ground nonneg_cfloats?
> 
> So I need to give a non-default definition of the ground instantiation
> 
> 
> How would that fit

With some difficulty, I think!

According to the Mercury Reference Manual,

	the mode system provides free and ground as names for
	instantiatedness trees all of whose nodes are free and bound
	respectively.

Adding `any' to the language of insts means we have to refine this
interpretation of `ground' since an `any' value is certainly bound all
the way down, but `any' is obviously not interchangable with `ground'.

In the presence of solver types, we want to interpret `ground'
semantically to mean "the set of unifying ground terms form an
equivalence class" and `any' to mean "the set of unifying ground terms
may not form an equivalence class".

Unfortunately, as your example illustrates, we can't have either of the
things I'd hoped we could have.  If we consider the deconstruction

	X = f(A1, ..., AN)

then
(1) if X has inst `ground', we can't assume A1, ..., AN each have inst
  `ground' because of cases like your example;
(2) if X has inst `any', we shouldn't assume A1, ..., AN each have inst
  `any' because (a) they might really be ground parts of the
  representation of a non-ground term, but (b) you can't pass `any'
  values where `ground' values are expected (hence we are prevented from
  using all those handy library predicates with `in' mode arguments).

So my previous suggestion doesn't work (is there any part of this
problem that has a simple and obvious answer?)


The next thing to consider is making the interpretation of `any' and
`ground' dependent upon whether the type of the variable in question is
a solver type or not.  There seem to be a number of problems here, too,
not least of them being what to do with polymorphic types.


After today's HAL meeting, the following syntax was proposed:

:- solver type t ---> ...
	where	initialisation is init_pred,
		ground         is ground_inst,
		any            is any_inst.

In the latest scheme, the programmer does not attach insts to data
constructor fields in the `...' part and the compiler does not generate
inst cast predicates.  Instead the programmer separately specifies insts
defining the meaning of `ground' and `any' for the type.

Deconstruction of an `any' inst `t' value occurs as though the value has
inst `any_inst'.

Deconstruction of a `ground' inst `t' value occurs as though the value
has inst `ground_inst'.

It is up to the solver type implementer to provide an (impure) semidet
predicate to convert an `any' value to a `ground' value (if indeed it is
semantically ground).


Pray God this is a working design at last!

-- Ralph


----- End forwarded message -----
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------