On 20-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> [Fergus wrote:]
> > 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.
(To correct a couple of minor typos, that should be
apply f [] = f
apply f (a:as) = apply (f a) as
)
I agree it is in some sense six of one and half a dozen of the other.
But I think that when using dynamic types, with an appropriate coding
style, you should be able to separate out the dynamic type tests and
the conversions to dynamic types a bit more clearly than you have done
above. For example:
apply :: Dynamic -> [a] -> b
-- code goes here -- dynamic type tests & conversions go here
apply f [] = f' where (f' :: b) = f
apply f (a:as) =
apply' (f' a) as where (f' :: a -> _) = f
apply' = apply . dynamic
I also think that the notion of dynamic types is quite straightforward
to understand (particularly for programmers with experience in other
languages that support similar constructs, e.g. Java, C++, Eiffel, etc.)
whereas the notion of dependent types is a bit more complicated.
You're right that we may well want to have both. But if we could only
have one, I'd rather dynamic types, and once we have dynamic types,
then the need for dependent types is much reduced. So we need to weigh
up the benefits and drawbacks of dependent types very carefully.
> 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 understand that, and I know about the Curry-Howard isomorphism,
and it is all certainly very conceptually elegant.
But from a programmer's perspective, the program and it's proof
of correctness are two different things. As a programmer, I want
the two to be clearly separated, so that I can tell at a glance
which part is the program and which part is the proof of correctness.
Using the same constructs for both could well make things easier, but
I still want some clear visual indication that distinguishes the two.
--
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.
