> > 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
> )
Heh, thank you. :)
> 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
*Personally,* I like the way I did it better. It might be silly to get into
style arguments, but I do think a discussion of which is a better style is
worthwhile: an official coding style wrt/ dynamics is a good thing, imo.
> 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.
Hm. I don't care much for this argument. I think people familiar with Java,
C++, Eiffel, are already with a disadvantage with functional programming:
the whole style of programming with higher order functions is foreign to
them.
The introductory programming course is in Scheme (for (EE)CS majors) at my
university. Everybody in the class has had some programming experience
(there's an entrance exam)--99% of them with imperative languages. For most,
using higher order functions like map, and lambda abstractions took time to
get used to. They got used to it however.
When imperative programmers go from C++ or whatever to Scheme, they have to
now think of "functions as data." Now, we're asking them to think of "types
as data."
1) I don't think we're asking them to leap that much further.
2) Who cares about imperative programmers anyway: our goal is to write
*correct* software with optimum productivity (and secondarily, optimum
performance). If extra effort is required *initially* to use dependant
types, but they further that goal, then add 'em.
> 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.
Dynamic types are in my opinion a necessity. There may very well be a debate
about this, but I'll completely grant you this point. We need them.
> > 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.
Hm. I don't care to see the proof. I only want to know that the function
satisfies its specification. But I'm also unsatisfied with Lennart's
"recording-up" of the proof.
I'm hoping one can express sort in a different way.
Lennart's:
sort :: (l :: [a]) -> sig { r :: [a]; o :: Ordered r; p :: Permutation l r }
I want the range of sort to be list... Rather, I want the range of sort to
be a subtype of [a]. That way you can keep the specification with the
implementation and you don't have to extract values from a tuple or a
record. How do you do this Lennart?
I want to be able to say:
(foldr (-) 0) . sort
Without having some spurious "sortReallySorts."
I am I stupidly assuming this is possible when it isn't?
I can't think of a good way to do this... My first thought was my own list
ADT:
data myList a = MkMyList [a] [a->#]
e.g., egList = MkMyList [1, 2, 3, 4] [Ordered, Permutation [4, 3, 2, 1]]
This works if I define my foldr for MkMyList and such, but this is yucky.
...I thought about this pretty hard. Particularly I thought about using
classes; this was fruitless. So I decided I'd invent a new language feature
and a nice little syntax to handle it.
Sorted l r = Ordered r /\ Permutation l r
sort :: (l :: [a]) -> (r :: [a]) <= Sorted l r
<= is the "magic operator". Basically it's equivalent to /\, except it
allows us to pretend that we're not dealing with the tuple generated by /\.
In other words, if there were a subtype relation <:, then
((r :: [a]) <= Sorted l r) <: [a]
so we can do things like
(foldr (-) 0) . sort
and not have to worry about anything. Note that the proof information is
never actually lost.
But Wait! there's more to my "magic operator"!
When we have dynamic types, check this out:
min2 :: [a] -> a
min2 ((l:ls) :: [a] <= Sorted) = l
min2 l = min l
If we have a program in which finding the minimum element of a list is a
costly operation (huge lists) and there's a sizeable probability that the
list has already been sorted, then min2 would be more efficient than min.
Heh. I'm not seriously advocating adding my magic operator to the language,
but I am pointing out that explicitly passing around proofs is a pain in the
ass. This is good evidence that Fergus is right when he says: "As a
programmer, I want the two to be clearly separated." However, his clear
separation would not allow min2, would it?
