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=none 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 AFE32BC6C for ; Thu, 31 Jan 2008 14:48:48 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANdgoUfAXQInh2dsb2JhbACQKwEBAQgKKYEUmHE X-IronPort-AV: E=Sophos;i="4.25,285,1199660400"; d="scan'208";a="8573739" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 31 Jan 2008 14:48:48 +0100 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 m0VDmgQK015030 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 31 Jan 2008 14:48:48 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABNhoUeBrw8Eh2dsb2JhbACQKwEBAQgKKYEUmGw X-IronPort-AV: E=Sophos;i="4.25,285,1199660400"; d="scan'208";a="7472339" Received: from ext.lri.fr ([129.175.15.4]) by mail1-smtp-roc.national.inria.fr with ESMTP; 31 Jan 2008 14:48:47 +0100 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id C235AA4931; Thu, 31 Jan 2008 14:48:47 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 79HDlBJnByEF; Thu, 31 Jan 2008 14:48:47 +0100 (CET) Received: from smtp.lri.fr (vhost3-23 [129.175.3.23]) by ext.lri.fr (Postfix) with ESMTP id 9E671A492D; Thu, 31 Jan 2008 14:48:47 +0100 (CET) Received: from [129.175.4.128] (lri4-128 [129.175.4.128]) by smtp.lri.fr (Postfix) with ESMTP id 7E5CBE052B; Thu, 31 Jan 2008 14:48:47 +0100 (CET) Message-ID: <47A1D212.3010205@lri.fr> Date: Thu, 31 Jan 2008 14:50:10 +0100 From: Romain Bardou User-Agent: Thunderbird 2.0.0.6 (X11/20071022) MIME-Version: 1.0 To: Dawid Toton Cc: caml-list Subject: Re: [Caml-list] Attach an invariant to a type References: <47a1cd167921b@wp.pl> In-Reply-To: <47a1cd167921b@wp.pl> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 47A1D1BA.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lri:01 invariants:01 run-time:01 ocaml:01 camlp:01 syntax:01 semantics:01 sig:01 val:01 val:01 struct:01 translated:01 beginner's:01 ocaml:01 bug:01 Well, there is no such thing as invariants with run-time checks in OCaml, but there are some solutions: 1) use a camlp4 syntax extension I would like to highlight the fact that there would be a lot of problems to give your extension a good semantics. Your example only tackles the case where your objects appears directly in some function argument. What about, for instance, if you have a structure with a field of type "subindex" as an argument of a function? There are solutions but it's not easy. 2) (much better imo) use a module with an abstract type, such as: module Subindex: sig type t val of_int: int -> t val to_int: t -> int end = struct type t = int let of_int n = assert (n >= 10 && x <= 100); n let to_int n = n end Typing ensures that the only way one can build a value of type Subindex.t is by using the function Subindex.of_int, thus ensuring the invariant for every value of type Subindex.t thanks to the assert. (You could use some user-defined exception such as Invariant_not_verified, or simply Invalid_argument, to make it clearer instead of using assert) Romain Bardou Dawid Toton a écrit : > What should I do if I have need for the following? Does already exist > any equivalent solution? > > I'd like to write: > > type subindex = int invariant x -> (x>=10)&&(x<=100) > > let doit (a:subindex) (b:subindex) = > let result = some_operation a b in > (result:subindex) > > And it should be translated to: > > type subindex = int > let subindex_invariant x = (x>=10)&&(x<=100) > > let doit (a:subindex) (b:subindex) = > assert (subindex_invariant a); > assert (subindex_invariant b); > let result = some_operation a b in > assert (subindex_invariant result); > (result:subindex) > > Am I going right direction at all? > > ---------------------------------------------------- > Promocyjne oferty biletów lotniczych! > Praga, Rzym, Pary¿, Mediolan ju¿ od 499z³ - Kliknij: > http://klik.wp.pl/?adr=http%3A%2F%2Fsamoloty.wp.pl%2Fpromocje%2F&sid=202 > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs