Private and type constraints

Private and type constraints

[Dario Teixeira]

Hi,

With 'private', you can make sure that users of a module can only use
constructors to create values, while at the same type maintaining the
ability to pattern-match (which abstracting the type makes impossible).
With 3.10, this can also be done with polymorphic variants:

module Foobar:
sig
    type foo_t = [ `A ]
    type bar_t = [ `B ]
    type foobar_t = [ foo_t | bar_t ]
    type t = private [< foobar_t ]

    val make_a: unit -> t
    val make_b: unit -> t
end =
struct
    type foo_t = [ `A ]
    type bar_t = [ `B ]
    type foobar_t = [ foo_t | bar_t ]
    type t = foobar_t

    let make_a () = `A
    let make_b () = `B
end


# open Foobar;;
# let ola = make_a ();;
val ola : Foobar.t = `A
# match ola with `A -> true | `B -> false;;
- : bool = true
# let ola2 : Foobar.t = `A;;
Characters 22-24:
  let ola2 : Foobar.t = `A;;
                        ^^
Error: This expression has type [> `A ] but is here used with type Foobar.t
       Types for tag `A are incompatible


Now, I want to do the same for a type 't' that is declared using a type constraint.
There are however two problems: first, the code below is accepted by the toplevel,
but not by the ocamlc/ocamlopt compilers (I'm running version 3.11+dev15); second,
while as expected it prevents the creation of Foobar2.t values without using the
constructor functions, pattern-matching is unfortunately also disallowed.

module Foobar2:
sig
    type foo_t = [ `A ]
    type bar_t = [ `B ]
    type foobar_t = [ foo_t | bar_t ]
    type 'a t = private 'a constraint 'a = [< foobar_t ]

    val make_a: unit -> foo_t t
    val make_b: unit -> bar_t t
end =
struct
    type foo_t = [ `A ]
    type bar_t = [ `B ]
    type foobar_t = [ foo_t | bar_t ]
    type 'a t = 'a constraint 'a = [< foobar_t ]

    let make_a () = `A
    let make_b () = `B
end


# open Foobar2;;
# let ola = make_a ();;
val ola : Foobar2.foo_t Foobar2.t = `A
# match ola with `A -> true;;
Characters 15-17:
  match ola with `A -> true;;
                 ^^
Error: This pattern matches values of type [< `A ]
       but is here used to match values of type Foobar2.foo_t Foobar2.t
# let ola2 : Foobar2.foo_t Foobar2.t = `A;;
Characters 37-39:
  let ola2 : Foobar2.foo_t Foobar2.t = `A;;
                                       ^^
Error: This expression has type [> `A ] but is here used with type
         Foobar2.foo_t Foobar2.t


This is the error produced by the compiler:

Error: The implementation constraint.ml
       does not match the interface (inferred signature):
       Modules do not match:
         sig
           type foo_t = [ `A ]
           type bar_t = [ `B ]
           type foobar_t = [ `A | `B ]
           type 'a t = 'a Foobar2.t constraint 'a = [< foobar_t ]
           val make_a : unit -> foo_t t
           val make_b : unit -> bar_t t
         end
       is not included in
         sig
           type foo_t = [ `A ]
           type bar_t = [ `B ]
           type foobar_t = [ `A | `B ]
           type 'a t = private 'a constraint 'a = [< foobar_t ]
           val make_a : unit -> foo_t t
           val make_b : unit -> bar_t t
         end
       Type declarations do not match:
         type 'a t = 'a Foobar2.t constraint 'a = [< foobar_t ]
       is not included in
         type 'a t = private 'a constraint 'a = [< foobar_t ]


Any idea on what is going on?  Also, is it at all possible to achieve
the 'private' semantics I am looking for with types declared using
a constraint?  I know I can do it by boxing the type inside a dummy
union or a record, but I would like to avoid that hassle if possible.

Thanks for your time + best regards,
Dario Teixeira



      __________________________________________________________
Not happy with your email address?.
Get the one you really want - millions of new email addresses available now at Yahoo! http://uk.docs.yahoo.com/ymail/new.html

Re: [Caml-list] Private and type constraints

[Dario Teixeira]

Hi,

I just noted that there's already a ticket (#4580) related to this problem:
http://caml.inria.fr/mantis/view.php?id=4580

My doubts are a) whether the code below will be correct for 3.11 final;
and b) whether its semantics are equivalent to other uses of 'private',
namely that external pattern-matching on Foobar.t values is allowed,
but the construction of new values must be done through the constructor
functions.  Any thoughts?

Thanks in advance for your time!
Cheers,
Dario Teixeira
 
module Foobar:
sig
  type foo_t= [ `A ]
  type bar_t = [ `B ]
  type foobar_t = [ foo_t | bar_t ]
  type 'a t = private 'a constraint 'a = [< foobar_t ]
 
  val make_a: unit -> foo_t t
  val make_b: unit -> bar_t t
end =
struct
  type foo_t = [ `A ]
  type bar_t = [ `B ]
  type foobar_t = [ foo_t | bar_t ]
  type 'a t = 'a constraint 'a = [< foobar_t ]

  let make_a () = `A
  let make_b () = `B
end



      __________________________________________________________
Not happy with your email address?.
Get the one you really want - millions of new email addresses available now at Yahoo! http://uk.docs.yahoo.com/ymail/new.html