[Caml-list] Breaking type abstraction of modules

[Caml-list] Breaking type abstraction of modules

[Oleg]

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.

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

[Gabriel Scherer]

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

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

[Oleg]

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]

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

[Leo White]

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

[Caml-list] [ANN] latest batteries release: v3.3.0

[Francois Berenger]

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.