Fergus Henderson <[EMAIL PROTECTED]> writes:
> > It is, however, also clear that when in using dependant types, much more
> > type information and documentation are provided. If, in fact, the example
> > from above can be type checked (question [2]), then it is clear that
> > dependant types are a *huge* bonus to more formally developing programs.
> > Since essentially anything (well, minus partial functions and some other
> > good things) can be specified in Lof's type theory, it becomes possible for
> > the programmer to use formal methods to any extent he desires, with theorem
> > proving being equivalent to the program type checking.
>
> 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. I attribute this to Haskell's strong type system.
Haskell's type system also provides a safety net in that if I change a
data type in a program, the compiler will inform me of any places I
forgot to change. This is why I want a stronger type system, to make
it more likely that my programs will work the first time, and continue
to work after modifications.
> When you only have a hammer, everything looks like a nail.
> If type checking is the only form of compile-time checking,
> then the only way of checking something at compile time is to
> make it part of the type system. And so the desire for
> better compile-time checking may lead us to create very
> complicated type systems. 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 fear that my brain has been warped by too many years of thinking
about type theory. I've managed to convince myself that these
properties ARE types, and that putting them in the type system is the
clearest and most straightforward way of expressing them.
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?
Carl Witty
[EMAIL PROTECTED]
