Fergus Henderson [EMAIL PROTECTED] writes:
Could you give an example of language syntax that you feel would be
better than putting these properties in the type system, while still
allowing similar compile-time checking?
I already gave NU-Prolog and Eiffel as examples.
Those languages don't provide the same kind of static
checking as Cayenne, because they don't provide a place
for the user to put proofs. But extending them with
some kind of syntax for proofs shouldn't be too hard, I think.
Once you've got the proofs in there, I believe checking
them at compile-time should be straight-forward.
I downloaded the NU-Prolog manual and skimmed it, but I didn't see the
features you're describing (probably because I haven't "done" Prolog
since my learn-5-languages-in-a-quarter class 12 years ago). Could
you give me a pointer to which section of the manual I should read?
For Eiffel, as far as I can tell, what you get are assertions in
function declarations (pre- and post-conditions on the functions). I
believe that the compile-time checking possible in Cayenne or other
hypothetical dependently-typed languages is significantly more
expressive.
Consider the Haskell function sortBy:
sortBy :: (a - a - Ordering) - [a] - [a]
Suppose you wanted to verify that the output of sortBy was sorted
according to the supplied comparison function. (This is half the
specification of a sorting function; the other half would be that the
output is a permutation of the input.) In other words, suppose we
want to verify that the comparison function, when applied to every
successive pair of values in the output, returns either LT or EQ
(never GT). This can be easily expressed as a postcondition on
sortBy.
Unfortunately, it cannot be proven; you need constraints on the
comparison function. (For example, with the comparison function
compare x y = GT
no list with two or more elements could ever be sorted.)
At a minimum, for any x and y, it must not be the case that
x `cmp` y == GT
and
y `cmp` x == GT
It must be a precondition on sortBy that the comparison function
satisfies this constraint. This can be expressed as a precondition,
if preconditions can have universally quantified formulas (so
preconditions can no longer be executable).
Now, when you define a sorting function, you want to state and verify
the above property. Where does it go? It's not a postcondition of
the comparison function, because it relates multiple different calls
of the comparator. What syntax would you use to state that only some
functions of type (a - a - Ordering) are acceptable as arguments to
sortBy? How does the compiler verify that calls to sortBy use only
acceptable comparison functions?
To me, the set of "acceptable comparison functions" feels like a type,
so "encoding" this requirement in the type system is natural. It also
means that you don't have to think about a separate verification
compiler pass to perform the compile-time checking; it's part of type
checking, which I find conceptually clear and simple.
Carl Witty
[EMAIL PROTECTED]
