[mercury-users] Types as sets?

[Douglas Auclair]

Dear all,

I've run into a problem quite a few times:  I'm creating a type where I'd 
like one of the members of that type to be some or all the members of 
another type.  So, for example:

:- 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?

Wholes could have their own set of predicates, seperate from naturals, so I 
don't think I'm looking for covariant/contravariant inheritance schemes 
here.

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").

will compile (I know the above is a silly example, but I do run into this 
kind of problem quite often and I prefer the declarative syntax to the 
if-then-else (i.e. ->) spagetti-nested mess).

Is there a way, currently, to create the type two_digit_natural that will 
allow the above code to compile?

An example I used as a work-around is in the apple-darwin port:  
send_money_quickly.m (I've also attached the module to this email) which 
uses the Peano series and DCG to solve a cryptarithmetic problem 40x faster 
than the same problem solved using ints in crypt.m (proving that there is 
indeed a practical application to implementing the Peano series ... that is, 
besides assigning to (under)grad students as a homework assignment).  
Although effective, I see it as a hack (please don't tell Peano I said 
that).  I'd prefer to define the new type as a (limited) subset of another 
type or as a union of some predefined types.  Is this possible in Mercury?

Another workaround that I've used commonly is to declare a helper predicate 
as (cc_)multi to a det main predicate and follow this pattern:

:- pred column_as_int(int::in, char::out) is det.
column_as_int(Int, promise_only_solution(convert_int_to_char(Int))).

:- pred convert_int_to_char(int::in, char::out) is cc_multi.
convert_int_to_char(1, 'a').
% ...
convert_int_to_char(8, 'h').
convert_int_to_char(_, '_').

which, of course, it very hackish.  Is there a clean alternative to that?  
I've also done:

convert_int_to_char(X, '_') :- (X < 1; X > 8) -> error("Integer input is out 
of range").

as the last alternative for the helper predicate, but I don't like that 
either:  one is deferring a check until runtime that should be handled by 
the compiler.  In either case, I believe that a well-defined type system 
should eliminate the need for the "catchall" that the user writes.

So, the problem is that I'm working with predefined types that are unbound 
or very large, and I know that my system has a limited subset of values of 
these types or a combination of these types, but the compiler rejects my 
programs because I have not found a way to express this knowledge to it.  Is 
there a way to do this well in Mercury (expressively in the code and, e.g., 
speeds up the executable because the compiler can use the information on the 
limited/combined types to eliminate type/value checks later on)?  Is your 
group conducting research along these lines to implement in future versions 
of the compiler if it's not there now?

Sincerely,
Doug Auclair

_________________________________________________________________
Add photos to your messages with MSN 8. Get 2 months FREE*.  
http://join.msn.com/?page=features/featuredemail
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: send_money_quickly.m
URL: <http://lists.mercurylang.org/archives/users/attachments/20030211/63cc80a5/attachment.ksh>