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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 89E457F0A3 for ; Sat, 5 Sep 2015 01:58:28 +0200 (CEST) IronPort-PHdr: 9a23:3+uNcxPI5uMPBCVWpUQl6mtUPXoX/o7sNwtQ0KIMzox0KPX7rarrMEGX3/hxlliBBdydsKIYzbKJ+Pq7EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35jxj7/5ocabSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzhRACW+3YHGkofiABJDBXIpEX1V43rsyTnu8J40TWae8v/QrclUHG/qa5gDh3w3nQpLTk8pUTekM9tl+p+pw69o1QrxofOY5yOcv95Yr/ZVdwfTGtFGM1WUnoSUcuHc4ITAr9Zbq5jpI7nqg5L9EPmCA== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=markus.mottl@gmail.com; spf=Pass smtp.mailfrom=markus.mottl@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f170.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.170 as permitted sender) identity=mailfrom; client-ip=209.85.223.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f170.google.com) identity=helo; client-ip=209.85.223.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-io0-f170.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A5AQBfL+pVlarfVdFdDoMyNWkGqzqUG4YBAoEsBzsRAQEBAQEBAQEQAQEBAQcNCQkfMIIdggcBAQQSEQQZARQHHQEDDAYFCw0CAiYCAiEBAREBBQEcBhMbB4d2AQMSqFqBLz4xi0CBbIJ5iXkKGScNVoQyAQEBAQEBBAEBAQEYAQUOgRSFUYR7gk+CPAeCaYFDBZVRh3SDFoFtkzSFcBIjgReCKYE/WiIziUsBAQE X-IPAS-Result: A0A5AQBfL+pVlarfVdFdDoMyNWkGqzqUG4YBAoEsBzsRAQEBAQEBAQEQAQEBAQcNCQkfMIIdggcBAQQSEQQZARQHHQEDDAYFCw0CAiYCAiEBAREBBQEcBhMbB4d2AQMSqFqBLz4xi0CBbIJ5iXkKGScNVoQyAQEBAQEBBAEBAQEYAQUOgRSFUYR7gk+CPAeCaYFDBZVRh3SDFoFtkzSFcBIjgReCKYE/WiIziUsBAQE X-IronPort-AV: E=Sophos;i="5.17,471,1437429600"; d="scan'208";a="176111901" Received: from mail-io0-f170.google.com ([209.85.223.170]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 05 Sep 2015 01:58:27 +0200 Received: by ioii196 with SMTP id i196so40441577ioi.3 for ; Fri, 04 Sep 2015 16:58:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=sA5S/y3OSEXbkU+HFeTeh+BmPYxcLsmCz9D25qsViZ8=; b=pPn0WqxAraA9VvSgHgKLF2UNDIVa6q964+OvKs8p7TJr6X1JAq/2jgchpVqyxlxAhT VevSNFgnBjptVSqrVRHN20Kid9H/tZeTTeNJX/ODz7jP0R6irwX64WHiIJY0leCeYPj6 LJvGZm4o3f5OFwnbVbOJGejf+jjkfZnfNCTRKnN2qE2I/6ox1w7z1+PBO2VEbTMS7ux3 PVHo9WM8jkPGEg8zT+DjLEL5XKiNzTu5XmOvAZvWizS8oQQb0wq8C3mtwryCUIam6qoN VrmMJk8DR+AniS4Tm7032W3HvBQR8vZ/L23DZlNH90oEbz6oOUolvE2gIHvWM2F/lQd/ FfUg== MIME-Version: 1.0 X-Received: by 10.107.158.18 with SMTP id h18mr12823883ioe.116.1441411106195; Fri, 04 Sep 2015 16:58:26 -0700 (PDT) Received: by 10.79.65.144 with HTTP; Fri, 4 Sep 2015 16:58:26 -0700 (PDT) In-Reply-To: References: Date: Fri, 4 Sep 2015 19:58:26 -0400 Message-ID: From: Markus Mottl To: Jacques Garrigue Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Late adding of type variable constraints 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. Lets assume the "skeleton" is the option type. The first part of the (slightly simplified) solution compiles just fine: --- module type S = sig type 'a t type ('a, 'b) mapper val map : ('a, 'b) mapper -> 'a t -> 'b t end module Option (Arg : S) = struct type 'a t = 'a Arg.t option type ('a, 'b) mapper = ('a, 'b) Arg.mapper let map mapper = function | None -> None | Some el -> Some (Arg.map mapper el) end --- In order to introduce any number of type variables, I thought one could use the following neat trick (example with two variables): --- module Arg1 = struct type 'args t = 'arg1 constraint 'args = 'arg1 * _ type ('src, 'dst) mapper = { map1 : 'src1 -> 'dst1; map2 : 'src2 -> 'dst2; } constraint 'src = 'src1 * 'src2 constraint 'dst = 'dst1 * 'dst2 let map mapper arg1 = mapper.map1 arg1 end --- But "Option (Arg1)" will not type-check, because the constraints are missing in signature "S". This is unfortunate, because I think the code would be correct. The body of "Option" should preserve any constraint on the type variables. Is there any alternative that preserves extensibility, i.e. an implementation of "Option" that will work with any number of type parameters? On Fri, Sep 4, 2015 at 6:19 PM, Jacques Garrigue wrote: > On 2015/09/04 13:28, Markus Mottl wrote: >> >> Hi, >> >> I wonder whether there is a way to add constraints to type variables >> in signatures after the signature was defined. E.g.: >> >> --- >> module type S = sig >> type 'a t >> type ('a, 'b) mappers >> >> val map : ('a, 'b) mappers -> 'a t -> 'b t >> end >> >> module type T = sig >> type 'a t constraint 'a = unit (* whatever *) >> include S with type 'a t := 'a t >> end >> --- >> >> The above will fail, because 'a has additional constraints for type >> "t" in signature "T". If I write instead e.g. "type 'a t = 'a list", >> this will work and also constrain the signature to something narrower. >> What makes constraints on polymorphic variables special here? > > Consider this signature: > > module type S = sig > type 'a t > type 'a u = U of 'a t constraint 'a = < m: int; .. > > end > > Now the signature > S with type 'a constraint 'a t = unit > is ill-typed, but to see it you must type-check again all of its contents > (not just the definition of t). > > This is the reason you cannot do that. > > Jacques Garrigue -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com