On 25-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> Fergus Henderson <[EMAIL PROTECTED]> writes:
>
> > 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.
>
> When I move back and forth between Haskell and other languages (these
> days, C and Scheme), I find that my Haskell programs--once they are
> accepted by the compiler--are a lot more likely to work the first
> time. I don't think this is just me; I've seen other people make the
> same observation.
Certainly.
> I attribute this to Haskell's strong type system.
I attribute this to strong static checking.
Type checking isn't the only form of static checking possible.
Other kinds of checks are useful too. For example, some Haskell
compilers warn about singleton variables, or about pattern matches
which don't cover all the possible cases. These checks are not
part of the type system, but they do help to make Haskell programs
work the first time.
> 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.
--
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.
