Re: [Caml-list] Breaking type abstraction of modules

[Oleg <oleg@okmij.org>]

Gabriel Scherer wrote:

> Is this very different from exposing the GADT equality directly in the
> module interface?
>
> module A : sig
>   type t (* abstract *)
>   val reveals_abstraction : (int, t) eq (* or maybe not *)
>   val x : t
> end

I think it is different: if you are declaring reveals_abstraction
(that is, the witness of the type equality) in your _interface_, you are
effectively declaring to the users that "type t = int", no? 

Thinking about this more, I come across the following example that
better illustrates my unease. The example concerns type generativity,
and explicit promise by generative functors to create fresh,
incompatible types. It seems this promise has to come with some
conditions attached.

Assuming the same preamble with teq as before, consider the following
code

  let counter = ref 0

  module AF() : sig
    type t             (* Here, t is abstract *)
    type _ trep += AT : t trep
    val x : t
   end = struct
    type t = int        (* Here, t is concrete int *)
    type _ trep += AT : t trep
    let x = incr counter; !counter

    let () = 
     let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y -> 
       match (x,y) with 
       | (AT,AT) -> Some Refl 
       | (AT,Int) -> Some Refl      (* Since t = int, it type checks *)
       | (Int,AT) -> Some Refl
       | _ -> None 
    in teq_extend {teq=teq}
  end

Here, AF is a generative functor. The type t is defined
abstract. Hence each instantiation of AF should come with its own,
fresh and incompatible with anything else type t. (For the same of
example below, the value x is also made fresh).

Here are the two instances of the functor.

   module A1 = AF ()
   module A2 = AF ()

Indeed, the types A1.t and A2.t are different: putting A1.x and A2.x
into the same list predictably fails.

   let _ = [A1.x; A2.x]

Line 1, characters 15-19:
1 | let _ = [A1.x; A2.x];;
                   ^^^^
Error: This expression has type A2.t but an expression was expected of type
         A1.t


But now it succeeds:

   let ar = ref [A1.x]

   let _ = match (teq A1.AT Int, teq A2.AT Int) with 
            | (Some Refl,Some Refl) -> ar := A2.x :: !ar
            | _ -> assert false

   let _ = !ar
- : A1.t list = [<abstr>; <abstr>]

The list in ar really has A2.x and A1.x as elements, which we can confirm
as

   let _ = match teq A1.AT Int with
           | Some Refl -> (!ar : int list) 
           | _ -> assert false

- : int list = [2; 1]