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 9FBCD5D4 for ; Wed, 4 Sep 2019 15:23:33 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,467,1559512800"; d="scan'208";a="400270846" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 04 Sep 2019 17:23:32 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id A559F7EF57; Wed, 4 Sep 2019 17:23:32 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 1D4EA7EF0B for ; Wed, 4 Sep 2019 17:23:28 +0200 (CEST) Authentication-Results: mail2-smtp-roc.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=3AplnKvBWI0edXmwwtNFhtgbFPxkXV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYYh2Bt8tkgFKBZ4jH8fUM07OQ7/m6HzVfvN3R7TgrS99lb1c9k8?= =?us-ascii?q?IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBo?= =?us-ascii?q?KevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrswndrNQajIliJ6o+yRbEomZDdv?= =?us-ascii?q?hLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfM?= =?us-ascii?q?TQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklD?= =?us-ascii?q?sLOjgk+2zRl8d+jr9UoAi5qhJxw4DafpybOvlxcazBYNwVS3FMXtpNWyFbHo+w?= =?us-ascii?q?c5ECA/QHMO1Fr4f9vVwOrR6mCAe1AOPg1DBIjWLx0K091+QuDw7G0RcnH9INtX?= =?us-ascii?q?TUrdf1OL0VUeCvw6nF1DPOZO5Y1zf67YjHaBEhofeUULJ3csrRzEgvFwHfglWX?= =?us-ascii?q?s4zlMDWY3fkOvWiD9+dtVOOih3Qppgx1uDSiyN0ghpTUio8a0lzJ+iF0zJwrKd?= =?us-ascii?q?C2TEN3e9+pHZhKuyyYOIZ7RN4pTXtytyYg0LIGvIa2fCgUx5QjwB7Sc/mHfJKJ?= =?us-ascii?q?4hLnSeqdOzh4iXx/dLKnnRmy8FKgxvfgWcmz1VZGtitFkt/SuXARzxHe68mKRu?= =?us-ascii?q?Fz80qlwzqC2Rrf5vxZLU07jabbLoQuwr80lpodq0TDGSr2lV3xjK+SaEok9fOl?= =?us-ascii?q?6+PkYrXjp5+cNZV4igbkMqQhgsC/G/g3MhASX2iH/uSxzKHs8lf8QLVOl/E2lq?= =?us-ascii?q?jZsIvGJckAva64AwpV0p455BqlDjem1s4YnXgdI15fdhKHlduhB1abK/n9CbK7?= =?us-ascii?q?gk+wuDZt3fHPeLP7UbvXKX2Wt7Pscv4p7EpRxyI0ztVe5dRTEL5Xc6G7YVP4qN?= =?us-ascii?q?GNVkxxCAez2euyUIwshLNbYnqGB+qiCI2XtFaJ4uw1JOzVPd0SuzP8Kb4i/fG8?= =?us-ascii?q?1CZky29YRrGg2N4sUF79HvliJBzIM3/lg9NYV2hR+BI3Tfasg1qHA2YKOySCGp?= =?us-ascii?q?kk7zR+M7qISJ/ZT9n00ruC2Sa5WJpMaTIeBw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AqBABK1m9dh3IDJ0JdCR4BBgcGgWeBb?= =?us-ascii?q?oEXUzIqjR2GD50kCQEDAQwjCgIBAYZzGwcBBDQTAgsBAQQBAQECAQMDBAETAQE?= =?us-ascii?q?BCgsJCBsOhTUMgjoigxwTOkE0BYN+AYIJAQ+rODOKSIE0i2kPGIE/QIN2AYMyg?= =?us-ascii?q?UgKDoNZgiYEjD0hiTGVJ26CKQOBcIUDjV8ngyOBEJQ4lXCQfoFnZYEUTTAIO4J?= =?us-ascii?q?sCYJTgQ0BAYZpdIVOMQEygQWOdgEB?= X-IPAS-Result: =?us-ascii?q?A0AqBABK1m9dh3IDJ0JdCR4BBgcGgWeBboEXUzIqjR2GD50?= =?us-ascii?q?kCQEDAQwjCgIBAYZzGwcBBDQTAgsBAQQBAQECAQMDBAETAQEBCgsJCBsOhTUMg?= =?us-ascii?q?joigxwTOkE0BYN+AYIJAQ+rODOKSIE0i2kPGIE/QIN2AYMygUgKDoNZgiYEjD0?= =?us-ascii?q?hiTGVJ26CKQOBcIUDjV8ngyOBEJQ4lXCQfoFnZYEUTTAIO4JsCYJTgQ0BAYZpd?= =?us-ascii?q?IVOMQEygQWOdgEB?= X-IronPort-AV: E=Sophos;i="5.64,467,1559512800"; d="scan'208";a="400270829" X-MGA-submission: =?us-ascii?q?MDHMucZIcIlNtGAN8speburM4PFvkgDZ1F3lRP?= =?us-ascii?q?NiQvMmprBcSfUvprN7kNc/3+66fvc6ggdl8+7Rd+MXNfWDZFj9P1UuMj?= =?us-ascii?q?VcFPTKygpu5g3GvM7bEWOB3YU7dhfpiBC/Tj3nUDQol1o/BkMvOhwcrW?= =?us-ascii?q?oIF1y8pZuM59pkRBv/PrVJ7g=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 04 Sep 2019 17:23:24 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 5FD843FB4B2; Wed, 4 Sep 2019 11:23:17 -0400 (EDT) Received: from Melchior.localnet (74.68.239.49.rev.vmobile.jp [49.239.68.74]) (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 8C1C6582FB7; Wed, 4 Sep 2019 11:23:16 -0400 (EDT) Date: Thu, 5 Sep 2019 00:25:17 +0900 From: Oleg To: caml-list@inria.fr Message-ID: <20190904152517.GA2014@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] Implicits for the masses Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 17794 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: This is to announce a simple, plain OCaml library to experiment with type-class/implicits resolution, which can be thought of as evaluating a Prolog-like program. One may allow `overlapping instances' -- or prohibit them, insisting on uniqueness. One may make the search fully deterministic, fully non-deterministic, or something in-between. There is an immediate, albeit modest practical benefit: the facility like "#install_printer", which was restricted to top-level, is now available for all -- as a small, self-contained, plain OCaml library with no knowledge or dependencies on the compiler internals. We show an example at the end of the message. This message has been inspired by the remarkable paper Canonical Structures for the working Coq user Assia Mahboubi, Enrico Tassi DOI: 10.1007/978-3-642-39634-2_5 Its introduction is particularly insightful: the power of (mathematical) notation is in eliding distracting details. Yet to formally check a proof, or to run a program, the omitted has to be found. When pressed to fill in details, people `skillful in the art' look in the database of the `state of the art', with the context as the key. Computers can be programmed similarly; types well represent the needed context to guide the search. Mahboubi and Tassi's paper explains very well how this eliding and filling-in is realized, as a programmable unification, and used in Coq. Yet their insights go beyond Coq and deserve to be known better. This message and the accompanying code is to explain them in plain OCaml and encourage experimentation. It could have been titled `Canonical Structures for the working OCaml (meta) programmer'. The rudiment of canonical structures is already present in OCaml, in the form of the registry of printers for user-defined types. This facility is available only at the top-level, however, and deeply intertwined with it. As a modest practical benefit, this facility is now available for all programs, as a plain, small, self-contained library, with no compiler or other magic. The full potential of the method is realized however in (multi-) staged programming. In fact, I'm planning to use it in the upcoming version of MetaOCaml to implement `lifting' from a value to the code that produces it -- letting the users register lifting functions for their own data types. http://okmij.org/ftp/ML/canonical.ml The implementation and the examples, some of which are noted below. http://okmij.org/ftp/ML/trep.ml A generic library of type representations: something like Typeable in Haskell. Some day it may be built-in into the compiler http://okmij.org/ftp/ML/canonical_leadup.ml A well-commented code that records the progressive development of canonical.ml. It is not part of the library, but may serve as its explanation. Here are a few examples, starting with the most trivial one module Show = MakeResolve(struct type 'a dict = 'a -> string end) let () = Show.register Int string_of_int (* Define `instances' *) let () = Show.register Bool string_of_bool Show.find Int 1;; However contrived and flawed, it is instructive. Here (Int : int trep) is the value representing the type int. The type checker can certainly figure out that 1 is of the type int, and could potentially save us trouble writing Int explicitly. What the type checker cannot do by itself is to find out which function to use to convert an int to a string. After all, there are many of them. Show.register lets us register the *canonical* int->string function. Show.find is to search the database of such canonical functions: in effect, finding *the* evidence that the type int->string is populated. Keeping Curry-Howard in mind, Show.find does a _proof search_. The type of Show.find is 'a trep -> ('a -> string). Compare with Haskell's show : Show a => a -> String (or, desuraging => and Show) show : ('a -> string) -> ('a -> string). Haskell's show indeed does not actually do anything: it is the identity function. All the hard work -- finding out the right dictionary (the string producing function) -- is done by the compiler. If one does not like the way the compiler goes about it -- tough luck. There is little one may do save complaining on reddit. In contrast, the first argument of Show.find is trivial: it is a mere reflection of the type int, with no further information. Hence Show.find has to do a non-trivial work. In the case of int, this work is the straightforward database search -- or, if you prefer, running the query ?- dict(int,R) against a logic program dict(int,string_of_int). dict(bool,string_of_bool). The program becomes more interesting when it comes to pairs: dict(T,R) :- T = pair(X,Y), !, dict(X,DX), dict(Y,DY), R=make_pair_dict(DX,DY). Here is how it is expressed in OCaml: let () = let open Show in let pat : type b. b trep -> b rule_body option = function | Pair (x,y) -> Some (Arg (x, fun dx -> Arg (y, fun dy -> Fact (fun (x,y) -> "(" ^ dx x ^ "," ^ dy y ^ ")")))) | _ -> None in register_rule {pat} let () = Show.register (Pair(Bool,Bool)) (fun (x,y) -> string_of_bool x ^ string_of_bool y) Our library permits `overlapping instances'. We hence registered the printer for generic pairs, and a particular printer just for pairs of booleans. The library is extensible with user-defined data types, for example: type my_fancy_datatype = Fancy of int * string * (int -> string) After registering the type with trep library, and the printer type _ trep += MyFancy : my_fancy_datatype trep let () = Show.register MyFancy (function Fancy(x,y,_) -> string_of_int x ^ "/" ^ y ^ "/" ^ "") one can print rather complex data with fancy, with no further ado: Show.find (List(List(Pair(MyFancy,Int)))) [[(Fancy ...,5)];[]] As Mahboubi and Tassi would say, proof synthesis at work! We should stress that what we have described is not a type-class facility for OCaml. It is *meta* type-class facility. Show.find has many drawbacks: we have to explicitly pass the trep argument like Int. The resolution happens at run time, and hence the failure of the resolution is a run-time exception. But the canonical instance resolution was intended to be a part of a type checker. There, the resolution failure is a type checking error. The trep argument, representing the type in the object program, is also at hand. Likewise, the drawbacks of Show.find disappear when we use the library in a meta-program (code generator). The library then becomes a type-class/implicits facility, for the generated code -- the facility, we can easily (re)program.