From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 91F30BC69 for ; Thu, 4 Oct 2007 03:55:06 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANPkA0fAXQInemdsb2JhbACONwEBCQo X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="3724030" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 03:55:06 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l941t5FF000745 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 03:55:06 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPHkA0fLENaMnmdsb2JhbACONwEBAQEHBAYPGA X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2103614" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 03:55:04 +0200 X-IronPort-AV: E=Sophos;i="4.21,226,1188743400"; d="scan'208";a="203772749" Received: from ppp121-44-123-220.lns10.syd6.internode.on.net (HELO [192.168.1.201]) ([121.44.123.220]) by ipmail01.adl2.internode.on.net with ESMTP; 04 Oct 2007 11:19:57 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Vincent Aravantinos Cc: Christophe Raffalli , oleg@pobox.com, caml-list@inria.fr In-Reply-To: <38BB2D08-E5D5-4A02-A3BF-7B0B51C2311F@yahoo.fr> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <38BB2D08-E5D5-4A02-A3BF-7B0B51C2311F@yahoo.fr> Content-Type: text/plain; charset=utf-8 Date: Thu, 04 Oct 2007 11:49:56 +1000 Message-Id: <1191462596.7542.73.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 470447F9.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 annotations:01 bounded:01 casts:01 casts:01 const:01 ocaml:01 ocaml:01 haskell:01 functor:01 emits:01 ergo:01 compiler:01 invariants:01 rewriting:01 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 Felix, successor to C++: http://felix.sf.net