[mercury-users] Circular lists

[Fergus Henderson]

On Thu, Nov 27, 1997 at 02:24:26PM +1100, Richard A. O'Keefe wrote:
> Basically, I guess what I'm saying is that static checks are very much
> in the spirit of Mercury, so what static checks on the foreign interface
> are doable and likely to be done?

Well, there's a number of things you could subvert:

	- memory management assumptions
	- types
		+ basic types (string, int, float, char)
		- user-defined types
	- modes
		+ in vs out
		- uniqueness
		- in vs in(any), or out vs out(any)
	- determinism
		+ whether or not a goal can fail (det vs semidet)
		+ possibility of computing multiple solutions
		  (det/semidet vs multi/nondet)
		- committed choice (det/semidet vs cc_multi/cc_nondet)
	- purity (i.e. no side effects without an explicit io__state pair)
	- termination analysis

The existing Mercury C interface provides static checks that
the cross-language interface doesn't subvert the ones marked `+' above.
The way this is done is that these characteristics are reflected
in the prototype of the C inferface function; the Mercury compiler
generates a C declaration for exported procedures or a C function call
for imported procedures, and this is fed to the C compiler, which checks
the consistency of the calls with the declarations.

Of course, the C code might subvert these internally, e.g. with a cast. 
We don't do anything to prevent that.  Although we do provide some
static checking of foreign language interfaces, the aim is mainly to
prevent accidental errors, not to detect or prevent deliberate subversion.

OK, that was the status quo, now for what is feasible.
We could do a better job of static checking for user-defined types.
Currently any user-defined type becomes `Word' in the C interface, but
we could provide a C type for each user-defined type, and pass that instead.
If you want termination analysis, uniqueness analysis, purity analysis,
etc., you would need a C compiler or C analysis tool that could
check these; you'd also need to modify the Mercury compiler to spit
out whatever annotations the tool needs on the C code.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   WWW: <http://www.cs.mu.oz.au/~fjh>  
Note: due to some buggy software and a (probably accidental)
denial-of-service attack, any mail sent to me between
	Tue Nov 25 20:00:00 UTC (6am Wed, local time)
and	Wed Nov 26 06:00:00 UTC (4pm, local time)
may have gone into the bit-bucket.  Please re-send it.