caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Gabriel Scherer <gabriel.scherer@gmail.com>
To: Oleg <oleg@okmij.org>, caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] Breaking type abstraction of modules
Date: Fri, 26 Feb 2021 17:29:01 +0100
Message-ID: <CAPFanBHqSGbSh8wiFXRShOy57ejrHyOjc6xCDm8zewqsjSFFmg@mail.gmail.com> (raw)
In-Reply-To: <20210226162856.GA5806@Melchior.localnet>

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

  reply	other threads:[~2021-02-26 16:29 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-02-26 16:28 Oleg
2021-02-26 16:29 ` Gabriel Scherer [this message]
2021-02-27 10:50   ` Oleg
2021-02-27 11:37     ` Leo White
2021-03-02  8:08       ` [Caml-list] [ANN] latest batteries release: v3.3.0 Francois Berenger

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAPFanBHqSGbSh8wiFXRShOy57ejrHyOjc6xCDm8zewqsjSFFmg@mail.gmail.com \
    --to=gabriel.scherer@gmail.com \
    --cc=caml-list@inria.fr \
    --cc=oleg@okmij.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list

This inbox may be cloned and mirrored by anyone:

	git clone --mirror http://inbox.vuxu.org/caml-list
	git clone --mirror https://inbox.ocaml.org/caml-list

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 caml-list caml-list/ http://inbox.vuxu.org/caml-list \
		caml-list@inria.fr
	public-inbox-index caml-list

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.caml-list


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git