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

["Leo White" <leo@lpw25.net>]

Hi Oleg,

I don't really understand your unease here. Firstly, this isn't some unexpected aspect of extensible variants, it is the main reason that I proposed adding them to the language. Secondly, you can easily create similar behaviour without extensible variants. For example, here we do the same thing without extensibility (code not actually tested or even type-checked):

type (_, _) eq = Refl : ('a, 'b) eq

module Rep : sig
  type 'a t
  val int : int t
  val string : string t
  val destruct : 'a t -> 'b t -> ('a, 'b) eq option
end = struct
  type 'a rep =
    | Int : int rep
    | String : int rep
  let int = Int
  let string = String
  let destruct (type a b) (a : a t) (b : b t) =
    match a, b with
    | Int, Int -> Some Refl
    | String, String -> Some Refl
    | _, _ -> None
end

let counter = ref 0
 
module AF() : sig
  type t             (* Here, t is abstract *)
  val rep : t Rep.t
  val x : t
end = struct
  type t = int        (* Here, t is concrete int *)
  let rep = Rep.int
  let x = incr counter; !counter
end

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

let ar = ref [A1.x]
 
let _ =
   match Rep.destruct A1.rep A2.rep with 
    | Some Refl -> ar := A2.x :: !ar
    | _ -> assert false

Extensible variants make these kinds of type representations much more useful, but they don't change the nature of what you can do.

Regards,

Leo

On Sat, 27 Feb 2021, at 10:50 AM, Oleg wrote:
> 
> 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]
>