Attach an invariant to a type

Attach an invariant to a type

[Dawid Toton]

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

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

[Romain Bardou]

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

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

[David Teller]

Actually, OCaml contains something slighly simpler than this of_int /
to_int mechanism: private types.


On Thu, 2008-01-31 at 14:50 +0100, Romain Bardou wrote:

> 2) (much better imo) use a module with an abstract type, such as:

-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act
brings liquidations. 

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

[Romain Bardou]

Wow, how could I forget about private types.

However, you still need the of_int function.

module Subindex: sig
   type t = private int
   val make: int -> t
end = struct
   type t = int
   let make n =
     assert (n >= 10 && x <= 100);
     n
end

	Romain Bardou

David Teller a écrit :
> Actually, OCaml contains something slighly simpler than this of_int /
> to_int mechanism: private types.
> 
> 
> On Thu, 2008-01-31 at 14:50 +0100, Romain Bardou wrote:
> 
>> 2) (much better imo) use a module with an abstract type, such as:
> 

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

[Hezekiah M. Carty]

On Jan 31, 2008 1:13 PM, Romain Bardou <Romain.Bardou@lri.fr> wrote:
> Wow, how could I forget about private types.
>
> However, you still need the of_int function.
>
> module Subindex: sig
>    type t = private int
>    val make: int -> t
> end = struct
>    type t = int
>    let make n =
>      assert (n >= 10 && x <= 100);
>      n
> end
>

This code does not work for me.  I get a "This fixed type is not an
object or variant" error on the "type t = private int" line.  From the
manual it looks like you would have to use something like this:

type t = private Index of int

to take advantage of private types.  Am I missing something?

Hez

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

[Stéphane Lescuyer]

On Jan 31, 2008 8:13 PM, Hezekiah M. Carty <hcarty@atmos.umd.edu> wrote:
>
> This code does not work for me.  I get a "This fixed type is not an
> object or variant" error on the "type t = private int" line.  From the
> manual it looks like you would have to use something like this:
>
> type t = private Index of int
>
> to take advantage of private types.  Am I missing something?
>

No you're not :) as far as I know, a private type can only be a record
or a variant.
It prevents one from constructing values of this type, but still
allows pattern-matching
on these values.

I guess that making types like "int" private would require the system
(among other things) to decide whether you're using a given integer as
a Subindex.t or not. At first glance, it seems it is a harder problem
than just forbidding the construction of any value of a given type.
Just my 0.02€ :-)

Stéphane L.

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

[Dawid Toton]

> I guess that making types like "int" private would require the system
> (among other things) to decide whether you're using a given integer as
> a Subindex.t or not.

Suppose we have "type t = private int" in module Subindex.

Is the following construct legal: let (a:Subindex.t) = 2 ?
It shouldn't be - to prevent me from constructing values of this type. 
So I couldn't "use given integer as Subinddex.t".

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

[Romain Bardou]

>> to take advantage of private types.  Am I missing something?
>>
> 
> No you're not :) as far as I know, a private type can only be a record
> or a variant.

Yes, sorry, I should have tested my code ><

-- 
Romain Bardou

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

[Edgar Friendly]

Dawid Toton wrote:
>> I guess that making types like "int" private would require the system
>> (among other things) to decide whether you're using a given integer as
>> a Subindex.t or not.
> 
> Suppose we have "type t = private int" in module Subindex.
> 
> Is the following construct legal: let (a:Subindex.t) = 2 ?
> It shouldn't be - to prevent me from constructing values of this type.
> So I couldn't "use given integer as Subinddex.t".
> 
type t = private int isn't legal.  Most types get completely erased
during compilation, but records and variants have code generated by the
compiler based off their type declaration to construct a value of that
type.  A plain int doesn't have this compiler-generated constructor, so
it can't be private in this way.

That said, I'd appreciate a simple system to do the kind of checking you
want at the site of an explicit typecast.

E

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

[Keiko Nakata]

Hello.

> type t = private int isn't legal.  Most types get completely erased
> during compilation, but records and variants have code generated by the
> compiler based off their type declaration to construct a value of that
> type.  A plain int doesn't have this compiler-generated constructor, so
> it can't be private in this way.
> 
> That said, I'd appreciate a simple system to do the kind of checking you
> want at the site of an explicit typecast.

Maybe a previous discussion on the list is interesting to you.
Among this active discussion, the following post by Pierre Weis
looks good new to you.

http://caml.inria.fr/pub/ml-archives/caml-list/2007/11/76aa857050497ee6cf62db65eadd567a.en.html

With best regards,
Keiko

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

[Stéphane Glondu]

Stéphane Lescuyer a écrit :
> No you're not :) as far as I know, a private type can only be a record
> or a variant.

Xavier mentioned the possibility to extend private types to any type:

  http://gallium.inria.fr/~xleroy/talks/cug2008.pdf (page 5)

So maybe Romain's code will work in a near future :-)


My 2 cents.

-- 
Stéphane