From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA26550; Wed, 17 Jul 2002 09:53:47 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA26518 for ; Wed, 17 Jul 2002 09:53:46 +0200 (MET DST) Received: from mel-rto4.wanadoo.fr (smtp-out-4.wanadoo.fr [193.252.19.23]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g6H7rjX08684 for ; Wed, 17 Jul 2002 09:53:45 +0200 (MET DST) Received: from mel-rta10.wanadoo.fr (193.252.19.193) by mel-rto4.wanadoo.fr (6.5.007) id 3D18589F00BF1007; Wed, 17 Jul 2002 09:53:07 +0200 Received: from AlphaSystem.dnsalias.net (80.11.74.121) by mel-rta10.wanadoo.fr (6.5.007) id 3D2A79160042ECF2; Wed, 17 Jul 2002 09:53:07 +0200 Received: from localhost ([127.0.0.1] helo=alphasystem.dnsalias.net) by AlphaSystem.dnsalias.net with esmtp (Exim 3.36 #1 (Debian)) id 17UjcQ-000MHQ-00; Wed, 17 Jul 2002 09:53:06 +0200 From: "Johan Baltié" To: Jacques Garrigue CC: caml-list@inria.fr Subject: Re: [Caml-list] Sub{range,type} (was: Statically detecting arrays bound exceptions ??) Date: Wed, 17 Jul 2002 08:53:06 +0100 Message-Id: <20020717075306.M43089@wanadoo.fr> In-Reply-To: <20020717163258S.garrigue@kurims.kyoto-u.ac.jp> References: <20020717061954.M92611@wanadoo.fr> <20020717154649S.garrigue@kurims.kyoto-u.ac.jp> <20020717071424.M65430@wanadoo.fr> <20020717163258S.garrigue@kurims.kyoto-u.ac.jp> X-Mailer: Open WebMail 1.61 20020204 X-OriginatingIP: 192.6.2.192 (baltie_j) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > From: "Johan Baltié" > > > > In the second case, you should propagate the information from the > > > assertion to the loop bound, and additionally treat swap as if it were > > > inlined (we know it is its only call context). > > > > No it's not such a mess. A subrange is a type. As ocaml is a bit > > strong on is types it solves itself the problem > > OK, I should have been clearer about my basic assumption: I was > talking about what you can do _without_ modifying the typing. > Modifying the typing is a mess: if your bounds are no longer integers, > then how can you convert between them and integers, back and forth. > You could use subtyping in one direction, but there is no implicit > subtyping in ocaml, as this would badly break type inference. *sigh* :,( I was dreaming of that kind of stuff. But I do not see why type inference reach an end with subtyping. Can you elaborate on this ? > > > And it's fragile: > > > if you move "swap" out of the function, then it might be used on any > > > array, and you have to do the bound check. > > > > If you move swap out of the function, in another one using another array, the > > type will change and a warning/error/check will occur if the types > > are incompatible. > > No, I was just saying moving swap to the toplevel: > let swap arr i = .... > > Supposing you use the original plain type, you are in trouble. > > But it looks like you're just asking for dependent types, no less... I did not know this name, and after a quick browse I can answer: "Yes" :) > I think this discussion started on efficiency considerations; > my belief is that you can already already optimize a lot, without > using fancy type systems. Ok, I left the previous thread, cause I'm getting totally of topic. > Such type systems are not only hard to > implement (and mix with an existing type system); while they > certainly take bugs, they also get in your way when you get out of > their small understanding. With my new and small understanding of dependent type, it seems to me that Ada types look a lot like this. It seems to add power to the type checker, so why would this be a bad thing ? Did I miss something ? The only problem that I see is that if you consider list type dependent of size, this kind of type cannot staticaly determined (is it the point that break type inference ?). Ciao Jo ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners