Re: [Caml-list] Unsoundness is essential

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-10-04 at 01:13 +0200, Vincent Aravantinos wrote:
> Le 4 oct. 07 à 00:50, skaller a écrit :

> > 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. 

Yes, this is a valid criticism. Can you please help refine my idea
to take this into account?

What we want is to push the programmer into using the most
checkable form, and only let them 'escape' if it is really
necessary (I hope you agree with that summary!)

But I have no idea how to do that in a coherent way.
A kind of Occam's Razor of programming .. :)

In C++, this is done by encouraging programmers not
to use casts, but still allowing them, and indeed,
providing a more refined and pointed set of casts as well:

	static_cast, dynamic_cast, const_cast, 
	reinterpret_cast

These are long winded (deliberately) and frowned upon so there
is both mechanical (I hate typing) and psychological (peer
pressure, pride, etc) pressure NOT to use casts, and this
is encourage by the fact that C++ needs a LOT LESS casts
than C.

In Ocaml .. Obj.magic is 'evil' and not documented..

But this is a really WEAK form of pressure.

> 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.

Yes, but the problem now is that all these new languages are
coming out and the designed IGNORE all the good academic work.
Java, Ruby .. to name two examples of *new* rubbish which are
immensely popular, whilst Ocaml and Haskell haven't taken off.

> I think it's a good thing to constrain the programmer.

No dispute. I'm not arguing for NO constraints. In fact
it is the other way around. I'm arguing to allow the programmer
to apply MORE constraints in the form of more expressive types
EVEN IF THESE CONSTRAINTS CANNOT BE ENFORCED.

>  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!".

Yes. I have to tell you that I use this idea systematically
as a programming technique!

However many things annoy me, some of which I have tried to
fix in Felix. One of them is that modules/functor do not
allow expression of semantic rules: Felix has typeclasses
WITH semantic rules.

Although the rules are limited, Felix can actually generate
a vast battery of axiom checks, and, it currently emits
theorem claims in Why encoding which allows the claims
to be checked by various theorem provers, including Ergo.

None of this comes close to doing what I actually need in
the Ocaml code of the compiler itself, which is a to enforce
invariants of the term rewriting system in the type system.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net