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.

[-- Attachment #1: Type: text/plain, Size: 3726 bytes --] 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 <oleg@okmij.org> 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. > > > [-- Attachment #2: Type: text/html, Size: 4967 bytes --]

```
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]
```

```
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]
>
```

Dear OCaml users, The batteries maintainers are pleased to announce the latest minor release of OCaml batteries-included: v3.3.0. Batteries is an open-source, community-maintained, extended standard library for OCaml. The latest version is available in opam. Many thanks to all the contributors for this release! This version is compatible with OCaml-4.12 and brings some minor changes. The change log follows: --- v3.3.0 (minor release) Several fixes for OCaml-4.12 #994, #992, (kit-ty-kate) Support for ocaml-multicore in the Gc module #991 (kit-ty-kate, review by Gabriel Scherer) Significant work preparing switch to dune #1025, #1024, #1023, #1022, #1021, #1020, #1019, #1017 (Gabriel Scherer, review by Francois Berenger) Remove -rectypes from BatFingerTree and simpler implementation #1012 (Gabriel Scherer) new BatEither module; available in all OCaml versions supported by batteries #1027 The implementation comes from the stdlib and is due to Gabriel Scherer. (Francois Berenger, review by Gabriel Scherer) BatList.partition_map: ('a → ('b, 'c) BatEither.t) → 'a list → 'b list * 'c list #1028 (Francois Berenger, review by Gabriel Scherer) BatSet: added several missing methods for compatibility with stdlib. The implementation of filter, map and filter_map was adapted from stdlib, authors of the original implementation are Xavier Leroy, Albin Coquereau and Gabriel Scherer #1006, #1008 (Jakob Krainz, review by Gabriel Scherer) BatSeq: compatibility with stdlib.Seq #1005, #1007 (Jakob Krainz, review by Gabriel Scherer) BatMap, BatSplay: find_first, find_first_opt, find_last, find_last_opt, to_rev_seq For compatibility with the stdlib. The implementation in BatMap was adapted from stdlib; authors of the original implementation are Albin Coquereau and Gabriel de Perthuis. #1000, #1031 (Jakob Krainz, review by Gabriel Scherer) BatArray.remove_at: int → 'a array → 'a array #996 For compatibility with BatList (Francois Berenger, review by Cedric Cellier) BatDynArray: several new functions BatDynArray now exposes almost the same functionalities as BatArray #872 (andrepd, review by Florent Monnier and Francois Berenger) BatDynArray: uniformization of exceptions and more documentation #988 (Florent Monnier, review by Francois Berenger) BatDynArray: user input checks in left, right, tail #987 (Florent Monnier, review by Francois Berenger) Fix stack overflow on Int32/64.pow with negative exponent (issue #989) #990 (Cedric Cellier, review by Francois Berenger) BatList.unfold_exn is an alias for unfold_exc. BatRefList.find_exn is an alias for find_exc. #978 (Cedric Cellier, review by Francois Berenger) --- Happy hacking, The batteries team.