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 943545D5 for ; Sat, 27 Jun 2020 15:33:10 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.75,287,1589234400"; d="scan'208";a="457018573" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 27 Jun 2020 17:33:08 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id D9072E016E; Sat, 27 Jun 2020 17:33:08 +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 16227E0133 for ; Sat, 27 Jun 2020 17:33:03 +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=3A/wDV9RUp4Yp4nkusMWU7pkVoySDV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYYxyPt8tkgFKBZ4jH8fUM07OQ7/m9HzVRut3R4DgrS99lb1c9k8?= =?us-ascii?q?IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBo?= =?us-ascii?q?KevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrNQajI9sJ6o+yRbEoWZDdv?= =?us-ascii?q?hLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfM?= =?us-ascii?q?TQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklD?= =?us-ascii?q?sLOjgk+2zRl8d+jr9UoAi5qhJxw4DafpybOvlxcazBYNwVR2ROU91NVyBdGI6w?= =?us-ascii?q?c5cDAvAfMetesoLzp0EOrRy7BQS0He3vziFHhnDr1qA91OQhFR/J3AM7EtIJs3?= =?us-ascii?q?TUqdT1NKUIXeCy1qnIwizOYvVL0jjy9IbGaAouoe2QXb1ua8rRz1EiGgzBg1iN?= =?us-ascii?q?rYHoMTyb2/kTv2SG8edtSeaihnI7pg1trTWi2toghpTGi44JxV3J9yV3zok6KN?= =?us-ascii?q?C4RkB3f8OpHYVOuyycKoB4TMQiQ2RytyY7zL0LoZm7fCsPyJQmxR7TcfuHc5KH?= =?us-ascii?q?4h/lSe2fIi94iWpkdb++nRq//0ytxvfyW8WuzVpGsyVInsHRun0M2RHf8MeKR/?= =?us-ascii?q?9n8ku/xTqC1xrf5vxYLU01k6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk//Kn?= =?us-ascii?q?6+XjYrn7vJOcOIF5hhvmMqs0m8y/G/40PRQJX2ie4ei81bvj8lPlQLhSj/A7k7?= =?us-ascii?q?PVvZ7eKMgBqKO1GRJZ3pss5hqnCjepytUYnX0JLFJffxKHipDkO1bKIP/mAvey?= =?us-ascii?q?mFOskDRux/DHPL3tGJLNLmLMkLv5Z7Zy91ZcyBYvzdBY/59bFqsOIPf3WkPosN?= =?us-ascii?q?zYDwQ5MxCvzub8CNR905seVniVDq+YNqPSq16I6fg1L+mCfo9G8Ar6fvoi/P7G?= =?us-ascii?q?h3IjlV4bcO+v0IdERmq/G6FBJ0iWKS7rhtoOOWAJuws8CuvwhwvRAnZoe3+uUv?= =?us-ascii?q?dktXkAA4W8ANKbH9z/sPm6xC6+W6ZuSCVeEFnVSCXvdICFWbELci3AepYwwAxB?= =?us-ascii?q?bqCoTsoa7T/rsQb7z7R9Ke+No38ftpfi1p5y/eKBzEhvpwwxNNyU1iS2d08xnm?= =?us-ascii?q?4MQGZnjqV2oEgkjFjYl7BxguYeHttWtatE?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BoAgASZvdeh3IDJ0JggQmEY1UBMSyNM?= =?us-ascii?q?aQWCwEDAQwjCgIEAQGERwKCKgIcBwEENBMCEAEBBQEBAQIBAwMEARMBAQEKCwk?= =?us-ascii?q?IKYViDII3IoMWBicTPxtad4MLAYJ7AQ+tO4EBM4pygTiMZg4MgUBAgRGCYi4+g?= =?us-ascii?q?kWFQYItBJp3mVYrgmaBFoEnhgqQZi+EDYEXmXCbZ5RkgWqBeE0wCDuCaQlHGQ2?= =?us-ascii?q?ON4Y2gjWFUTIBMjcCBggBAQMJWJAZBQEB?= X-IPAS-Result: =?us-ascii?q?A0BoAgASZvdeh3IDJ0JggQmEY1UBMSyNMaQWCwEDAQwjCgI?= =?us-ascii?q?EAQGERwKCKgIcBwEENBMCEAEBBQEBAQIBAwMEARMBAQEKCwkIKYViDII3IoMWB?= =?us-ascii?q?icTPxtad4MLAYJ7AQ+tO4EBM4pygTiMZg4MgUBAgRGCYi4+gkWFQYItBJp3mVY?= =?us-ascii?q?rgmaBFoEnhgqQZi+EDYEXmXCbZ5RkgWqBeE0wCDuCaQlHGQ2ON4Y2gjWFUTIBM?= =?us-ascii?q?jcCBggBAQMJWJAZBQEB?= X-IronPort-AV: E=Sophos;i="5.75,287,1589234400"; d="scan'208";a="457018550" X-MGA-submission: =?us-ascii?q?MDHnzDwT+NdmrXszUga4OYMJxEfmgf9iuWSht3?= =?us-ascii?q?P7YSkPSRSZq25NFZipQVBpu6MyBEg0yfbVN8TdW3zvicN4b5tRxZUn+9?= =?us-ascii?q?sx6u0bZJpjGyvjla06DZwSwdJ484TMfAKdyV+ZAJqmAls9dXgNNEiwtU?= =?us-ascii?q?pWjolPJsAKtYugusXosjnruw=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; 27 Jun 2020 17:33:01 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 256353FB222; Sat, 27 Jun 2020 11:32:59 -0400 (EDT) Received: from Melchior.localnet (106.205.49.163.rev.vmobile.jp [163.49.205.106]) (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 A82465835EA; Sat, 27 Jun 2020 11:32:57 -0400 (EDT) Date: Sun, 28 Jun 2020 00:36:43 +0900 From: Oleg To: josh@berdine.net Cc: caml-list@inria.fr Message-ID: <20200627153643.GA4954@Melchior.localnet> Mail-Followup-To: Oleg , josh@berdine.net, caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <452E9622-D117-43E6-A0B1-9B8272F3C5FE@berdine.net> User-Agent: Mutt/1.10.1 (2018-07-13) Subject: Re: [Caml-list] Subtyping of phantom GADT indices? Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 18180 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: Josh Berdine has posed a problem: > As a concrete example, consider something like: > ``` > type _ exp = > | Integer : int -> [> `Integer] exp > | Float : float -> [> `Float] exp > | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp > | String : string -> [> `String] exp > ``` > The intent here is to use polymorphic variants to represent a small > (upper semi-) lattice, where basically each point corresponds to a > subset of the constructors. The type definition above is admitted, but > while the index types allow subtyping ... > this does not extend to the base type: > ``` > # let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);; > Line 1, characters 18-67: > 1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);; > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > Error: Type [ `Integer ] exp is not a subtype of > ([> `Float | `Integer ] as 'a) exp > The first variant type does not allow tag(s) `Float > ``` > This makes sense since `type _ exp` is not covariant. But trying to > declare it to be covariant doesn't fly, yielding: > ``` > Error: In this GADT definition, the variance of some parameter > cannot be checked > ``` We demonstrate three solutions to this problem. The first has an imperfection, but is easier to explain. The second removes the imperfection. The third one is verbose, but requires the least of language features and can be implemented in SML or perhaps even Java. All three solutions give the end user the same static guarantees, statically preventing building of senseless expressions. All three rely on the tagless-final style, in effect viewing the problem as a language design problem -- designing a DSL with subtyping. It has been my experience that the tagless-final, algebraic point of view typically requires less fancy typing. Incidentally, the third solution, of explicit coercions, can be combined with GADTs and is hence the general solution to the posed problem, showing how to do phantom index subtyping with GADTs. Presenting all three solutions is too long for a message, so one should look at the complete code with many comments: http://okmij.org/ftp/tagless-final/subtyping.ml Below is the outline of the first solution, the easiest to explain. (The others just add slight variations; the main example looks almost the same in all three). We will think of the problem as a DSL with subtyping. Let's define its syntax and the type system, as an OCaml signature: 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 The language expressions are indexed with a subset of tags `int, `float, `string. The language has the obvious subtyping: [> `int] can be weakened to [> `int | `float]. This weakening, and general typechecking of our DSL is performed by OCaml's type checker for us. Let's see an example 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 *) end Now, what we can do with the expressions? We can print/show them module Show : (exp with type 'a t = string) = struct type 'a t = string ... elided ... end let _ = let module M = Ex1(Show) in M.l1 (* - : string list = ["1"; "2."; "Add(Add(3,1.),4)"] *) We can also reduce them. The following is the reducer -- although in reality it does the normalization-by-evaluation (NBE) A subset of expressions: values module type vals = sig type +'a t val int : int -> [> `int] t val float : float -> [> `float] t val string : string -> [> `string] t end module Reducer(I:vals) : (sig include exp val observe : ([> `float | `int ] as 'a) t -> 'a I.t end) = struct type 'a t = Unk of 'a I.t | Int of int | Float of float let observe = function | Unk x -> x | Int x -> I.int x | Float x -> I.float x let int x = Int x let float x = Float x let string x = Unk (I.string x) let add x y = match (x,y) with | (Int x, Int y) -> Int (x+y) | (Float x, Float y) -> Float (x+.y) | (Int x, Float y) | (Float y, Int x) -> Float (float_of_int x +. y) (* This is the imperfection. We know that the case cannot happen, but this is not clear from the type system. We should stress that this imperfection does not compromise the guarantees offered to the end user, who never sees the internals of Reducer, and can't even access them. *) | _ -> assert false end (* We can now evaluate exp to values. We need a way to show them though. Luckily, exp is a superset of values, and we already wrote the show interpreter for exp *) let _ = let module I = Reducer(Show) in let module M = Ex1(I) in List.map I.observe M.l1 (* - : string list = ["1"; "2."; "8."] *) The second solutions removes the imperfection in Reduce, making Reduce.add total, by making the types more phantom. The third solution does the obvious thing: implementing subtyping using explicit coercions. In the given example, it doesn't add too much annoyance to the user. It does however remove the reliance on variance and so is applicable to GADTs in general. One can imagine more solutions along the shown lines.