Re: [Caml-list] Attach an invariant to a type

[Romain Bardou <Romain.Bardou@lri.fr>]

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