From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 4579EE1D37 for ; Fri, 26 Feb 2021 17:29:40 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk1-f180.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.222.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.222.180 as permitted sender) identity=mailfrom; client-ip=209.85.222.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qk1-f180.google.com) identity=helo; client-ip=209.85.222.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-qk1-f180.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AwoY8qhZYdDAiZ1Y8DBcIU13/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZrs+/bnLW6fgltlLVR4KTs6sC17OH9fG5EjJYqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba52IRmsqQjdq8YajIp+Jq0s1hbHv3xEdv?= =?us-ascii?q?hMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTD?= =?us-ascii?q?QhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlS?= =?us-ascii?q?EKPCM7/m7KkMx9lK1UoByjqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6x?= =?us-ascii?q?aZYEAeobPeZfqonwv1oAogGlCgm2BePg1DtIjWLr06Im0+QuDxvG0xI6H9kTt3?= =?us-ascii?q?nUo8/6O7wIUeC00qbIyS/Pb+hK1jf99ofIaA4uoeuXULJ/dMre00gvFwffglqM?= =?us-ascii?q?rozlOiqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hh4rJi48W11zJ+jh0zog1K9?= =?us-ascii?q?O3RkN1Yd6qHpteuS2GN4V7TcAvT31ptSs1yrMIt5C2cTYUxJkkwxPTd/OJf5SV?= =?us-ascii?q?7x/lSe2fLzB4hHd/d7K+gRa/6U+gxfHmWcmx1FZGtC1FksPDtnwV0BzT6c2HSv?= =?us-ascii?q?p//ku73jaPzQ/T5vleLkwuj6XbN5gsyaMzmJoLqUnPADP6lUHsgKKVdkgo4Pak?= =?us-ascii?q?5/r5brn8u5ORNJN4hwfjOao0gMO/G/43Mg0WUmib5+u80Lrj8FX8QLpQj/02lr?= =?us-ascii?q?DVsInZJcgGv6K5DRJZ34U/5xqlADem19MYnXYDLF1bYh6Ik4/pO1TWLPD5C/ew?= =?us-ascii?q?nUisnS91y/zaOrDtGJbAI3jZnLv/Y7px9VRQxBcwwNxD/55UD6sOIPP3Wk//rt?= =?us-ascii?q?zYCRo5PhS7w+n9E9p9zIIeVnyLAqODK6PdrV+I6fw1I+aSfo8Yozn9K/0/6P7v?= =?us-ascii?q?iX81g0MSfa6s3ZcPcnC3AuxmI1mFYXrrmtoODX0Fvg86TODzjF2CUCVTZ2qpUq?= =?us-ascii?q?In5jA7DZqmAp3ZSoCshryBxia7EYdMamBIEFDfWUvvIqKAVvhEPCWWL8BJlT8B?= =?us-ascii?q?VLrnTJUug1Xmvwb/z/J6NefO4WVMvpvm0J1x5vbPvRA07z19ScqHhTKjVWZxy0?= =?us-ascii?q?wBTSU30aQ3mkd9x02Oy+AsjPVSD91e47VSWQc3L5PG5+N/AtH2HAnGe4HaGx6d?= =?us-ascii?q?Xty6DGRpHZoKyNgUbhMlQoTwvlX4xyOvRoQtufmODZ0w/Ljb2iGodcl4wnfCkq?= =?us-ascii?q?Imigt/G5cdBSidnqd6sjPrKcvRiUzAzvSlcK0d2GjG82LRlTPT7nEdaxZ5VOD+?= =?us-ascii?q?ZV5aZkbSqo6ntEbLTrvrELd+dwUYmZbEJaxNZdnky15BQaW7NQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A+AgCrIDlgf7TeVdFihS5LVjoxhEGBH?= =?us-ascii?q?pAaBR0DizCPM4FoCwEDAQ0oDAQBAYRNAoF6Ah0HAQQ0EwIQAQEFAQEBAgEDAwQ?= =?us-ascii?q?BEwEBDQsLCCeFag2COCKDawEBAQEBARIRBBkBGx4DAQsGAwILNwICIgERAQUBH?= =?us-ascii?q?AYBEggagk+CVAEDDiEPlGmPEoEEPYs0fxYFAReDBQaBNAGDJQoZKA1iA4E4Agc?= =?us-ascii?q?SgSaFZIEYAQGCUoNzJhCBUUKBETaCNi4+gkYXA4ElZ4Jpgl8EgkAIej4BgR2BK?= =?us-ascii?q?AK5PywHgn+BGgULiBWSYSKEbJ5qlFWLPZZ5ECOBSIF6MxojUDGCOAlHGQ2QRYF?= =?us-ascii?q?JhRSFRkMvOAIGAQkBAQMJjBMBAQ?= X-IPAS-Result: =?us-ascii?q?A0A+AgCrIDlgf7TeVdFihS5LVjoxhEGBHpAaBR0DizCPM4F?= =?us-ascii?q?oCwEDAQ0oDAQBAYRNAoF6Ah0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBDQsLCCeFa?= =?us-ascii?q?g2COCKDawEBAQEBARIRBBkBGx4DAQsGAwILNwICIgERAQUBHAYBEggagk+CVAE?= =?us-ascii?q?DDiEPlGmPEoEEPYs0fxYFAReDBQaBNAGDJQoZKA1iA4E4AgcSgSaFZIEYAQGCU?= =?us-ascii?q?oNzJhCBUUKBETaCNi4+gkYXA4ElZ4Jpgl8EgkAIej4BgR2BKAK5PywHgn+BGgU?= =?us-ascii?q?LiBWSYSKEbJ5qlFWLPZZ5ECOBSIF6MxojUDGCOAlHGQ2QRYFJhRSFRkMvOAIGA?= =?us-ascii?q?QkBAQMJjBMBAQ?= X-IronPort-AV: E=Sophos;i="5.81,208,1610406000"; d="scan'208,217";a="374218733" X-MGA-submission: =?us-ascii?q?MDHw128KX/sbzBd8fnxRS/D396tKurZFHXIB5A?= =?us-ascii?q?DUN3sVaJR6przV1AKtTGIjcpANAjoH82u5+IqSyo0U/Whu5PeFRyf6gB?= =?us-ascii?q?V9E1IjmTRKW1/qRLzIK6uItBLv1thddoq6rDUzrZdcrdatqXTsX34wdS?= =?us-ascii?q?M3RqwrKx/dYmz41YMl8RjX6Q=3D=3D?= Received: from mail-qk1-f180.google.com ([209.85.222.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 26 Feb 2021 17:29:38 +0100 Received: by mail-qk1-f180.google.com with SMTP id l132so8395841qke.7 for ; Fri, 26 Feb 2021 08:29:38 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=PCRxd+d/+CjZ+xPGEAzQxz7M3iyz5RkzIGVgZyYMveM=; b=Vvw0vCTRypO9Am1osEJzWgeDNWahOKzBJI440/pCvvclT9aD0xQpQwklVgfF3+dJDc krXgbZdX1/gNiiLDLHSTJG6eDLtez3GqPs+dYd/1sJXlb9joqJcitKOpqOXIR8zstpcx EkS4GCZsmYIdvOTwbDo+3xBzFVT2P1mewcx/KBA4xV3q5sPU45TKy/U6g5PTS4C8cmHy HR7TOEI+m3blk6f+75L/AtICR9XvZw7WIPumbZ4b6mfYYbxF2nZUD9Zul3pSKdvc2bq9 n+EgO78tX9IfvjcV3tEefYbcNckfGY8+ZyHjWJrA/HPOe0uFW/r7PaBZV3hv38I4QIXf sifg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to; bh=PCRxd+d/+CjZ+xPGEAzQxz7M3iyz5RkzIGVgZyYMveM=; b=N85apdsrYVyOgU1DzjpbFkzDJ45VG5EYL6H277LrtAHS2W4qfxeunIhskSt9KQevPf tVJFCf7YmEXkUlXFdWIPw1W3HSI/ry4qiPfZQnQwqe6arOzJLoZcQENLDkD8BE0pEB0f siOS1tJ/Hjke9dN5boUXVuv0FmQdDbB1W4pMghO+BaysObY/quW7l3NXJNf5afwE699Z Sk6h1DkNV0aF8PO4Fa6RmO1WEMTaUbjG0WWO0t6fjqXhfribMjQ1nyvePqCKtEwlKoBn QStIx4sHOgD66QzoolHV35MHY4yfubnp9UVIUDFLstP28UQ5lxqIDq0dzsp8m+c55qLd ar4A== X-Gm-Message-State: AOAM533GcKjnLUIi4mPHP+abebjWTlnjPMsZgm+b+RgzYpqFPDDTYxyt rbyW0kU2HalaBGDkXIfObQVk1aplAX18rajRWnbRcOMGEuw= X-Google-Smtp-Source: ABdhPJwYk8d5iHROj4Ix9umr4ie4jJVE05YbYjgaqIdmZQPO0qfO7wzHVoskS5E+YPWU9sUSK+fDI/Y94CxoQgNPTLE= X-Received: by 2002:a37:68c1:: with SMTP id d184mr3273667qkc.395.1614356977592; Fri, 26 Feb 2021 08:29:37 -0800 (PST) MIME-Version: 1.0 References: <20210226162856.GA5806@Melchior.localnet> In-Reply-To: <20210226162856.GA5806@Melchior.localnet> From: Gabriel Scherer Date: Fri, 26 Feb 2021 17:29:01 +0100 Message-ID: To: Oleg , caml users Content-Type: multipart/alternative; boundary="00000000000030aeb605bc3fc6fe" Subject: Re: [Caml-list] Breaking type abstraction of modules --00000000000030aeb605bc3fc6fe Content-Type: text/plain; charset="UTF-8" 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. > > > --00000000000030aeb605bc3fc6fe Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Oleg,

