Dear Oleg,
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
let Refl = A.reveals_abstraction in A.x + 1
On Fri, Feb 26, 2021 at 5:24 PM Oleg wrote:
>
> I wonder if the following behavior involving extensible GADTs is
> intentional. It could be useful -- on the other hand, it breaks the type
> abstraction, smuggling out the type equality that was present in the
> implementation of a module but should not be visible to the clients of
> the module. The example is fully above the board, using no magic. It
> runs on OCaml 4.11.1.
>
> Come to think of it, the example is not surprising: if we can reify
> the type equality as a value, we can certainly smuggle it out. Still
> it leaves an uneasy feeling.
>
> Incidentally, I came across the example when pondering Garrigue and
> Henry's paper submitted to the OCaml 2013 workshop.
> https://ocaml.org/meetings/ocaml/2013/proposals/runtime-types.pdf
>
> The paper mentions that runtime type representations may allow breaking
> type abstractions (p2, near the end of the first column).
> Their paper describes a compiler extension. The present example works
> in OCaml as it is, and doesn't depend on any OCaml internals.
>
> First is the preliminaries. Sorry it is a bit long. It is included to
> make the example self-contained.
>
> (* Type representation library
> A minimal version of
> http://okmij.org/ftp/ML/trep.ml
> *)
>
> type _ trep = ..
>
> type (_,_) eq = Refl : ('a,'a) eq
>
> (* The initial registry, for common data types *)
> type _ trep +=
> | Int : int trep
>
> type teq_t = {teq: 'a 'b. 'a trep -> 'b trep -> ('a,'b) eq option}
>
> let teqref : teq_t ref = ref {teq = fun x y -> None} (* default case *)
>
> (* extensible function *)
> let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y ->
> (!teqref).teq x y
>
> (* Registering an extension of teq *)
> let teq_extend : teq_t -> unit = fun {teq = ext} ->
> let {teq=teq_old} = !teqref in
> teqref := {teq = fun x y -> match ext x y with None -> teq_old x y | r
> -> r}
>
> (* Registering the initial extension *)
> let () =
> let teq_init : type a b. a trep -> b trep -> (a,b) eq option = fun x y
> ->
> match (x,y) with
> | (Int,Int) -> Some Refl
> | _ -> None
> in teq_extend {teq = teq_init}
>
>
> Now, the main problematic example
>
> module A : 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 = 1
>
> 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
>
>
> And here is the problematic behavior:
>
> # let _ = A.x + 1
>
> Line 1, characters 8-11:
> 1 | let _ = A.x + 1
> ^^^
> Error: This expression has type A.t but an expression was expected of
> type
> int
>
> That is the expected behavior: to the user of the module A, the type
> A.t is abstract. The users cannot/should not know how it is actually
> implemented.
>
> But we can still find it out
>
> # let _ = match teq A.AT Int with | Some Refl -> A.x + 1 | _ -> assert
> false
> - : int = 2
>
> and bring in the equality that t is an int, and get A.x + 1 to type
> check after all.
>
>
>