[cffi-devel] expressive types (was: cffi/allegro crash)

[Hoehle, Joerg-Cyril]

Luis Oliveira
>Let me see if I got this straight, your proposal is that the :pointer
>type may or may not accept NIL (but it should documented as
>non-portable),
No. :pointer is documented to only accept valid CFFI pointers.
These are documented as opaque.
Code using NIL is in error, as well as code using 0.

> and that we should provide a second pointer type that
>is guaranteed to translate between the null pointer and NIL.
Yes, because such a type is useful.  Well, for Allegro not really -- forget it.

Another useful addition is a pointer type which does not accept a null-pointer, but signals an error instead, or just specifies that "passing (null-pointer) is an error".  This type can be used in function declarations.  The effect is two-fold:
a) just from seeing the declaration, you know that NULL is not allowed.
b) optionally, the transformers could check for this at run-time.

It's like the difference between C-PTR and C-PTR-NULL in CLISP.
Expressive type definitions are what I'd like to arrive at.

There are plenty of functions in the C lib where NULL is not allowed, yet you cannot tell it from reading the .h files.
The difference between NULL not allowed vs. allowed is fundamental to program verification. That's the first thing that other languages, which aim at formal verification distinguish.  E.g. Cyclone is IIRC such a dialect of C.

Regards,
	Jörg Höhle