Attach an invariant to a type
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Romain Bardou <Romain.Bardou@l...> 
Subject:  Re: [Camllist] Attach an invariant to a type 
Well, there is no such thing as invariants with runtime 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 userdefined 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 > > _______________________________________________ > Camllist mailing list. Subscription management: > http://yquem.inria.fr/cgibin/mailman/listinfo/camllist > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/camlbugs