Is this very diff= erent from exposing the GADT equality directly in the module interface?

module A : sig
=C2=A0 type t (* abstract *)=
=C2=A0 val reveals_abstraction : (int, t) eq (* or maybe not *)<= /div>
=C2=A0 val x : t
end

l= et Refl =3D A.reveals_abstraction in A.x + 1

On Fri, Feb 26, 2021= at 5:24 PM Oleg <oleg@okmij.org&g= t; 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/20= 13/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.

=C2=A0 (* Type representation library
=C2=A0 =C2=A0 A minimal version of
=C2=A0 =C2=A0 http://okmij.org/ftp/ML/trep.ml
=C2=A0 *)

=C2=A0 type _ trep =3D ..

=C2=A0 type (_,_) eq =3D Refl : ('a,'a) eq

=C2=A0 (* The initial registry, for common data types *)
=C2=A0 type _ trep +=3D
=C2=A0 =C2=A0 | Int=C2=A0 =C2=A0 : int trep

=C2=A0 type teq_t =3D {teq: 'a 'b. 'a trep -> 'b trep -&= gt; ('a,'b) eq option}

=C2=A0 let teqref : teq_t ref =3D ref {teq =3D fun x y -> None} (* defau= lt case *)

=C2=A0 (* extensible function *)
=C2=A0 let teq : type a b. a trep -> b trep -> (a,b) eq option =3D fu= n x y ->
=C2=A0 =C2=A0 (!teqref).teq x y

