[mercury-users] range of input

[Fergus Henderson]

On 08-Nov-1999, Robert Ernst Johann JESCHOFNIK <rejj at cat.cs.mu.OZ.AU> wrote:
> 
> As I was walking home from the train station this evening, I found myself
> thinking that it would be nice if there were a way to tell the compiler
> the range of input a particular predicate will receive for each variable.
> This would allow you to use pattern matching / switches with a
> non-exhaustive set of constructors.

For discriminated union types (a.k.a. algebraic types), you can do
that already, using insts as subtypes.
For example:

	:- type fruit ---> apple ; orange ; lemon ; banana.
	:- inst citrus_fruit ---> orange ; lemon.

	:- func num_pips(fruit) = int.
	:- mode num_pips(in(citrus_fruit)) = out is det.
	num_pips(orange) = 42.
	num_pips(lemon) = 35.

	:- pred is_citrus_fruit(fruit).
	:- mode is_citrus_fruit(ground -> citrus_fruit) is semidet.
	is_citrus_fruit(orange).
	is_citrus_fruit(lemon).

	:- func count_pips(fruit) = int.
	count_pips(Fruit) = NumPips :-
		( is_citrus_fruit(Fruit) ->
			NumPips = num_pips(Fruit)
		;
			NumPips = 0
		).

Here the num_pips/1 function takes as input a subset of the
possible values of the `fruit' type.

But if you want to allow integer ranges, then you really
need something that will do runtime checking.

> That wasn't all too clear, so here is an attempt to show what I mean:
> 
> :- pred  fib(int, int).
> :- mode  fib(in, out) is det.
> :- range fib({1;2;>=3}, all).
> 
> fib(1, 1).
> fib(2, 1).
> fib(X, Y) :-
> 	fib(X1, Y1),
> 	fib(X2, Y2),
> 	X + 1 = X1,
> 	X + 2 = X2,
> 	Y1 + Y2 = Y.

Presumably you should have a call to `X >= 3' or `X > 2' in the last clause.
And I think the `+ 1' and `+ 2' should be `- 1' and `- 2' respectively.
Anyway, that seems like a somewhat obfuscated way of writing `fib'.
I'd suggest using a function and writing it like so

	:- func fib(int) = int.
	:- range fib({1;2;>=3}) = all.
	fib(1) = 1.
	fib(2) = 1.
	fib(X) = Y :-
		X >= 3,
		Y = fib(X - 1) + fib(X - 2).

Here I've kept your `:- range' declaration, and I'm still using
separate clauses rather than an if-then-else, so this is not
legal in Mercury as it stands.

> Given "range" information, this wouldn't have to be semidet or multi. Any
> call out of the promised range should call error/1.
> 
> And yes, I'm sure the syntax for the range could/should be much nicer, but
> I'm just interested in the idea at the moment. Does this seem viable?

Let me play devil's advocate for the moment.
You can achieve the same effect by writing

	fib(X) =
		if X < 0 then error("fib: arg < 0") else
		if X = 1 then 1 else
		if X = 2 then 2 else
		fib(X - 1) + fib(X - 2).

	% Currently the standard library only has a predicate
	% version of error/1.  This function version should go
	% in the standard library too.
	:- func error(string) = _.
	:- mode error(in) = out is erroneous.
	error(Msg) = _ :- error(Msg).

So what would be the advantage in letting you write it using
the alternative syntax that you've suggested?

----------

Perhaps you are mixing several different things here.

  (1)	One issue is the idea of expressing properties such as
	admissability constraints which cannot be checked at compile
	time but which can be checked at runtime.

  (2)	Another issue or two is idea of extending determinism inference to 

	  (2a)	support analysis of calls to predicates like `>' and `>='
		on ints, to detect when things are mutually exclusive
		and when they cover all cases.
	and

	  (2b)	take runtime-checked admissability constraints into account.

Regarding (1):

	I think that extending Mercury to support that kind of thing
	would be a very good idea.

	I discussed this a bit in the "assertions summary" [1] that
	I posted to the mercury-developers mailing list. 
	That post included a proposed a syntax for runtime-checked
	post-conditions, but it did not discuss syntax for
	admissability constraints (i.e. preconditions).  However,
	Peter Schachte has previously proposed [2] on the same list
	the following syntax:

		:- admissable fib(X) => X > 0.
 
	I think we need two different variants, one for admissability
	constraints which are checked at runtime and one for those
	which are not.  So perhaps the syntax could be something like
	this:

		:- admissable fib(X) => X > 0.		% unchecked
		:- check admissable fib(X) => X > 0.	% checked at runtime

	However, it might be better to use a keyword or some other special
	syntax rather than `=>', to avoid mixing object level logic with
	meta-level logic.

Regarding (2):

	With (2a) alone, you would be able to write it as

		fib(1) = 1.
		fib(2) = 2.
		fib(X) = Y :-
			X > 2,
			Y = fib(X - 1) + fib(X - 2)
		fib(X) = Y :-
			X < 0,
			error("fib: arg < 0").

	With (2b), you could omit the fourth clause, instead using an
	admissibility declaration such as

		:- check admissable fib(X) => X > 0.

	(2a) is closely related to the proposal which has been
	championed by Richard O'Keefe of allowing users to declare
	which predicates (or goals) are exhaustive and mutual
	exclusive.  However, user declarations of such properties are
	not really an attractive solution to this particular instance
	of the problem, where you are dealing with integer ranges,
	because (at least with a simple approach) each such case would
	require a separate declaration.  You could given a general
	declaration that `X < Y' and `X > Y' are mutually exclusive,
	but in this case the compiler needs to know that `X < 0' and
	`Y > 2' are mutually exclusive, and since `2' is not `0',
	the general declaration doesn't help for this case.
	To avoid a plethora of declarations, I think determinism
	analysis would need to have some knowledge of integer
	arithmetic.  But then it gets hard to know where to stop;
	should the compiler just know (fixed-precision) `int' arithmetic,
	or would it have to know (arbitrary precision) `integer'
	arithmetic too?  What about `float'?  And so on.

	Personally I don't find the code for fib above to be a
	major improvement in readability over the version that I gave
	in the "devil's advocate" section above.  So I don't find
	the reasons for (2a) or (2b) to be compelling.


References:
[1]	<http://www.cs.mu.oz.au/mercury/mailing-lists/mercury-developers/mercury-developers.9804/0181.html>.
[2]	<http://www.cs.mu.oz.au/mercury/mailing-lists/mercury-developers/mercury-developers.9907/0225.html>.
-- 
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.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------