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.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id BA8FFBC69 for ; Thu, 4 Oct 2007 01:13:26 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj0KAGe/A0fZDAtPa2dsb2JhbACONwsEBg4SBw X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2098820" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 01:13:26 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l93NDQlE017853 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 01:13:26 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj0KAGe/A0fZDAtPa2dsb2JhbACONwsEBg4SBw X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2098819" Received: from smtp010.mail.ukl.yahoo.com ([217.12.11.79]) by mail1-smtp-roc.national.inria.fr with SMTP; 04 Oct 2007 01:13:25 +0200 Received: (qmail 57545 invoked from network); 3 Oct 2007 23:13:25 -0000 DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Received:X-YMail-OSG:In-Reply-To:References:Mime-Version:Content-Type:Message-Id:Cc:Content-Transfer-Encoding:From:Subject:Date:To:X-Mailer; b=qs3mL5GWXJDmht2GZpUsynaJ9+zNhjAGQU8YHy6FYosqaZSyOBxD5oUhOi4yfJ8ddy0K8NbI+fhZ4xQQGBBs8CUcrL2x5CfK+UpbFvdt8MwVYPKu2nbuitcfWoTDQ67lO+d+aw/E+koWI67Bg8l1apLj/zNGot4UIhTJ+skRjhg= ; Received: from unknown (HELO ?192.168.0.11?) (vincent.aravantinos@82.229.199.66 with plain) by smtp010.mail.ukl.yahoo.com with SMTP; 3 Oct 2007 23:13:25 -0000 X-YMail-OSG: vZJcVt8VM1mUrk7HzVLOdUSp.D.ICpei.79iz.HdvIfiCO.bkli0N1hwBckQZt.I6CHTsHamQw-- In-Reply-To: <1191451810.7218.86.camel@rosella.wigram> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Message-Id: <38BB2D08-E5D5-4A02-A3BF-7B0B51C2311F@yahoo.fr> Cc: Christophe Raffalli , oleg@pobox.com, caml-list@inria.fr Content-Transfer-Encoding: quoted-printable From: Vincent Aravantinos Subject: Re: [Caml-list] Unsoundness is essential Date: Thu, 4 Oct 2007 01:13:23 +0200 To: skaller X-Mailer: Apple Mail (2.752.2) X-Miltered: at discorde with ID 47042216.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 christophe:01 raffalli:01 annotations:01 bounded:01 ocaml:01 ocaml:01 cheers:01 50,:98 wrote:01 caml-list:01 exceptions:01 expressive:01 expressive:01 int:01 Le 4 oct. 07 =E0 00:50, skaller a =E9crit : > 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 =20 >> 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 =20 envisaging), the programmer will be tempted to use this "everything" =20 whereas he could achieve the same with a "bounded" language. And in =20 this case I bet the programmer won't do things that will ever be =20 "type theoretic friendly", whatever progress in type theoretics will be. To my eyes it looks like many things that appeared in other languages =20= to appeal the programmers, but that could be achieved in other (did I =20= say better ?) ways. If you allow everything, people will be tempted =20 to do anything... And any progress in computer science will never =20 catch the gap. I think it's a good thing to constrain the programmer. How many times =20= I thought "that's a pity I can't do this *as I want* in ocaml". And =20 then after having been forced to think of another way to achieve my =20 goal *within the constraints of ocaml*, I ended with something like =20 "woah, actually it's better this way!". Cheers, Vincent=