=C2=A0 (* Registering an extension of teq *)
=C2=A0 let teq_extend : teq_t -> unit =3D fun {teq =3D ext} ->
=C2=A0 =C2=A0 let {teq=3Dteq_old} =3D !teqref in
=C2=A0 =C2=A0 teqref :=3D {teq =3D fun x y -> match ext x y with None -&= gt; teq_old x y | r -> r}

=C2=A0 (* Registering the initial extension *)
=C2=A0 let () =3D
=C2=A0 =C2=A0 let teq_init : type a b. a trep -> b trep -> (a,b) eq o= ption =3D fun x y ->
=C2=A0 =C2=A0 =C2=A0 match (x,y) with
=C2=A0 =C2=A0 =C2=A0 | (Int,Int)=C2=A0 =C2=A0 =C2=A0 =C2=A0-> Some Refl<= br> =C2=A0 =C2=A0 =C2=A0 | _=C2=A0 -> None
=C2=A0 =C2=A0 in teq_extend {teq =3D teq_init}


Now, the main problematic example

=C2=A0 module A : sig
=C2=A0 =C2=A0 type t=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(* Here= , t is abstract *)
=C2=A0 =C2=A0 type _ trep +=3D AT : t trep
=C2=A0 =C2=A0 val x : t
=C2=A0 =C2=A0end =3D struct
=C2=A0 =C2=A0 type t =3D int=C2=A0 =C2=A0 =C2=A0 =C2=A0 (* Here, t is concr= ete int *)
=C2=A0 =C2=A0 type _ trep +=3D AT : t trep
=C2=A0 =C2=A0 let x =3D 1

=C2=A0 =C2=A0 let () =3D
=C2=A0 =C2=A0 =C2=A0let teq : type a b. a trep -> b trep -> (a,b) eq = option =3D fun x y ->
=C2=A0 =C2=A0 =C2=A0 =C2=A0match (x,y) with
=C2=A0 =C2=A0 =C2=A0 =C2=A0| (AT,AT) -> Some Refl
=C2=A0 =C2=A0 =C2=A0 =C2=A0| (AT,Int) -> Some Refl=C2=A0 =C2=A0 =C2=A0 (= * Since t =3D int, it type checks *)
=C2=A0 =C2=A0 =C2=A0 =C2=A0| (Int,AT) -> Some Refl
=C2=A0 =C2=A0 =C2=A0 =C2=A0| _ -> None
=C2=A0 =C2=A0 in teq_extend {teq=3Dteq}
=C2=A0 end


And here is the problematic behavior:

=C2=A0 # let _ =3D A.x + 1

=C2=A0 Line 1, characters 8-11:
=C2=A0 1 | let _ =3D A.x + 1
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ^^^
=C2=A0 Error: This expression has type A.t but an expression was expected o= f type
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0int

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

=C2=A0 # let _ =3D match teq A.AT Int with | Some Refl -> A.x + 1 | _ -> assert= false
=C2=A0 - : int =3D 2

and bring in the equality that t is an int, and get A.x + 1 to type
check after all.


--00000000000030aeb605bc3fc6fe--