Re: [Caml-list] Unsoundness is essential

[Vincent Aravantinos <vincent.aravantinos@yahoo.fr>]

Le 4 oct. 07 à 00:50, skaller a écrit :

> On Wed, 2007-10-03 at 22:39 +0200, Christophe Raffalli wrote:
>
>> So the story is by saying (wrongly) that it is too heavy to anottate
>> arrow types with exceptions,
>> making the arrow type a ternary type construct, ML is missing a  
>> lot ...
>
> To be bold I propose type theorists have got it totally wrong.
> ...
> expressive type systems. Stop CHEATING by refusing to allow
> me to write types you can't check -- because this forces
> ME as the programmer to cheat on the type annotations:
>
> 	divide: int * int -> int
> 	hd : 'a list -> 'a

If you allow everything (such as the "type expressive" C you are  
envisaging), the programmer will be tempted to use this "everything"  
whereas he could achieve the same with a "bounded" language. And in  
this case I bet the programmer won't do things that will ever be  
"type theoretic friendly", whatever progress in type theoretics will be.

To my eyes it looks like many things that appeared in other languages  
to appeal the programmers, but that could be achieved in other (did I  
say better ?) ways. If you allow everything, people will be tempted  
to do anything... And any progress in computer science will never  
catch the gap.

I think it's a good thing to constrain the programmer. How many times  
I thought "that's a pity I can't do this *as I want* in ocaml". And  
then after having been forced to think of another way to achieve my  
goal *within the constraints of ocaml*, I ended with something like  
"woah, actually it's better this way!".

Cheers,
Vincent