[m-dev.] A change for varset and term

[Fergus Henderson]

On 20-Oct-1998, Thomas Charles CONWAY <conway at cs.mu.OZ.AU> wrote:
> 
> After just talking with Renaud, the following idea occured to me.
> What do people think?
> 
> In the library we have the types `var' and `varset'. Although they're
> the one type, we use them to represent a number of things including
> program variables, type variables and size variables (in termination
> analysis). The use of `var' and `varset' are prone to two kinds of
> bug: mixing vars that represent two different kinds of thing (eg
> program vars and type vars) and mixing vars from two different varsets.
> The following proposal would fix the first problem and has a trivial
> extension which would fix the second.
> 
> Instead of
> 
> 	:- type varset.
> 	:- type var.
> 
> 	:- pred new_varset(varset).
> 	:- mode new_varset(out) is det.
> 	...
> 
> we have
> 
> 	:- type varset(T).
> 	:- type var(T).
> 
> 	:- pred new_varset(T, varset(T)).
> 	:- mode new_varset(in, out) is det.
> 	...

I think this is a good idea, so long as you preserve
backwards compatibility using some type synonyms:

	:- type varset == varset(unit).
	:- type var == var(unit).

> Now in varset.m, we make the concrete representation of var(T) be:
> 	
> 	:- type var(T)	--->	var(int). % Remember, we can't use an
> 					  % equivalence here for impl.
> 					  % reasons!
> 
> This has the same runtime representation as the original `var', but
> is more typesafe.

I should point out that there will actually be an efficiency cost
from this, with the current implementation, because of the extra
type_info arguments.  But the cost is extremely small, and so I think
the extra type-safety is worthwhile.

> The extension is to make the representation of varset include the given `T',
> and for `var(T)'s to include it too:
> 
> 	:- type var(T)	--->	var(int, T).
> 
> (The ordering of the arguments is very deliberate here - the comparison
> of the variable numbers will usually fail more quickly than the relatively
> expensive polymorphic unification for the second argument). This has a
> time and space cost but is certainly useful for debugging if for example
> we changed prog_var:
> 
> 	:- type prog_var_type	--->	prog_var(pred_proc_id).
> 	:- type prog_var	==	var(prog_var_type).
> 
> Now, if we try to unify two variables from different varsets the
> unification can fail, or even call error (if, for example we use
> user defined equality, or explicit calls to unify_var in term.m, etc).

This would be useful, but it's more expensive, and also requires
more changes.

> Given that we really only need to change 1 line (the defn of var(T))
> to switch between the two,

No, you also need to change the defn of varset(T), and also
you need to change varset__init so that it takes a parameter of
type `T' which you can store in the varset and use to initialize
the `T' in the var at every call to varset__new_var.
And you then also need to change every call to varset__init
to pass a value of type `T'.  So this is quite a bit of work.

I recommend just doing the first part.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.