[m-dev.] for review: use bitsets in quantification

[Fergus Henderson]

On 06-Nov-2000, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> 
> > > @@ -410,10 +437,13 @@
> > >  
> > >  :- pragma c_header_code("
> > >  	#include <limits.h>
> > > +
> > > +	#define ML_BITS_PER_INT		(sizeof(MR_Integer) * CHAR_BIT)
> > >  ").
> > 
> > Technically that is making an assumption which standard C does not guarantee,
> > namely that integers have no p, since integer types
> 
> The code there is just copied from the original definition of
> int__bits_per_int.

Sorry, that comment was incomplete -- I meant to delete it, but obviously forgot.

What I was going to say was

	Technically that is making an assumption which standard C does not guarantee,
	namely that integers have no padding bits.

but this is not worth worrying about, since no important current or
future C implementations will ever use padding bits in integer types
(to do so would be commercial suicide: too much code makes this same
assumption), so I decided not to say it.  Oh well, guess it slipped out
anyway ;-)

>  :- module enum.
>  
>  :- interface.
>  
> +	% For all instances the following must hold:
> +	%	all [X, Int] (Int = to_int(X) => X = from_int(Int)).
>  :- typeclass enum(T) where [
>  	func to_int(T) = int,
> |	func from_int(int) = T is semidet
>  ].

You could write the invariant more concisely as

	%	all [X] from_int(to_int(X)) = X

There's still several problems with this type class:

1.  The use of `int' rather than `integer' here is somewhat
problematic.  For example, it prevents types such as `int64' or
`int128' from being instances of this class.  It might also be worth
providing an `enumerable' type class that was the same as `enum'
except that it used `integer' rather than `int'.

2.  The use of `int' means that all instances of this class must be
bounded.  However, you don't provide any means to find out what the
bounds are.  That makes it impossible to e.g. write a `dense_bitset'
type (implemented using an array of ints rather than a list of ints)
using this type class.  So I think it would be a good idea to add the
following methods:

	func enum_first = T,
	func enum_last = T,

with the following invariants:

	all [X] to_int(enum_first) =< to_int(X)
	all [X] to_int(X) =< to_int(enum_last)

[Another alternative would be to add a `bounded' type class,
and an `ordered' type class,

	:- typeclass ordered(T) where [
		% we can debate the details of this class some
		% other day...
		func cmp(T, T) = comparison_result
	].

	:- typeclass bounded(T) <= ordered(T) where [
		func min = T,		% all [X] cmp(min, X) \= (>)
		func max = T		% all [X] cmp(max, X) \= (<)
	].

and then either have

	:- typeclass enum(T) <= bounded(T) where [
		...
	].

or have places that rely on boundedness to use `enum(T), bounded(T)'
rather than `enum(T)'.  But that alternative doesn't really solve the
problem, because it assumes that `to_int' preserves the ordering, i.e.
that the ordering on T is the same as the ordering on the ints that
result from to_int.  Making that assumption would be unwise since many
enumerable types won't satisfy it.]

3.  Although the class is named `enum', the invariants given are not
sufficient for you to actually enumerate the values of the type (or at
least not with reasonable efficiency).  For example, to get the next
value after X in the enumeration sequence, you could try
`from_int(to_int(X) + 1)'.  But there is no guarantee that this call
to `from_int' will succeed.  So I think you should add another invariant:

	all [Int] ((enum_first =< Int, Int =< enum_last) =>
		some [X] X = from_int(Int)).

4.  It would be a good idea to add some procedures to the `enum' module
for enumerating values.  For example, Haskell provides the following:

       succ, pred       :: Enum a => a -> a
       enumFromTo       :: Enum a => a -> a -> [a]        -- [n..m]
       enumFromThenTo   :: Enum a => a -> a -> a -> [a]   -- [n,n'..m]
       succ             =  toEnum . (+1) . fromEnum
       pred             =  toEnum . (subtract 1) . fromEnum
       enumFromTo x y   =  map toEnum [fromEnum x .. fromEnum y]
       enumFromThenTo x y z =
                           map toEnum [fromEnum x, fromEnum y .. fromEnum z]

However, this is not required for the sparse_bitset stuff, and can be
done as a separate change.

> --- int.m	2000/11/06 03:26:40	1.2
> +++ int.m	2000/11/06 03:27:20
> +:- instance enum(int) where [
> +	func(to_int/1) is id,
> +	func(from_int/1) is id
> +].

You might want to consider using the new syntax for instance declarations:

	:- instance enum(int) where [
		to_int(X) = X
		from_int(X) = X
	].

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  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
--------------------------------------------------------------------------