From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 93CF67F168 for ; Mon, 7 Sep 2015 20:33:56 +0200 (CEST) IronPort-PHdr: 9a23:CPX/+RZyJTK0VENk4DTyK1P/LSx+4OfEezUN459isYplN5qZpcS+bnLW6fgltlLVR4KTs6sC0LqK9fm4EjVaut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDuvcSLKFwS33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs14VSGYLiVJtBBTZ6FmuW57rsTbh8O96xDWeFcLzRLEwHz+l6vE4ZgXvjXIiNj05+WDTwul5iq5BsRGgoVQrxofSbJuEN/t4VqLGZckTXixbQ5ACBGR6HoqgYt5XXKI6NuFCoty4/gNWoA== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mandrykin@ispras.ru; spf=None smtp.mailfrom=mandrykin@ispras.ru; spf=None smtp.helo=postmaster@smtp.ispras.ru Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.79; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=mailfrom; client-ip=83.149.199.79; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp.ispras.ru) identity=helo; client-ip=83.149.199.79; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@smtp.ispras.ru"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CvBADJ1+1Vbk/HlVNdg3dphQavPIsdgxWCaAKBMDwQAQEBAQEBAQEQPD2CHYIHAQEEJxM/EAsYCRUQDwFHBhMbiBfJBQEBAQEGAiCLboRZMweELAWNaIdthQqKAoZakguEKW6ISQEBAQ X-IPAS-Result: A0CvBADJ1+1Vbk/HlVNdg3dphQavPIsdgxWCaAKBMDwQAQEBAQEBAQEQPD2CHYIHAQEEJxM/EAsYCRUQDwFHBhMbiBfJBQEBAQEGAiCLboRZMweELAWNaIdthQqKAoZakguEKW6ISQEBAQ X-IronPort-AV: E=Sophos;i="5.17,485,1437429600"; d="scan'208";a="145024886" Received: from smtp.ispras.ru ([83.149.199.79]) by mail3-smtp-sop.national.inria.fr with ESMTP; 07 Sep 2015 20:33:54 +0200 Received: from molnar.localnet (unknown [83.149.199.91]) by smtp.ispras.ru (Postfix) with ESMTP id 5C213203C6; Mon, 7 Sep 2015 21:33:52 +0300 (MSK) From: Mikhail Mandrykin To: Markus Mottl Cc: OCaml List Date: Mon, 07 Sep 2015 21:33:52 +0300 Message-ID: <2362538.z7Nm2DEGTb@molnar> User-Agent: KMail/4.14.6 (Linux/3.19.0-26-generic; KDE/4.14.6; x86_64; ; ) In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 7Bit Content-Type: text/plain; charset="us-ascii" Subject: Re: [Caml-list] Late adding of type variable constraints On Friday, September 04, 2015 07:58:26 PM Markus Mottl wrote: > I see. So it's not really a matter of soundness, but the type checker > changes would presumably be overly intrusive and possibly cause issues > with efficiency. Ultimately, I wanted to be able to constrain type > variables via a functor argument, which is also apparently not > possible. > > Maybe there are alternative solutions to what I'm trying to do, which > is actually a quite neat type system challenge: > > Imagine you have a datastructure that is parameterized over an unknown > number of type variables. Given such a datastructure, I want to be > able to map all these type variables from one type to another while > preserving the "skeleton" of that structure, but without limiting the > skeleton constructors to a specific number of type variables. Not sure if it's exactly what's desired, but I'd suggest Format-like implementation in spirit of the following: (* The mapper "format" GADT, support for pairs, options, results and type variables *) type ('c, 'r, 'i, 'o) mfmt = (* 'c -- continuation, 'r -- result of the form (('a -> 'b) -> ... -> ('y -> 'z) -> 'c), 'i -- input type, o -- output type *) | T_v : ('c, ('e -> 'f) -> 'c, 'e, 'f) mfmt | Pair : ('r1, _ -> _ as 'r2, 'i1, 'o1) mfmt * ('c, _ -> _ as 'r1, 'i2, 'o2) mfmt -> ('c, 'r2, 'i1 * 'i2, 'o1 * 'o2) mfmt | Option : ('c, _ -> _ as 'r, 'i, 'o) mfmt -> ('c, 'r, 'i option, 'o option) mfmt | Result : ('r1, _ -> _ as 'r2, 'i1, 'o1) mfmt * ('c, _ -> _ as 'r1, 'i2, 'o2) mfmt -> ('c, 'r2, ('i1, 'i2) result, ('o1, 'o2) result) mfmt constraint 'r = 'x -> 'y (* The CPS mapper generator, accepts continuation after mapper "format" *) let rec map : type a y z d e x. (x -> e, (y -> z), a, d) mfmt -> ((a -> d) -> x -> e) -> (y -> z) = function | T_v -> fun c f -> c f | Pair (m1, m2) -> fun c -> map m1 @@ fun f1 -> map m2 @@ fun f2 ->c @@ fun (a, b) -> f1 a, f2 b | Option m -> fun c -> map m @@ fun f -> c (function Some a -> Some (f a) | None -> None) | Result (m1, m2) -> fun c -> map m1 @@ fun f1 -> map m2 @@ fun f2 -> c @@ function | Ok a -> Ok (f1 a) | Error b -> Error (f2 b) (* The final mapper generator *) let map f = map f (fun x -> x) (* Examples *) (* Mapper for the skeleton (('a, 'b) option, 'c option * 'd) result *) let map_1 m1 m2 m3 m4 = map (Result (Pair (T_v, Option T_v), Pair (Option T_v, T_v))) m1 m2 m3 m4;; let f = map_1 succ int_of_string string_of_int pred;; f (Ok (5, Some "6"));; (* Ok (6, Some 6) *) f (Error (None, 0));; (* Error (None, -1) *) (* Mapper for skeleton ('a * ('c * 'e), 'g option * 'i option) result *) let map_2 m1 m2 m3 m4 m5 = map (Result (Pair (T_v, Pair (T_v, T_v)), Pair (Option T_v, Option T_v))) m1 m2 m3 m4 m5;; let f = map_2 succ (fun (a, b) -> Some (int_of_string b, string_of_int a)) float_of_int pred (function Ok a -> Some (Error a) | Error a -> Some (Ok a));; f (Ok (1, ((6, "7"), 0)));; (* Ok (2, (Some (7, "6"), 0.)) *) f (Error (None, Some (Ok "5")));; (* Error (None, Some (Some (Error "5"))) *) With open extensible types it's possible to extend this approach to unlimited number of supported basic skeleton types, but the resulting usages would look somewhat messy, e.g.: let map_1 m1 m2 m3 m4 = let open T_v in let module O = Option (T_v) in let module P1 = Pair (T_v) (O) in let module P2 = Pair (O) (T_v) in let module R = Result (P1) (P2) in R.map (R.Result (P1.Pair (T_v, O.Option T_v), P2.Pair (O.Option T_v, T_v))) m1 m2 m3 m4 -- Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru