> Well, yes, up to a point, but it may be clearer if the simple
> regular types part is kept separate from the undecidable part,
> as was done in NU-Prolog, or as is done in Eiffel.
I'm not necesssarily advocating that the properties and proofs of these
properties should be mixed with the regular code. That's just
one way of doing it. Take sort as an example, we can do this
(ignoring the compare function):
sort :: (xs :: [a]) -> ListTypeWithProofOfCorrectnes xs
sort xs = ... sort code with integrate proof
or this
sort :: [a] -> [a]
sort xs = ... normal sort code
sortReallySorts :: IsASortingFunction sort
sortReallySorts = ... proof that sort really sorts
Both of these styles are perfectly feasible to express in Cayenne.
Which one to use depends on the situation (and your taste :-).
I guess you prefer the latter.
BTW, has Eiffel changed? Last time I looked you could only
have assertions checked at runtime, and no correctness proofs.
If you were talking about assertions, you might as well have said C. :-)
> > I don't see how these properties can be expressed in a different way
> > even if they were outside the types. You may object to the notation
> > used, but give me a font with quantifiers and I'll make it look pretty. :-)
>
> You may be right, but I won't believe it until I see it ;-)
Well, I won't believe that you can make it any easier by moving
the proof out of the instance declarations. Defining what an
equivalence relation is will look similar in other notations.
> BTW, don't get me wrong -- I think Cayenne is a very interesting
> language, and it's a very promising line of research. I'm just
> saying that I think we should be very cautious about adopting
> this kind of thing into Haskell-2.
I've not been advocating that either. I'm advocating some form
of dependent types. I would like to see dependent records, but
you could limit the dependency to be on types (just as Haskell
already has for the function tupe). That way records can replace
modules (if you add some other little goo).
Let me just point out that my main interest in dependent types is
NOT to do specifications and proofs (like sort above), but to
make the type system more expressible. This way we can make more
programs typeable, and also give more accurate types to programs.
The latter is well illustrated in a paper by Hongwei Xi and Frank
Pfenning in POPL99.
-- Lennart
