Le 28 févr. 07 à 05:01, Jacques Garrigue a écrit :

> Wow, here is a strong statement. Basically, you seem to be saying that
> types are useless for safety if they don't ensure full correctness,
> and that in the absence of safety they need to be nominal in order to
> declare any intent?

I think you took the statement stronger that I intended (my fault).  
I'm certainly not saying types are useless for safety without  
correctness. I find it _immensely_ usefull that a machine takes care  
of the bureaucracy of types and I often wonder, when the compiler  
reminds me, how bad my software development would be in a dynamically  
typed language -- not even talking about those in which you don't  
declare your identifiers.

My statement was really about the module system part of the type  
system. I sometimes find it a little bit artificial that if your  
module structuraly matches a signature you can pass it to a functor.  
If you take the point of view of a programmer who is provided with  
modules he didn't write, I think it makes it easier for him to make  
correct functor applications in a nominal setting because modules  
explictely indicate that they were designed to support a given  
interface. On the other hand, nominality hinders code reuse since you  
may found a use that the initial programmer couldn't ever foresee.  
But this problem can be alleviated by a simple construct that allows  
to extend a module to support a new interface (even if no new code  
needs to be written).

Besides that, I agree with most of your points, even though your  
`Apples may be oranges to me but I quite buy your probabilistic  
argument.

Best,

Daniel