[mercury-users] Appreciate some help #4:

[Thomas Charles CONWAY]

tcklnbrg, you write:
	[this is a bit frustrating - if you were here, 1/2 an hour
	 in front of a whiteboard, and you'd be happily on your way.
	 email is a difficult medium for this kind of thing]
	[oh, and just a small note - we have evolved a (loose) system of
	 formatting that makes programs easier to read and easier
	 to get right, so you too may find it helpful to be careful
	 about formatting]

> % test.m----Please look at this example and tell me if I understand it. 
> Thanks very much.
> 
> :- module test.
> :- interface.
> :- import_module io, string.
> :- type classname ---> validateClassname(string).

I think that you may mean:
:- type classname ---> classname(string).

or

:- type classname == string.

> 
> :- pred validateClassname(string::in) is semidet.

This looks fine. Presumably it just checks whether a given
string is a valid class name (as opposed to checking whether
the appropriate source/etc file exists).

> :- pred javaclass(classname::in) is det.

I get suspicious straight away when I see det predicates that
have only input arguments. Logically they are quivalent to `true'.

> :- pred main(io__state::di, io__state::uo) is det.
> 
> 
> :- implementation.
> 
> validateClassname(S):- string__is_alpha(S).
> javaclass(C).
> % the actual javaclass clause would be read in at runtime.

What do you mean by this comment? Is this a place-holder that would
turn into something like:

	% javaclass(Name, IsAValidClass, IO0, IO)
	% Binds IsAValidClass to `yes' if `Name' denotes a
	% valid java class ..., or to `no' otherwise.
:- pred javaclass(classname, bool, io__state, io__state).
:- mode javaclass(in, out, di, uo) is det.

javaclass(Name, IsAValidClass) -->
	% search all the right paths for Name
	....

> 
> main--> {javaclass(validateClassname("123"))}->
> io__write_string("OK\n\n");  io__write_string("Failed\n\n").
> 
> /* the above prints "OK" implying that the function
> validateClassname("123")
> is never called --compiler admits main
> cannot fail.  
> 

Hang on, hang on. validateClassname is the name of a *functor* and
the name of a *predicate*, but not the name of a *function*.

Do you mean:

main -->
	{ Name = "123" },
	( { validateClassname(Name) } ->
		javaclass(validateClassname(Name), _IsOk),
		...
	;
		...
	).

The *functor* validateClassname that was in the classname is a
data-constructor not a function.

> The module also compiles and runs without any definition for 
> pred, validateClassname.  I have tested, also, that a string which would
> fail the "is_alpha" test, including a "", also succeeds.

This is because your program never calls validateClassname.

[incorrect suppositions about the type system deleted]

When you declare a type:

:- type classname ---> this_is_just_a_functor(string).

you are telling Mercury that you want a type called `classname' which
denotes a set of terms all of the form:
	this_is_just_a_functor(<any old string can go here>)

Now, if you want to attach some meaning to the string, then you need to
check that when you construct the term:

:- pred make_classname(string, classname).
:- mode make_classname(in, out) is semidet.

make_classname(String, ClassName) :-
	check_string_has_right_properties(String),
	ClassName = this_is_just_a_functor(String).

Now you can pass around things of type classname, and know that if
this is the only place where you construct classnames then they
have the right form.

Thomas
Maybe we should take this discussion off mercury-users?
-- 
Thomas Conway <conway at cs.mu.oz.au>
Nail here [] for new monitor.  )O+