Private types

Private types

[David Allsopp]

I'm trying to play with the new private type abbreviations in OCaml
3.11+beta1

If I write:

module type S =
sig
  type t = private int
  val create : int -> t
end;;

module M : S =
struct
  type t = int
  let create x = x
end;;

let x = M.create 0;;

Shouldn't I now be able to say:

string_of_int x;;

But I get a type error... I'm struggling to see what difference the private
declaration has made, therefore.

I thought that the point of private types was that you could deconstruct
them... so values of type M.t are valid wherever an int is used but not the
converse.

Or have I missed something? <prepares to be embarrassed...>


David

Re: [Caml-list] Private types

[Daniel Bünzli]

Le 30 oct. 08 à 21:18, David Allsopp a écrit :

> Shouldn't I now be able to say:
>
> string_of_int x;;

I don't think so. According to the manual [1] the only thing you can  
do on private types is pattern match or project their fields. I  
doesn't mean your type can be substituted by int.

Daniel

[1] http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#htoc99

RE: [Caml-list] Private types

[David Allsopp]

Daniel Bünzli wrote:
> Le 30 oct. 08 à 21:18, David Allsopp a écrit :
>
> > Shouldn't I now be able to say:
> >
> > string_of_int x;;
>
> I don't think so. According to the manual [1] the only thing you can  
> do on private types is pattern match or project their fields. I  
> doesn't mean your type can be substituted by int.

Strictly speaking the manual says that you can't construct values directly
(you can construct other values which contain private types, though, so it's
not limited to pattern matching or projection).

>
> [1] http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#htoc99

