On 19-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> I'll admit to not having yet written something in Cayenne, but I'm an
> adamant supporter of adding dependant types to the language. I remember a
> year ago, I was writing a small (trivial) program. One of the essential ways
> I was structuring the program was with a function "apply" similar to
> Lisp/scheme's apply. Needless to say, you can't express apply in Haskell
> although you can in Cayenne. In the context of this problem, I could easily
> get around this by restructuring my program, but this was obviously not
> ideal. We should be able to express trivial functions like apply in the type
> system.
If your language supports optional dynamic type checking, as it should,
then expressing functions like apply shouldn't be too hard.
I'm an adamant supporter of adding optional dynamic types to the
language. But I remain very cautious about the merits of dependent
types. I think it is quite possible that the additional complexity
of dependent types may outweigh their benefits.
> Foremost is that dependant types allow us to type more things than before.
Yes, but not as many as optional dynamic types allow.
For example with dynamic types you would not need to
change the order of the arguments for `apply'.
> It is also clear, however, that dependant types are no trivial thing.
> Expressing the most general type of apply--that's not a super-type--is a
> complicated process. It is clear that a large library of type functions will
> likely be necessary, I think. This can be used as an argument both for and
> against dependant types.
Indeed.
> 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 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.
--
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.
