Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Attach an invariant to a type
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Romain Bardou <Romain.Bardou@l...>
Subject: Re: [Caml-list] Attach an invariant to a type
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);
   let to_int n = n

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:
> _______________________________________________
> Caml-list mailing list. Subscription management:
> Archives:
> Beginner's list:
> Bug reports: