caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Oleg <oleg@okmij.org>
To: caml-list@inria.fr
Subject: [Caml-list] Breaking type abstraction of modules
Date: Sat, 27 Feb 2021 01:28:56 +0900
Message-ID: <20210226162856.GA5806@Melchior.localnet> (raw)


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.



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

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-02-26 16:28 Oleg [this message]
2021-02-26 16:29 ` Gabriel Scherer
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=20210226162856.GA5806@Melchior.localnet \
    --to=oleg@okmij.org \
    --cc=caml-list@inria.fr \
    /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