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 5A95CE00E5 for ; Wed, 7 Oct 2020 15:13:17 +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 Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of oleg@okmij.org) identity=pra; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of oleg@okmij.org designates 66.39.3.114 as permitted sender) identity=mailfrom; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; 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@mail1.g3.pair.com) identity=helo; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="postmaster@mail1.g3.pair.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AuNHGLB3BDvRnj5Q5smDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?seISI/ad9pjvdHbS+e9qxAeQG9mCtLQY1aGI6ejJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglVhjexe7x/IRS5oQjQqMUdnJdvJLs2xhbVuHVDZv?= =?us-ascii?q?5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnM?= =?us-ascii?q?URGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1ii?= =?us-ascii?q?kIKiQ5/XnZhMJwkqxVvRGvqBNjzIHJYo6aOuFzfr/Bcd4AWWZNQtxcWzJHD4ih?= =?us-ascii?q?b4UPFe0BPeNAoofko1sBsxS+DhSrCePozj9HmHD20LY90+QiFAHG3Q4gE8gJsH?= =?us-ascii?q?TOo9X4LaEfWv26w6fU1zvMde9W2Svj54jSdBAsuf6BULZtfMfVx0QhGB7IgkuN?= =?us-ascii?q?pYH7Iz6Y0vgAvnSH4+dvSe+jlnMrpg5trjWgxMoiiobHi40Vx17K6yl03Zg4Kc?= =?us-ascii?q?O+RUVmb9CkF55QuDubN4twWs4iRGJouCM7yr0Eo5K7ezIKyJshyhXCaPKHa5CF?= =?us-ascii?q?7xPiWeqLLzp1gGhpdbylixqv7EStxfXwWtep3FpWtCZJj9fBu3MX2xDO6MWKSe?= =?us-ascii?q?Fx80mj1DuJygvd8PtLIVoumqreM5MhwqA/lp4UsUnbGy/5gkT2jKuLekk+9eil?= =?us-ascii?q?5f7rYq38qZ+dLY94kB3xMqMrmsCnAOQ4NBYBX3SD9Om91bDv50P0TbFQgvA4iK?= =?us-ascii?q?XVrY3WKMsDqq68GQBV04Ij6xilDzeh1dQVhX4HLFZbdxKIlIXpPFLOIPX5Dfe9?= =?us-ascii?q?mVisly1rx//eMr37HprNNmTDkKvmfbtl90FT0g8zzdRG65JQC7EBO+7zV1TqtN?= =?us-ascii?q?3YCx85Kxa7z/zmCNV7zIMeWHiADrWXMKPIqVWI/P4gI/GQZI8JvzbwM/Yl5+bp?= =?us-ascii?q?jX8lhV8dfLem3YEMZXG5H/RmJl6WYWD2jdsbEGcKuBA+TO3wh1GYXz5TfSX6Y6?= =?us-ascii?q?Vp5DYgCKqsAJ3PR4agxrqMwHSVBJpTM0dCB1/ERXDseoqsXPQJaSDUJdVuxG9X?= =?us-ascii?q?HYO9QpMsgEn9/DTxzKBqe7KNp38o8Kn73d0w3NX90BE/8TstXpaY2mCJFid7xS?= =?us-ascii?q?UQTj4smqt4pB4lkwvR4e1Dm/VdUOdrybZRSA5jbMzbzOl7CZb1QA2TJo7YGmbj?= =?us-ascii?q?ec2vBHQKdvx0xtYPZ0hnHND710LE3C+rAfkSjbPZXZE=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AUAQCEvX1fh3IDJ0JggQmEaVYBMSyNP?= =?us-ascii?q?4g5nCYLAQMBDSMKAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQo?= =?us-ascii?q?LCQgphWMMgjcigxoBAgIBJxM/BRZahAIBglwfAQ+pS4EBM4pggTiNMw4NgUBAg?= =?us-ascii?q?RGCYi4+gkWFQoItBJxUmlUvgnKBHYEshjeRWDGEPIEkm02eCpVTgWuBek0wCDu?= =?us-ascii?q?CaQlHGQ2OKw4Jhi2CNYVRMgEyNwIGCgEBAwlYjWsFAQE?= X-IPAS-Result: =?us-ascii?q?A0AUAQCEvX1fh3IDJ0JggQmEaVYBMSyNP4g5nCYLAQMBDSM?= =?us-ascii?q?KAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQoLCQgphWMMgjcig?= =?us-ascii?q?xoBAgIBJxM/BRZahAIBglwfAQ+pS4EBM4pggTiNMw4NgUBAgRGCYi4+gkWFQoI?= =?us-ascii?q?tBJxUmlUvgnKBHYEshjeRWDGEPIEkm02eCpVTgWuBek0wCDuCaQlHGQ2OKw4Jh?= =?us-ascii?q?i2CNYVRMgEyNwIGCgEBAwlYjWsFAQE?= X-IronPort-AV: E=Sophos;i="5.77,346,1596492000"; d="scan'208";a="361119751" X-MGA-submission: =?us-ascii?q?MDEY7Ix27PO7mRKbeU7AE6PbV6HxAUk9dpHSUu?= =?us-ascii?q?ojTgCAidnfiQXt6/MM8eY6GQiacPeh7JTFAsezO2SV+DOrTV2tdkyJ95?= =?us-ascii?q?EcR4NnswjT4CNX9lMUNvFDdxSVwKkPRqF+i1qEeRkfmSspTdZqMZhGYe?= =?us-ascii?q?4d5yEpqVgxbHgDfzOAakb7bA=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; 07 Oct 2020 15:13:15 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 3B8353FBAAA; Wed, 7 Oct 2020 09:13:12 -0400 (EDT) Received: from Melchior.localnet (37.178.138.210.rev.vmobile.jp [210.138.178.37]) (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 D8D7F584BA6; Wed, 7 Oct 2020 09:13:10 -0400 (EDT) Date: Wed, 7 Oct 2020 22:17:26 +0900 From: Oleg To: josh@berdine.net Cc: francois.pottier@inria.fr, caml-list@inria.fr Message-ID: <20201007131726.GA4913@Melchior.localnet> Mail-Followup-To: Oleg , josh@berdine.net, francois.pottier@inria.fr, 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: Re: [Caml-list] Question on the covariance of a GADT (polymorphic > What I'm unsure of is how this generalizes to additional functions on > expressions. For instance, suppose I also wanted to define a function > which computed the set of int literals that appear in the (unreduced) > expression? ... > More pressingly, I think, is what operations such as `map_ints : (int > -> int) -> 'a exp -> 'a exp` would look like. Frankly speaking, after re-reading the message I sent back in June, I found it rather confusing. It didn't say what the main idea was and the talk about Reducer was too long and unenlightening. Luckily, this time I have your excellent questions, and so get another chance to explain the approach, hopefully better. The basic set up is a little language with int, float and string literals, and the addition operation. The user should be able to add (and keep adding) ints and floats, but attempting to add strings should raise a clear error message. The language expressions should be first-class, that is, we should be able to put them into a list, among other things. (I too find Francois' example superb, but I already had the code for the earlier example). Here is the definition of the language: its operations. The type parameter of t enforces the constraint: ints and floats can be (recursively) added in any combination but strings may not. module type exp = sig type +'a t val int : int -> [> `int] t val float : float -> [> `float] t val add : ([< `int | `float] as 'n) t -> 'n t -> [> `int | `float] t val string : string -> [> `string] t end Here are sample expressions: module Ex1(I:exp) = struct open I (* We can put expressions of different sorts into the same list *) let l1 = [int 1; float 2.0; add (add (int 3) (float 1.0)) (int 4)] (* val l1 : [> `float | `int ] I.t list *) let l2 = string "str" :: l1 (* val l2 : [> `float | `int | `string ] I.t list *) (* An attempt to build an invalid expression fails, with a good error message: let x = add (int 1) (string "s") ^^^^^^^^^^^^ Error: This expression has type [> `string ] t but an expression was expected of type [< `float | `int > `int ] t The second variant type does not allow tag(s) `string *) (* We can define a function to sum up elements of a list of expressions, returning a single expression with addition *) let rec sum l = List.fold_left add (int 0) l (* val sum : [ `float | `int ] I.t list -> [ `float | `int ] I.t *) (* We can sum up l1 *) let l1v = sum l1 (* val l1v : [ `float | `int ] I.t *) (* but, predictably, not l2 let l2v = sum l2 ^^ Error: This expression has type [> `float | `int | `string ] t list but an expression was expected of type [ `float | `int ] t list The second variant type does not allow tag(s) `string *) end One doesn't have to use the functor as I just did. First-class modules, or even records/objects will work too. It is useful to see the expressions. Hence the first implementation of the signature exp: module Show : (exp with type 'a t = string) = struct type 'a t = string let int = string_of_int let float = string_of_float let string x = "\"" ^ String.escaped x ^ "\"" let add x y = Printf.sprintf "Add(%s,%s)" x y end Here is how the sample expressions look like: let _ = let module M = Ex1(Show) in M.l1 (* - : string list = ["1"; "2."; "Add(Add(3,1.),4)"] *) let _ = let module M = Ex1(Show) in M.l2 (* - : string list = ["\"str\""; "1"; "2."; "Add(Add(3,1.),4)"] *) let _ = let module M = Ex1(Show) in M.l1v (* - : string = "Add(Add(Add(0,1),2.),Add(Add(3,1.),4))" *) Now, to your questions. ``suppose I also wanted to define a function which computed the set of int literals that appear in the (unreduced) expression?'' That is easy: we just interpret the same expressions in a different way: instead of showing them, we compute the set of integers that occur in their literals. module IntSet = Set.Make(struct type t = int let compare = compare end) module CollectInts : (exp with type 'a t = IntSet.t) = struct type 'a t = IntSet.t let int x = IntSet.singleton x let float x = IntSet.empty let string x = IntSet.empty let add x y = IntSet.union x y end let _ = let module M = Ex1(CollectInts) in List.map IntSet.elements M.l1 (* - : int list list = [[1]; []; [3; 4]] *) let _ = let module M = Ex1(CollectInts) in IntSet.elements M.l1v (* - : int list = [0; 1; 3; 4] *) The second question: ``More pressingly, I think, is what operations such as `map_ints : (int -> int) -> 'a exp -> 'a exp` would look like. With an initial style representation, this could be defined by traversing the abstract syntax and rebuilding it with the updated `int`s.'' In tagless-final, it looks essentially like this, only simpler. There is no need to write any traversal (a tagless-final term itself specifies the traversal of itself) module MapInts(Map:sig val f : int -> int end)(I:exp) = struct type 'a t = 'a I.t let int x = I.int (Map.f x) let float = I.float let string = I.string let add = I.add end let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l1 (* - : string list = ["2"; "2."; "Add(Add(4,1.),5)"] *) let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l2 (* - : string list = ["\"str\""; "2"; "2."; "Add(Add(4,1.),5)"] *) let _ = let module M = Ex1(MapInts(struct let f = succ end)(Show)) in M.l1v (* - : string = "Add(Add(Add(1,2),2.),Add(Add(4,1.),5))" *) The central idea is this: eval (map f exp) === (compose eval (map f)) exp === let eval' = compose eval (map f) in eval' exp Instead of transforming expressions we transform interpreters (eval). Since evaluation is essentially folding, two foldings may be fused. I have updated http://okmij.org/ftp/tagless-final/subtyping.ml to include your questions.