On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> [Fergus wrote:]
> > The basic problem that I have with this is that although dependent types
> > do allow you to specify a lot of things in the type system, I'm not sure
> > that using the type system is really the best way to specify these things.
>
> Well, I think types are just the place for these things. People already
> use types as a partial specification, enabling types to express all
> properties you want is, IMO, the right way.
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 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 ;-)
I don't think it's just the font that is the issue. For example,
I find the use of instance declarations for expressing proofs of
correctness to be rather unintuitive. I don't think a different
font will fix that.
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.
--
Fergus Henderson <[EMAIL PROTECTED]> | "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh> | but source code lives forever"
PGP: finger [EMAIL PROTECTED] | -- leaked Microsoft memo.