Thanks for this - although it's a link to an OCaml 3.10 manual so not
applicable here it did point me to the correct chapter in the OCaml 3.11
manual (I'd been looking in Part I of the manual and given up). What I
should have written is

string_of_int (x :> int)

Though that does make me wonder why the coercion is mandatory. What happens
if I *want* to allow the use of M.t values as though they were ints and only
want to guarantee that they come from a specific sub-set of the integers
(I'm thinking of database row IDs which is what I want to use them for)?
Assuming that the type abbreviation doesn't contain type-variables, would
there be anything theoretically preventing the inclusion of two keywords:

type t = private int      (* can be used as though it were an int  *)
type t = very_private int (* requires a coercion to be used an int *)

Or are there some very obvious programming gotchas that I'm missing if the
need to write the coercion were relaxed? The important point to me would
seem to be that if I say:

x + 1

then I get the *int* 1 and not the *M.t* value 1. As it stands, I can't see
a huge amount of difference, given that you have to write the coercion
everywhere, between a fully abstract type and a function M.getValue : t ->
int and a private int type.

(I'm assuming that if M.getValue is defined as %identity then the compiler
would optimise out the calls to it... of course if that isn't the case than
private ints are already one stage better!)

And one final thought - given that you can't assign to mutable members of
private record types, isn't a bit strange that you can change the contents
of private string values? Wouldn't having type t = private string where
character access is not possible give some people the immutable strings
they've been asking for in the past?


David

Re: [Caml-list] Private types

[Jacques Garrigue]

From: "David Allsopp" <dra-news@metastack.com>

> Thanks for this - although it's a link to an OCaml 3.10 manual so not
> applicable here it did point me to the correct chapter in the OCaml 3.11
> manual (I'd been looking in Part I of the manual and given up). What I
> should have written is
> 
> string_of_int (x :> int)
> 
> Though that does make me wonder why the coercion is mandatory. What happens
> if I *want* to allow the use of M.t values as though they were ints and only
> want to guarantee that they come from a specific sub-set of the integers
> (I'm thinking of database row IDs which is what I want to use them for)?
> Assuming that the type abbreviation doesn't contain type-variables, would
> there be anything theoretically preventing the inclusion of two keywords:
> 
> type t = private int      (* can be used as though it were an int  *)
> type t = very_private int (* requires a coercion to be used an int *)

Explicit coercions in ocaml are completely unrelated to casts in C or
Java, in that they only allow upcast (cast to a supertype). They are
also completely erasable: they do not produce any code after type
checking. So they are not there for any soundness reason, but just for
type inference purposes. There would be no point at all in having two
constructs: if the 1st one were possible, we wouldn't need the second.

As for type inference, (x :> int) is already an abbreviated form of
(x : t :> int), that only works if x is "known" to be of type t.
Since ocaml type inference does not include subtyping, there is no way
to do without coercions. To explain this, you should just see how the
type checker handles
     string_of_int x
It fetches the type of the string_of_int, int -> string, fetches the
type of x, which is t, and tries to unify int and t.
Since there is no direction in unification, this can only fail, as int
and t are not equivalent, just related through subtyping.

Your intuition is correct that it would theoretically be possible to
try subtyping in place of unification in some cases. The trouble is
that thoses cases are not easy to specify (so that it would be hard
for the programmer to known when he can remove a coercion), and that
subtyping is potentially very costly (structural subtyping is much
harder to check than the nominal subtyping you have in Java.)
So the current approach is to completely separate subtyping and type
inference, and require coercions everywhere subtyping is needed.

You can also compare that to the situation between int and float.
For most uses, int can be viewed as a subtype of float. However ocaml
separates the two, and requires coercion functions whenever you want
to use an int as a float.

Cheers,

Jacques Garrigue

Re: [Caml-list] Private types

[Dario Teixeira]

Hi,

> Your intuition is correct that it would theoretically be possible to
> try subtyping in place of unification in some cases. The trouble is
> that thoses cases are not easy to specify (so that it would be hard
> for the programmer to known when he can remove a coercion), and that
> subtyping is potentially very costly (structural subtyping is much
> harder to check than the nominal subtyping you have in Java.)


Thanks for the explanation, Jacques.  If I understand correctly, by requiring
subtyping relations to be explicitly coerced, the "giant system of equations"
behind unification can be simplified because it doesn't need to worry about
all possible subtyping relations.  So in a sense this is also a matter of
computational tractability, right?

I have also been playing with 3.11's private types, and I would like to
share a problem I've come across.  Suppose I have a Foobar module defined
as follows (note the use of a type constraint):


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

	val make_a: unit -> foo_t t
	val make_b: unit -> bar_t t
	val is_foo: [< foobar_t] t -> bool
	val is_bar: [< foobar_t] t -> bool
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
	let is_foo = function `A -> true | `B -> false
	let is_bar = function `B -> true | `A -> false
end


Suppose also that I want to define a "is_foo" function in an external module.
This function only needs to pattern-match on Foobar.t values.  The following
code will work:

module Mymod:
sig
	open Foobar

	val is_foo2: [< foobar_t] t -> bool
end =
struct
	let is_foo2 = function `A -> true | `B -> false
end


But now consider that I want to enforce the creation of Foobar.t values only
via Foobar's constructor functions, but I would like to keep the possibility of
external modules to pattern-match on Foobar.t values.  In other words, change
Foobar but don't break Mymod.  The immediate (naïve) solution is to make
use of private types, thus changing the signature of Foobar to the following:


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
	val is_foo: [< foobar_t] t -> bool
	val is_bar: [< foobar_t] t -> bool
end = (...)


But this will break Mymod.  The compile will complain with the following error:

      Values do not match:
         val is_foo2 : [< `A | `B ] -> bool
       is not included in
         val is_foo2 : [< Foobar.foobar_t ] Foobar.t -> bool

Any ideas on how can I get around this problem?

Thanks!
Cheers,
Dario Teixeira

Re: [Caml-list] Private types

[Jacques Garrigue]

Dear Dario,

Since you use a private abbreviation, extraction from the private type
must be explicit before you can do anything on its representation.
So the solution is simple enough:

module Mymod =
  struct
    let is_foo2 x =
      match (x : _ Foobar.t :> [> ]) with `A -> true | `B -> false
  end

The [> ] as target type just says that you expect a polymorphic
variant, which is incompatible with Foobar.t, and triggers its
expansion.

If you want to avoid this explicit coercion, you must use a private
row type in place of a private abbreviation. However, you loose the
ability to distinguish between values created by make_a and make_b at
the type level.

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
  val is_foo: t -> bool
  val is_bar: t -> bool
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
  let is_foo = function `A -> true | `B -> false
  let is_bar = function `B -> true | `A -> false
end

You may recover this distinction by adding an extra parameter to t,
just as in your original code.

  type 'a t = private [< foobar_t]

but since you won't be able to relate it directly to the expansion of
the type (the row variable is quantified at the module level, so you
cannot capture it with 'a), you would have to recover it by hand.

Jacques Garrigue

> I have also been playing with 3.11's private types, and I would like to
> share a problem I've come across.  Suppose I have a Foobar module defined
> as follows (note the use of a type constraint):
> 
> 
> module Foobar:
> sig
> 	type foo_t = [ `A ]
> 	type bar_t = [ `B ]
> 	type foobar_t = [ foo_t | bar_t ]
> 	type 'a t = 'a constraint 'a = [< foobar_t ]
> 
> 	val make_a: unit -> foo_t t
> 	val make_b: unit -> bar_t t
> 	val is_foo: [< foobar_t] t -> bool
> 	val is_bar: [< foobar_t] t -> bool
> 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
> 	let is_foo = function `A -> true | `B -> false
> 	let is_bar = function `B -> true | `A -> false
> end
> 
> 
> Suppose also that I want to define a "is_foo" function in an external module.
> This function only needs to pattern-match on Foobar.t values.  The following
> code will work:
> 
> module Mymod:
> sig
> 	open Foobar
> 
> 	val is_foo2: [< foobar_t] t -> bool
> end =
> struct
> 	let is_foo2 = function `A -> true | `B -> false
> end
> 
> 
> But now consider that I want to enforce the creation of Foobar.t values only
> via Foobar's constructor functions, but I would like to keep the possibility of
> external modules to pattern-match on Foobar.t values.  In other words, change
> Foobar but don't break Mymod.  The immediate (naïve) solution is to make
> use of private types, thus changing the signature of Foobar to the following:
> 
> 
> 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
> 	val is_foo: [< foobar_t] t -> bool
> 	val is_bar: [< foobar_t] t -> bool
> end = (...)
> 
> 
> But this will break Mymod.  The compile will complain with the following error:
> 
>       Values do not match:
>          val is_foo2 : [< `A | `B ] -> bool
>        is not included in
>          val is_foo2 : [< Foobar.foobar_t ] Foobar.t -> bool
> 
> Any ideas on how can I get around this problem?
> 
> Thanks!
> Cheers,
> Dario Teixeira

Re: [Caml-list] Private types

[Edgar Friendly]

Jacques Garrigue wrote:

> Your intuition is correct that it would theoretically be possible to
> try subtyping in place of unification in some cases. The trouble is
> that thoses cases are not easy to specify (so that it would be hard
> for the programmer to known when he can remove a coercion), 

Does the compiler really get any information from an explicit cast that
it can't figure out already?  I can't come up with any example.

> and that
> subtyping is potentially very costly (structural subtyping is much
> harder to check than the nominal subtyping you have in Java.)

As the compiler needs to check that explicit casts are valid, I don't
see any performance difference between explicit and implicit subtype casts.

> So the current approach is to completely separate subtyping and type
> inference, and require coercions everywhere subtyping is needed.
> 
Would it be particularly difficult to, in the cases where type [x] is
found but type [y] is expected, to try a (foo : x :> y) cast?

> You can also compare that to the situation between int and float.
> For most uses, int can be viewed as a subtype of float. However ocaml
> separates the two, and requires coercion functions whenever you want
> to use an int as a float.
> 
Code isn't produced by a :> cast.  As the internal representation of int
and float differs, a coercion function isn't required.  The internal
representation of [private int] and [int] is the same, not to mention
one is exactly the [private] of the other.

> Cheers,
> 
> Jacques Garrigue

Merci,
E.

RE: [Caml-list] Private types

[David Allsopp]

Edgar Friendly wrote:
> Jacques Garrigue wrote:
>
> > Your intuition is correct that it would theoretically be possible to
> > try subtyping in place of unification in some cases. The trouble is
> > that thoses cases are not easy to specify (so that it would be hard
> > for the programmer to known when he can remove a coercion), 
>
> Does the compiler really get any information from an explicit cast that
> it can't figure out already?  I can't come up with any example.

Polymorphic variants. Consider:

type t = [ `A of int ]

let f (x : t) =
  let `A n = x
  in
    if n mod 2 = 0
    then (x : t :> [> t ])
    else `B (2 * n)

Without the full coercion for x you'll get a type error because the type
checker infers that the type of the [if] expression is [t] from the [then]
branch and then fails to unify [> `B of int ] with [t] unless the type of
[x] is first coerced to [> t ]. If the compiler were to try (x : t : [> t ])
in all those instances I think that would render polymorphic variants pretty
unusable ... the type checker needs to know that you meant to do that or
everything will unify!

> > So the current approach is to completely separate subtyping and type
> > inference, and require coercions everywhere subtyping is needed.
> > 
> Would it be particularly difficult to, in the cases where type [x] is
> found but type [y] is expected, to try a (foo : x :> y) cast?

+1! With reference my previous comment that "the type checker needs to know
if you meant that", there's still the option of using fully abstract types
if you wanted to avoid this kind of automatic coercion and have, say,
positive integers totally distinct from all integers without an explicit
cast.

All said, I do see Jacques point of wanting to keep coercion and type
inference totally separate... though perhaps if coercions were only tried
during unification if at least one of the types in question is private that
would maintain a certain level of predictability about when they're used
automatically?


David

Re: [Caml-list] Private types

[Edgar Friendly]

David Allsopp wrote:

> Without the full coercion for x you'll get a type error because the type
> checker infers that the type of the [if] expression is [t] from the [then]
> branch and then fails to unify [> `B of int ] with [t] unless the type of
> [x] is first coerced to [> t ]. If the compiler were to try (x : t : [> t ])
> in all those instances I think that would render polymorphic variants pretty
> unusable ... the type checker needs to know that you meant to do that or
> everything will unify!
> 
Okay, you claim we shouldn't automatically open polymorphic variants.  I
don't see why auto->ing polymorphic types is really a problem.  If the
later code (receiving the returned value) can't handle the [> ] type,
that type error will stop things (although it won't point out where the
[> ] came from).  This seems one case where the compiler can easily DWIM
the correct result.

>> Would it be particularly difficult to, in the cases where type [x] is
>> found but type [y] is expected, to try a (foo : x :> y) cast?
> 
> +1! With reference my previous comment that "the type checker needs to know
> if you meant that", there's still the option of using fully abstract types
> if you wanted to avoid this kind of automatic coercion and have, say,
> positive integers totally distinct from all integers without an explicit
> cast.
> 
Actually, I do see the use of two kinds of derived types:
type positive = private int ( auto-coerced to int )
type category_id = new int (not auto-coerced to int - math not allowed)

I assume there's some efficiency benefit to exposing the underlying type
of category_id, if not then abstract types will quite suffice.

> All said, I do see Jacques point of wanting to keep coercion and type
> inference totally separate... though perhaps if coercions were only tried
> during unification if at least one of the types in question is private that
> would maintain a certain level of predictability about when they're used
> automatically?
> 
> 
> David
> 
I'm happy moving down this slope of the compiler doing more of the work.
 Hopefully it's slippery, so it'll end up doing lots of work for me.

E.

RE: [Caml-list] Private types

[David Allsopp]

Edgar Friendly wrote:
> David Allsopp wrote:
>
> > Without the full coercion for x you'll get a type error because the type
> > checker infers that the type of the [if] expression is [t] from the
> > [then] branch and then fails to unify [> `B of int ] with [t] unless the
> > type of [x] is first coerced to [> t ]. If the compiler were to try (x :
> > t : [> t ]) in all those instances I think that would render polymorphic
> > variants pretty unusable ... the type checker needs to know that you
> > meant to do that or everything will unify!
> 
> Okay, you claim we shouldn't automatically open polymorphic variants.  I
> don't see why auto->ing polymorphic types is really a problem.  If the
> later code (receiving the returned value) can't handle the [> ] type,
> that type error will stop things (although it won't point out where the
> [> ] came from).  This seems one case where the compiler can easily DWIM
> the correct result.

I agree that the error will still show up somewhere if there is an error -
but remember that a closed polymorphic variant type required an annotation
in the first place (in this case, the type [t] and the explicit type
annotation to use it)... so having made the explicit choice to declare the
type closed (which you either do to declare module interfaces or to try to
trap errors) the last thing (I'd say!) you want is the compiler trying to
open them back up on every unification failure!


David

Re: [Caml-list] Private types

[Edgar Friendly]

David Allsopp wrote:
> I agree that the error will still show up somewhere if there is an error -
> but remember that a closed polymorphic variant type required an annotation
> in the first place (in this case, the type [t] and the explicit type
> annotation to use it)... so having made the explicit choice to declare the
> type closed (which you either do to declare module interfaces or to try to
> trap errors) the last thing (I'd say!) you want is the compiler trying to
> open them back up on every unification failure!
> 
> 
> David
> 
You only declared the argument to the function as closed.  This doesn't
mean that the return type of the function must be that closed type.  If
you declared the function as returning type t, then the auto-open would
run into a type roadblock before it left the function.  But given your
initial code, the intent of the programmer seems clear in wanting a
different return type.

E.

Re: [Caml-list] Private types

[Jacques Garrigue]

From: Edgar Friendly <thelema314@gmail.com>

> > So the current approach is to completely separate subtyping and type
> > inference, and require coercions everywhere subtyping is needed.
> > 
> Would it be particularly difficult to, in the cases where type [x] is
> found but type [y] is expected, to try a (foo : x :> y) cast?

If we limit ourselves to the case where both [x] and [y] contrain no
type variables, this si not particularly difficult. However whether
they will contain type variables or not depends heavily on how the
type inference algorithm proceeds.

If they contain type variables, then the situation becomes much more
muddled, as these type variables may get instantiated by the subtyping
check, and not necessarily as expected. So typing becomes rather
unpredictable...

> > You can also compare that to the situation between int and float.
> > For most uses, int can be viewed as a subtype of float. However ocaml
> > separates the two, and requires coercion functions whenever you want
> > to use an int as a float.
> > 
> Code isn't produced by a :> cast.  As the internal representation of int
> and float differs, a coercion function isn't required.  The internal
> representation of [private int] and [int] is the same, not to mention
> one is exactly the [private] of the other.

This was not intended as a complete comparison :-)
However, since the coercion function is canonical, I don't think that
this difference matters much here.

     Jacques Garrigue

Re: [Caml-list] Private types

[Edgar Friendly]

Jacques Garrigue wrote:
> If we limit ourselves to the case where both [x] and [y] contrain no
> type variables, this si not particularly difficult. However whether
> they will contain type variables or not depends heavily on how the
> type inference algorithm proceeds.
> 
> If they contain type variables, then the situation becomes much more
> muddled, as these type variables may get instantiated by the subtyping
> check, and not necessarily as expected. So typing becomes rather
> unpredictable...
> 
>      Jacques Garrigue

We've reached the end of my intuition - I admit I get stuck thinking
about automatic casts with type variables.  I can only point out that
for an appropriate definition of "expected" (as in "found type x but
expected type y"), one will always get the expected type.  :)

If the line in the sand has to be drawn somewhere (between
auto-subtyping and not), this seems a simple and effective place to do so.

E.

Re: Private types

[Rémi Vanicat]

Edgar Friendly <thelema314@gmail.com> writes:

> Jacques Garrigue wrote:
>
>> Your intuition is correct that it would theoretically be possible to
>> try subtyping in place of unification in some cases. The trouble is
>> that thoses cases are not easy to specify (so that it would be hard
>> for the programmer to known when he can remove a coercion), 
>
> Does the compiler really get any information from an explicit cast that
> it can't figure out already?  I can't come up with any example.

you mean as in the following function ? 
let f x = (x : t :> t')


-- 
Rémi Vanicat

Re: [Caml-list] Re: Private types

[Edgar Friendly]

Rémi Vanicat wrote:
> Edgar Friendly <thelema314@gmail.com> writes:
> 
>> Does the compiler really get any information from an explicit cast that
>> it can't figure out already?  I can't come up with any example.
> 
> you mean as in the following function ? 
> let f x = (x : t :> t')
> 
Well, yes and no.  That function in a vacuum doesn't have enough
information to infer types t and t', but within a larger program, if it
gets used in a manner other than ('a -> 'a), the cast should be obvious, no?

E.

Re: [Caml-list] Private types

[Jérémie Dimino]

"David Allsopp" <dra-news@metastack.com> writes:

> I thought that the point of private types was that you could
> deconstruct them... so values of type M.t are valid wherever an int
> is used but not the converse.

It should probably be ok for immutable data but not for mutable
ones. One example is using String.set on a private string.

Jérémie