> If your language supports optional dynamic type checking, as it should,
> then expressing functions like apply shouldn't be too hard.
Here's a dynamic apply in a pseudo Clean 2.0 syntax:
apply :: Dynamic [a] -> a
apply (f :: a -> b) (arg:args) = apply (dynamic (f arg) :: b) args
apply (f :: a) [] = f
apply _ _ = Error "Run Time Type Error!!"
Personally, it's 6 of one, 12/2 of the other, for me. With dynamics you fill
up apply's definition with noise. With dependant types
apply :: (F a *) [a] -> (F a *)
apply f [] = a
apply f [a:as] = apply (f a) as
The type gets noisier.
> 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.
That's definitely a valid argument. We have to be willing to good eschew
type inference altogether (I think), to add dependant types.
> > 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'.
Indeed. But it's a question of the best tool for the job. You can basically
make any function accept and return anything with dynamic types--make your
program have as much static checking as a Scheme program ;). Or you can use
dependant types and essentially do everything statically. Two tools that can
work together, IMO.
> > 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.
I completely disagree with this argument. Your example is valid, but I think
it stems from a mistaken understanding of the type system. We're not just
extending HM in the case of Cayenne, we're implementing Martin Lof's
constructive type system. It's a whole new ballgame. This is not a hammer;
Lof's type theory is all about expressing proofs and such. I'm talking about
the curry-Howard isomorphism
Implication is the arrow (->)
Universal quantification is a function,
etc.
There are two ways to look at Cayenne, fundamentally:
- As a programming language
- As a system for expressing proofs.
They're equivalent in Lof's system and amazingly, it's just as elegant in
expressing both: they're the same thing!
I recommend you read:
Type Theory and Functional Programming (International Computer Science
Series) by Simon Thompson
It was in my school library, and was a pleasure to read. In one of the
examples, they express the properties of the quicksort (permutation, etc.),
and then go on to prove that their implementation of quicksort satisfies the
specification.
It's not a hammer, it's a, um, pillow.
