From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 6818C5D5 for ; Fri, 26 Feb 2021 16:23:50 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.81,208,1610406000"; d="scan'208";a="495122884" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 26 Feb 2021 17:23:48 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 573E1E1D40; Fri, 26 Feb 2021 17:23:48 +0100 (CET) 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 EFD57E1D37 for ; Fri, 26 Feb 2021 17:23:46 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=oleg@okmij.org; spf=Pass smtp.mailfrom=oleg@okmij.org; spf=None smtp.helo=postmaster@mail1.g3.pair.com IronPort-PHdr: =?us-ascii?q?9a23=3AI8wRtxZihtQpQ5N0beJICW3/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZr8y/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/m7KkMx9lKxVrhK/qRJiwIDbb52aO+dwca7GYdMWWXBMUtpNWyFbHI+x?= =?us-ascii?q?aZYEAeobPeZfqonwv0IArR+gCgmjGejizThIhnvo0q01yOkhFgLG3AkhH9IMqn?= =?us-ascii?q?jUq8/1NKgLXO2z0aLHwinNYelM1jfh9IjHbAohofeUUL9sbMfd10giGQ3Hg1uf?= =?us-ascii?q?p4HoPjOb2vkNvmWZ8+ZsSeKhhmElpgxxvDSixdkghpXVio8X11zJ6St0zJsoKN?= =?us-ascii?q?CkS0N2Z8OvHpVXtyGfLYR2Q8UiTnlvuCkm0LIGvJq7cDINyJQ9yB7Tc/uHc4uN?= =?us-ascii?q?4hLiVuadOzB4hGhqeL+5mh288lCgx/X9W8S1ylpHoC5InsPCu3wXyhDf98eKRu?= =?us-ascii?q?Ng8kqg1zuDzQ/e5+VeLUwqiabWKoQtzqAumpYPt0nIAzX4l1/sjKCMc0Up4uio?= =?us-ascii?q?5PrjYrXhvpKcMpV7igD6MqgzgMC/Duo1PhIWX2eB+OS8zqfv8lH+QLVPlvE2k6?= =?us-ascii?q?/Zv47GJckDp6O0AhVZ34gn5hqlATqqyskUkWQIIV5dfRKIlYnpO1XAIPDiCve/?= =?us-ascii?q?hkyhkDBvx//YMb3sGZLNLnvGkLfgf7Zx8UlcyBA8zdxH/ZJbFqkBIO7vWk/2rN?= =?us-ascii?q?HXEgU2Mwmww+r+DNV915geWX6UD6+CMKLStEeI6fg1L+mNYo8Vojf9JOI/6/7g?= =?us-ascii?q?l39q0WMaKKKg2J9SbHGjAtxnJV+YaDzimIQvC2AP6y06QeOi3FqGXDF7YHW3Xq?= =?us-ascii?q?B64Ss0XtH1RbzfT5yg1eTSlBywGYdbMzgfWwK8VEzwfoDBYM8iLSebI8tviDsB?= =?us-ascii?q?DOHzTIwk1BPosxX1meM+crjkvxYAvJem7+BbovXJnEhrpzt3CsWflWaXQDMsxz?= =?us-ascii?q?5ad3oNxKl65HdF5BKD3Kx/2q0KENVS46oPXVx8LZfd1apxDNWgAg8=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CIAQB8HzlgmHIDJ0JigQmBUYMfVwE4M?= =?us-ascii?q?Y1FiFacTgsBAwENKAoCBAEBhkkCHQcBBDQTAhABAQUBAQECAQMDBAETAQEBAQE?= =?us-ascii?q?BAQEJCwsGKYVoDUMWAYFeIoNvKROBNINMAYMGAQ+wboEBM4Q/AYYggTiNQyYPD?= =?us-ascii?q?YFEQ4N+AYMwFwOFKYIrBIJACHo+AYEdgSgCnW6bSzKDBgSBJoE0hmGSUjGEbIE?= =?us-ascii?q?unTygEpcJgWuBek0wCIMkCUcZDY44gg2GXYVUMgExOAIGCgEBAwlYhxeEJAEB?= X-IPAS-Result: =?us-ascii?q?A0CIAQB8HzlgmHIDJ0JigQmBUYMfVwE4MY1FiFacTgsBAwE?= =?us-ascii?q?NKAoCBAEBhkkCHQcBBDQTAhABAQUBAQECAQMDBAETAQEBAQEBAQEJCwsGKYVoD?= =?us-ascii?q?UMWAYFeIoNvKROBNINMAYMGAQ+wboEBM4Q/AYYggTiNQyYPDYFEQ4N+AYMwFwO?= =?us-ascii?q?FKYIrBIJACHo+AYEdgSgCnW6bSzKDBgSBJoE0hmGSUjGEbIEunTygEpcJgWuBe?= =?us-ascii?q?k0wCIMkCUcZDY44gg2GXYVUMgExOAIGCgEBAwlYhxeEJAEB?= X-IronPort-AV: E=Sophos;i="5.81,208,1610406000"; d="scan'208";a="374218364" X-MGA-submission: =?us-ascii?q?MDHpQ8i5Gug5qGMngdLdA0dbaaaKgJxs2+Sq2v?= =?us-ascii?q?DQQG8RUT8V8ZLpedeSXgr15Bbw9kD6jdbw+zURUmNX3om956q86lsXNZ?= =?us-ascii?q?NZ6cU+fQCZ8o96gAx4jCEwsXrPiKszB87VzMiZ9FZZm+MSqL12wBLOXo?= =?us-ascii?q?KDgqFooh9N/QlISSv2AG7AUA=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 26 Feb 2021 17:23:45 +0100 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 83F6F3FB9CA; Fri, 26 Feb 2021 11:23:42 -0500 (EST) Received: from Melchior.localnet (220.206.49.163.rev.vmobile.jp [163.49.206.220]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id BE5AF582CB2; Fri, 26 Feb 2021 11:23:41 -0500 (EST) Date: Sat, 27 Feb 2021 01:28:56 +0900 From: Oleg To: caml-list@inria.fr Message-ID: <20210226162856.GA5806@Melchior.localnet> Mail-Followup-To: Oleg , caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.10.1 (2018-07-13) Subject: [Caml-list] Breaking type abstraction of modules Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 18409 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: 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.