Re: Haskell 2 -- Dependent types?

[Lennart Augustsson]

> 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.

But I don't think we have found the right formalism for it yet.
E.g., equational reasoning doesn't look pretty in Cayenne.

> But when it comes to things like
> proving that `==' is reflexive, symmetric, and transitive,
> I think it may well be much clearer if these kinds of
> properties are expressed more directly, rather than by
> cleverly encoding them in the type system.
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. :-)

      -- Lennart