[mercury-users] Types as sets?

[Richard A. O'Keefe]

"Douglas Auclair" <dauclair at msn.com> wrote:
	:- type natural ---> ???.  % how do I put only all the positive integers 
	here?
	:- type whole ---> zero; ?natural?.  % how do I say that whole numbers are 
	all the natural numbers and zero?
	
To start with, it is confusing to find the positive integers called
'natural' (which in computing and much of mathematics always includes 0)
and the natural numbers called 'whole' (which when I was at school included
the negative numbers; just because -2 is negative doesn't make it
fractional or algebraic or anything like that).

:- type natural
   ---> zero
      ; nonzero(positive).

:- type positive
   ---> successor(natural).

Now, when you _write_ a natural number like 3,
you'll have to _write_

    nonzero(positive(
      nonzero(positive(
        nonzero(positive( zero )) )) ))

but the successor(_) tag, being the only alternative for its type,
won't have any run-time representation in Mercury.

You can also have

:- type integral
   ---> negative(positive)
      ; non_negative(natural).

and here the tag bit is the sign and you want that.

	Another way of stating the problem is that, for example, I know that a 
	particular variable is constrained to a subset of values of another type, 
	but the compiler doesn't know this, and I wish to create a new type that 
	reflects this knowledge, so that:
	
	:- pred p(two_digit_natural::in, string::out) is det.
	p(1, "one").
	% ...
	p(99, "ninety-nine").
	
Setting up a system of _new_ types which includes, via appropriate (and
cheap) wrapping, the subtypes you want, is no problem.

Creating subtypes of _existing_ types is seldom an easy thing to do.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------