Private type abbreviations

Learning
1

Hey all, I recently ran into this blogpost and was playing around with one of the OCaml examples. Here I’m not concerned with type classes, but rather with type checking. To rephrase a section from the blogpost, consider:

module F : sig
  type t
  val fake: int -> t
end = struct
  type t = int
  let fake n = n
end
type fake_int = F.t

type _ wrap =
  | WrapInt : int -> int wrap
  | WrapString : string -> string wrap
  | WrapAny : 'a -> 'a wrap

Now, the definition

let f : fake_int wrap -> unit = function
  | WrapAny _ -> ()

complains that the pattern matching is non-exhaustive until you add both a WrapInt _ case and a WrapString _ case.
Here it looks like the type checker can’t prove that fake_int is distinct from int or even from string, which makes sense to me, since the abstract type hides everything about its implementation.

I then learned about private type abbreviations. If we alter the signature of F as

module F : sig
  type t = private int
  val fake: int -> t
end = ...

then the pattern matching below is still non-exhaustive, but now it’s enough just to add a WrapInt _ case. This time, it looks like the definition exposes the fact that fake_int is distinct from string, so the type-checker can successfully discard the case WrapString _, but it still cannot discard the WrapInt _ case.

My question is, what’s the rationale behind that last part? Are there any undesirable consequences from allowing the type-checker to discriminate fake_int from int at the above exhaustiveness check? I’m not very familiar with how GADT pattern matching is implemented, is there any obvious problem there? Are there common patterns that this would break?

I know the types fake_int (namely t) and int are equal inside the module F – in fact the implementation of fake witnesses this. But once we’re outside, aren’t they effectively distinct types? The annotations 1 : fake_int and (fake 1) : int both fail with a similar error message Type int is not compatible with type F.t.

I’m aware a usual pattern is

type fake_int = Fake of int

where fake_int is indeed a brand-new type distinct from int (and the type-checker knows it). But for this to solve the exhaustiveness issue, we still need to expose the type constructor Fake and thus allow users to construct values directly. So I was wondering how close one could get to something like how in Haskell we can expose the type info but hide the constructor(s), even when the type is a newtype.

2

Not necessarily: the module F could expose a value

type (_, _) eq = Eq : ('a, 'a) eq
module F : sig
  (* ... *)
  val eq : (t, int) eq
end = struct
  (* ... *)
  let eq = Eq
end

then

let Eq = F.eq in
f (WrapInt 12) (* [fake_int] is equal to [int] here! *)

Cheers,
Nicolas

3

You can use private with sum and record types:

type fake_int = private Fake of int

And you can get rid of the extra indirection at runtime by annotating with [@@unboxed]:

type fake_int = private Fake of int [@@unboxed]

Cheers,
Nicolas