[EMAIL PROTECTED] writes:
> [EMAIL PROTECTED] writes:
>
> > enabling types to express all properties you want is, IMO, the right way.
>
> Why do I feel that there must be another approach to programming?
>
> How many people do you expect to program in Haskell once you are done adding all
> it takes to "express all imaginable properties through types"? What kind of
> baroque monster will it be? Is type really _the_ medium for everything?
I would certainly love to program in a language that let me specify
that a sorting function really did sort. Also, I am confident that if
done right, a dependent type system could be added on to Haskell such
that all existing Haskell programs would continue to be valid.
I see a couple of reasons to "enable types to express all properties
you want".
1) I've been following efforts in the theorem proving/proof
verification community which are based on this idea. Several
type-theory based verification systems are based directly on
expressing properties in types (e.g. Coq, LEGO, the Alf* family,
NuPRL). Others (PVS and Ontic) gain a lot of mileage out of a very
expressive type system. (My apologies for any relevant systems I've
left out here.) Based on these efforts, it seems very natural to me
to extend this idea to a real, usable programming language.
2) Type checking has been widely studied and is pretty well
understood. It makes sense to take this base and use it to make
languages even more powerful and expressive.
Carl Witty
[EMAIL PROTECTED]
