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 JAA26072; Wed, 17 Jul 2002 09:33:10 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA25927 for ; Wed, 17 Jul 2002 09:33:09 +0200 (MET DST) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g6H7X7f02384 for ; Wed, 17 Jul 2002 09:33:08 +0200 (MET DST) Received: from localhost (suiren.kurims.kyoto-u.ac.jp [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id QAA06664; Wed, 17 Jul 2002 16:32:58 +0900 (JST) To: johan.baltie@wanadoo.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer) In-Reply-To: <20020717071424.M65430@wanadoo.fr> References: <20020717061954.M92611@wanadoo.fr> <20020717154649S.garrigue@kurims.kyoto-u.ac.jp> <20020717071424.M65430@wanadoo.fr> X-Mailer: Mew version 1.94.2 on Emacs 20.7 / Mule 4.0 (HANANOEN) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20020717163258S.garrigue@kurims.kyoto-u.ac.jp> Date: Wed, 17 Jul 2002 16:32:58 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) 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. > > 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 think this discussion started on efficiency considerations; my belief is that you can already already optimize a lot, without using fancy type systems. 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. Cheers, Jacques Garrigue ------------------- 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