[mercury-users] mode decls are promises? What are promise decls?

[doug.auclair at logicaltypes.com]

Dear all,

I have this bit of code to initialize a random switch:

-----
:- pred init_each_weight_n_threshold(peano, int, supply, supply,
	                             list(float), list(float)).
:- mode init_each_weight_n_threshold(in, in, in, out, in, out(non_empty_list))
        is det.

init_each_weight_n_threshold(zero, _, !RNG) --> [].
init_each_weight_n_threshold(s(Peano), Maxie, !RNG) -->
	{ random(Rand, !RNG) },
	cons(fdiv(Rand, Maxie)),
	init_each_weight_n_threshold(Peano, Maxie, !RNG).
-----

called with:

	init_each_weight_n_threshold(s(peano_from_int(Size)), Maxie, R1, _RNG,
	                             [], [Threshold|Weights]).

Now, since the initial call has Peano always some successor to zero, then
the out(non_empty_list) is the correct mode argument, and the program
compiles and runs as expected.  But how does the compiler know or
guarantee this?  For, when I change the call to:

	init_each_weight_n_threshold(peano_from_int(Size), Maxie, R1, _RNG,
	                             [], [Threshold|Weights]).

(n.b.: no more successor on the peano_from_int/1 result), it still compiles
but dies at runtime with a "caught bus error" when Size is set to 0.  Is this 
a compiler bug? After all, isn't the Mercury compiler proving the program 
logically consistent? Or, is there a way to associate the knowledge that 
Peano is always a successor to zero on the initial call, guaranteeing 
(/"promise"ing? or proving?) that  ListOut /will/ be a non_empty_list inst?

Sincerely,
Doug Auclair

P.S. A side issue is that I'm unclear as to what the 'promise' declaration
does -- it seems to be a declaration that is skipped in the refman.  I
see it in e.g. the list module and see it's descriptive (to the user)
declarative value ... is it, at the same time, telling the compiler something,
so that code that it may declare as erroneous it instead compiles on the
grace of the promise?  What does ':- promise <foo>.' do? and where do
I find its precise definition and usage?

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------