[m-dev.] Re: for review: big rats

[Peter Schachte]

On 9 Apr 1998, Bert Thompson wrote:

> |In this case, the builtin unification will do the correct thing, so you
> |can just delete this predicate.  However, a comment next to the type
> |definition about the type's invariant and why it is needed (to ensure
> |that the builtin equality gives correct results) would be a good idea.

There are probably other places in the code where it's assumed that the
representation is normalized.  As I recall at least the absolute value code
assumed this.

> I've done this, but I think adding the `where equality is <blah>'
> approach may be preferable since it makes the code blindingly obvious:
> it does what it says not what the comments say.
> (Who has any faith in comments?)

Not me.  But this won't work, if what I said above is true.  It'll only fix
the problem for unification, not for other places where the representation
is assumed to be normalized.

This is interesting:  there are actually two potential problems with types: 
1) when the type is not canonical (two distinct objects represent the same
value), and 2) when the type is not total (some instances of the type are
not admissible).  Unfortunately, 'where equality is ...' only solves the
first problem.

So Lee, how about incorporating your extended type system into Mercury, so
users can attach statements (predicates) to types, where all members of the
type are assumed to obey the regular type definition plus the predicate? 
Then throw your proof system into the compiler and spit out an error message
when the extended type can definitely be violated, and a warning when it
can't be proved that it won't be violated.  In the latter case, when
compiled in --debug mode, also insert sanity checking code where safety
can't be statically guaranteed.

Sounds like there's probably a good PhD in there for someone.


-Peter Schachte               | When I give food to the poor, they call me a
mailto:pets at cs.mu.OZ.AU       | saint. When I ask why the poor have no food,
http://www.cs.mu.oz.au/~pets/ | they call me a communist.
PGP: finger pets at 128.250.37.3 |     -- Dom Helder Camara