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 ESMTP id B88BD5D4 for ; Tue, 10 Sep 2019 14:38:53 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,489,1559512800"; d="scan'208";a="401100602" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 10 Sep 2019 16:38:27 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id F1A757EF60; Tue, 10 Sep 2019 16:38:27 +0200 (CEST) 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 EB0FE7EF07 for ; Tue, 10 Sep 2019 16:38:19 +0200 (CEST) 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=3ATCT+zRHAsN2bF4qh8+HTPZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78os+wAkXT6L1XgUPTWs2DsrQY0rGQ6/irBDFIoc7Y9ixbKtoUD15NoP?= =?us-ascii?q?5VtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blIt?= =?us-ascii?q?daz6FYHIksu4yf259YHNbAVUnjq9Zq55IAmroQnLucQanIVvJrwtxhfVrXdFe+?= =?us-ascii?q?Rbzn5sKV6Pghrw/Mi98IN9/yhKp/4t68tMWrjmcqolSrBVEC4oOH0v6s3xshnD?= =?us-ascii?q?QwqP5n8CXWgTjxFFHQvL4gzkU5noqif1ufZz1yecPc3tULA7Qi+i4LtxSB/pky?= =?us-ascii?q?gIKTg0+3zKh8NqjaJbpBWhpwFjw4PRfYqYOuZycr/bcNgHQ2dKQ8RfWDFbAo6k?= =?us-ascii?q?YYUBD/QPM/tboYbyu1QBsBmxCge3CePz1jNFnGP60bEg3ug/FwzNwQwuH8gJsH?= =?us-ascii?q?TRtNj7LaMSXv66zKLVyjjDaPdW1iny6IXTdRAhovSMXbNyccbLzkkvDQzFg0yW?= =?us-ascii?q?pIf4MT2V0eENvHKa7+pmTe+vhG8nqx1xojiy3cggkJXGhoUQylzc8iV5w4M1Jd?= =?us-ascii?q?y6SEJhZt6kCpRQuieHPIV1WsMvW2BltScgxrAIvZO3ZiYHxI46yxLCZPGLa5aE?= =?us-ascii?q?7g//WOqLPDt1inFodKiiixuw80Ws0PDwW8m63VtMsyFLiMPDtmoX2BzW8sWHSu?= =?us-ascii?q?Vy/kOm2TuX0gDc8OBEIUQpmabBJJ4szKQ8loIJvkTCBC/6gln5jKiTdkk8++io?= =?us-ascii?q?7froYqn+q5KdNoJ4kA/zP6A0lsGxG+g0LxUCUmeD9eS5zrLj/En5QLtQjv0xl6?= =?us-ascii?q?nUqJfaJcAFqa62GAJV1YUj6xO+DzekytgYmmMHLF1ddBKdk4fpI03OIOz/Dfqn?= =?us-ascii?q?n1ujijJrx/TfMr3lA5XNNWTDnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tN?= =?us-ascii?q?zCXVcFNFm13enPCdhw28UZQ23cLLWeNfb1tVKHrrYoJ+SDTIgWvTf/bf8/6Ki9?= =?us-ascii?q?3jcChVYBcPzxjtMsY3eiE6E+ehnLUT/Xmt4EVFwykE8mVuWz0Q+FUjtSZTC1Ra?= =?us-ascii?q?1uvmhmWrLjNp/KQ8WWuJLE3Cq/GcQHNGVPC1TVV3izMZ2NWu1KYyWXcJc4w240?= =?us-ascii?q?EIO5Qopk7imA8Qrzyr5pNO3Ro3RKspHm1doz4Pfcx0g/?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DGAADAtHddh3IDJ0JkGgEBAQEBAgEBA?= =?us-ascii?q?QEHAgEBAQGBZwIBgwJTMiqNHYYVgg+bGQkBAwEMIwoCAQGEPwKCSRsHAQQ1BQ0?= =?us-ascii?q?CDAEBBAEBAQIBAwMEARMBAQEKCwkIGw6FNQxCFgGBYSKCcAICAScTPwU3NAWDf?= =?us-ascii?q?gGBew4BD6gqM4pDgTQBi3cYgT9Ag25zgkgZAoEtg3GCJgSJIotfgSCWJoIrgXa?= =?us-ascii?q?FC4kihEgngySBEJRWlgOREoFqgXhNMAg7gmwJgkQPCYNPhRSFTjEBMoEFin2EJ?= =?us-ascii?q?gEB?= X-IPAS-Result: =?us-ascii?q?A0DGAADAtHddh3IDJ0JkGgEBAQEBAgEBAQEHAgEBAQGBZwI?= =?us-ascii?q?BgwJTMiqNHYYVgg+bGQkBAwEMIwoCAQGEPwKCSRsHAQQ1BQ0CDAEBBAEBAQIBA?= =?us-ascii?q?wMEARMBAQEKCwkIGw6FNQxCFgGBYSKCcAICAScTPwU3NAWDfgGBew4BD6gqM4p?= =?us-ascii?q?DgTQBi3cYgT9Ag25zgkgZAoEtg3GCJgSJIotfgSCWJoIrgXaFC4kihEgngySBE?= =?us-ascii?q?JRWlgOREoFqgXhNMAg7gmwJgkQPCYNPhRSFTjEBMoEFin2EJgEB?= X-IronPort-AV: E=Sophos;i="5.64,489,1559512800"; d="scan'208";a="318924729" X-MGA-submission: =?us-ascii?q?MDEwjTtnIRsuRDpQwEHS7JRwOweUX0GBxtuVn1?= =?us-ascii?q?bcQJezdiY7JzJGSsOVmdtMzG0PBxhpX208XhSwCP5kDfzuy1fs997Yg9?= =?us-ascii?q?m5/r/CMYkdUEH+mkBmaQttawOfY85z3k7jCAmhwPtfWY+E4EwWtHRdZv?= =?us-ascii?q?GQ8Wk9349a0H1zdeLDL4KB4g=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; 10 Sep 2019 16:38:18 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 17CF03FB80C; Tue, 10 Sep 2019 10:38:15 -0400 (EDT) Received: from Melchior.localnet (153.177.138.210.rev.vmobile.jp [210.138.177.153]) (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 F123A582FA7; Tue, 10 Sep 2019 10:38:13 -0400 (EDT) Date: Tue, 10 Sep 2019 23:40:16 +0900 From: Oleg To: ivg@ieee.org Cc: caml-list@inria.fr Message-ID: <20190910144016.GA1725@Melchior.localnet> Mail-Followup-To: Oleg , ivg@ieee.org, caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.10.1 (2018-07-13) Subject: [Caml-list] Type-indexed heterogeneous collections (Was: Implicits for the masses) Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 17798 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: > https://github.com/BinaryAnalysisPlatform/bap - the BAP project per se. > ... That is quite a project! And interesting, too. Thank you for letting me know. Now I understand what you mean by ``universe of types actually grew quite large, that large that the linear search in the registry is not an option for us anymore.'' What your message has made it very clear, to me, is that we really need the standard type representation library -- hopefully being part of Stdlib and eventually integrated with the compiler. For one, it is high time we standardized the spelling of the ('a,'b) eq type and its constructor. Mainly, as your message has well demonstrated, an efficient trep is actually non-trivial, and takes lots of experience to design. Incidentally, the situation on Haskell is very similar: Typeable is now well integrated with the compiler. It is quite a popular library. I'd also like to draw attention to truly type-indexed heterogeneous collections where trep is a part of a key rather than a part of a value. To explain what I mean, let's recall the state of the art of heterogeneous collections. Let ('key,'v) coll be an ordinary homogeneous collection (a map, a hashtable, or an associative list) with a look-up function lookup : 'key -> ('key,'v) coll -> 'v option We can turn it into a heterogeneous collection that stores data of various types by using dynamics dyn: an existential that contains the data of some type t along with t trep, the representation of the type t. You have showed a very efficient dyn (which I will keep in mind, thank you). The dyn extraction from_dyn_opt : 'a trep -> dyn -> 'a option checks if the trep given as an argument matches trep stored inside dyn, and if so, returns dyn's value, of the requested type. Related from_dyn : 'a trep -> dyn -> 'a throws an exception on mismatch. The heterogeneous collection is then ('key, dyn) coll, with the look-up operation that is a `composition' of lookup and from_dyn let lookup_het : 'key -> 'a trep -> ('key,dyn) coll -> 'a option = fun key trep coll -> match lookup key coll with | None -> None | Some dyn -> Some (from_dyn trep dyn) I grant the elegance of the implementation and the reuse of the existing collections. What bothers me however is that the 'a trep is a part of the element value (part of dyn) rather a part of the key. The real lookup is done solely on the key, and the trep comparison is used as a verification, just to make sure we found the right dyn. If the code is correct, the check does not fail. Somehow I am always bothered by operations whose results isn't actually used but still have to be done. Wouldn't it be nice if all operations advanced us towards the goal, with no need for looking back and double-checking. Heterogeneous collections, at least, could be designed that way. Here is the gist: type 'key binding = B : 'key * 'a trep * 'a -> 'key binding (a more efficient existential could be designed, following the ideas of your message.) The binding is what its name says: an association of the key, the trep, and the value. The simplest heterogeneous collection, the analogue of association lists, is a list of bindings. type 'key halist = 'key binding list let lookup_hetkey : type a key. key -> a trep -> key halist -> a option = fun key trep coll -> let rec loop : key halist -> a option = function | [] -> None | B (key',trep',v) :: t -> match (key=key',teq trep' trep) with | (true,Some Refl) -> Some v | _ -> loop t in loop coll Now both key and trep equally participate in search: the mismatch of trep and trep' is not a failure but an indicator to continue search. The clear drawback is that the shown code uses a linear search -- and we cannot use off-the-shelf Maps or hashtables to speed it up. Still, an adaptation of an extant Hashtable is rather straightforward. In fact, the following file http://okmij.org/ftp/ML/hetcoll.ml shows the implementation of type-indexed heterogeneous hash tables. It is almost the same as Stdlib.Hashtable, but stripped to bare minimum and slightly adjusted. (The biggest adjustment has nothing to do with types; I simply didn't like how resizing was implemented). module type TypedHashedType = sig type t (* key type *) val equal: t -> t -> bool (* key equality *) val hash: t -> 'a trep -> int (* Hash the key and trep *) end module type S = sig type key type t val create: int -> t val clear : t -> unit val add: t -> key -> 'a trep -> 'a -> unit val find_opt: t -> key -> 'a trep -> 'a option val length: t -> int end Although the interface is very minimal, it is enough for registering your types and classes and my canonical functions. Stdlib.Map could likewise be adjusted.