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 D1E9C7F1AA for ; Fri, 11 Sep 2015 17:56:35 +0200 (CEST) IronPort-PHdr: 9a23:9j27BBEWaa09CDv9evp9/p1GYnF86YWxBRYc798ds5kLTJ75r86wAkXT6L1XgUPTWs2DsrQf27aQ6vCrCD1IyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6brq9aCMk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGC6O5XsVU2FetxNODxLU7xD8FsP0uy32rPt+2S+yPNbuV7kvHy6/ufRFUhjt3QIOLT0k6ynyjdBsiOoPpRu7pAFkhYvTfJ2RHPV7d6LZO9gdQDwSDY5qSyVdD9bkPMM0BO0bMLMd9tGlqg== 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-f171.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.171; 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.171 as permitted sender) identity=mailfrom; client-ip=209.85.223.171; 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-f171.google.com) identity=helo; client-ip=209.85.223.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-io0-f171.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ABAgC4+PJVlavfVdFdg3dpBoMkvA+FdwKBTgc8EAEBAQEBAQEBEAEBAQEHDQkJHzCCHYIGAQEBAgEBEhEEGQEUBx0BAwELBgULDQICJgICIQEBEQEFARwGEyKHdgEDCggNqkKBMD4xi0GBbIJ5iX4KGScNVoQPAQEBAQEBBAEBAQEBARYBBQ6BFIVRhH2CUII9B4JpgUMFlVaFCoYDgW2BTJFxg1CCIBIjgRc4gi+CGSIzAYoeAQEB X-IPAS-Result: A0ABAgC4+PJVlavfVdFdg3dpBoMkvA+FdwKBTgc8EAEBAQEBAQEBEAEBAQEHDQkJHzCCHYIGAQEBAgEBEhEEGQEUBx0BAwELBgULDQICJgICIQEBEQEFARwGEyKHdgEDCggNqkKBMD4xi0GBbIJ5iX4KGScNVoQPAQEBAQEBBAEBAQEBARYBBQ6BFIVRhH2CUII9B4JpgUMFlVaFCoYDgW2BTJFxg1CCIBIjgRc4gi+CGSIzAYoeAQEB X-IronPort-AV: E=Sophos;i="5.17,511,1437429600"; d="scan'208";a="177040744" Received: from mail-io0-f171.google.com ([209.85.223.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 11 Sep 2015 17:56:35 +0200 Received: by ioii196 with SMTP id i196so102860001ioi.3 for ; Fri, 11 Sep 2015 08:56:33 -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=pHNinzFyqySZNjmSkrqYDfFwEiZ6xD1RwJ69+Pj3Fgc=; b=VqDchKssNr+qxYJJTTjFGfDnubuV1VXWspCkecuw54h0+R8b4Gzbpr11FObhVLcbpF gEGa47nP2sIoFwMTQ/XWiAnxGZ0j6by7Xt6kzBevQ99wjK0uNVViGH+1k0Sg0m41DKg2 G9SfldX+Z8cBasDenFqGMsMHejXMaRep1rPiWyN5Lk+ZVf5SIAU9S/4yWvs15tPhDLC2 Iilf6ZFz+KdoQ1X4iHnUW4j3VwIIvNLVKXJKVCM1/xrSuk2f8VxwqgAnT5BgzD2I/0PR gCTaLtPJSUN/rT39HTe1A6/Y66mEcHzpPHmkoWI/Pfne+KdXK3gOoG/V4ivRo9nXdeMw D/jw== MIME-Version: 1.0 X-Received: by 10.107.162.200 with SMTP id l191mr4911982ioe.176.1441986993833; Fri, 11 Sep 2015 08:56:33 -0700 (PDT) Received: by 10.79.65.144 with HTTP; Fri, 11 Sep 2015 08:56:33 -0700 (PDT) In-Reply-To: <1527892.mlrKSESLQ8@molnar> References: <2362538.z7Nm2DEGTb@molnar> <1527892.mlrKSESLQ8@molnar> Date: Fri, 11 Sep 2015 11:56:33 -0400 Message-ID: From: Markus Mottl To: Mikhail Mandrykin Cc: caml-list@inria.fr, OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Late adding of type variable constraints On Wed, Sep 9, 2015 at 3:28 PM, Mikhail Mandrykin wrote: > Probably the defunctionalization encoding used in the paper on Lightweight > Higher-Kinded Polymorphism in OCaml > (https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf) can help in some way. The corresponding library and examples > are available at https://github.com/ocamllabs/higher. Thanks a lot for this reference and your code. Though my problem still seems slightly different, I found this to be a very interesting paper. I remember reading Reynolds' work on defunctionalization many years ago, and it's fascinating how his work translates from the object to the type language. > The implementation used in the library doesn't perfectly fit the case, because > the suggested encoding puts the type `t' capturing the type skeleton on an > unknown depth inside the list of type constructor applications. I tried the > following slight variation on the initial encoding: I think the main problem for me is not so much capturing the skeleton, which the initial approach does just fine, but that type constraints on the polymorphic variables are maintained with mapper functions. Maybe the more complicated approaches can be combined to solve the problem, but that is likely not trivial. > module Newtype1 (T : sig type 'a t end) = > struct > type 'a s = 'a T.t > type t > type (_, _) typ += Mk : 'a T.t -> (('a, nil) app, t) typ > let inj v = Mk v > let prj (Mk v) = v > end The compiler will warn above that "prj" is not exhaustive. If I understand this correctly, the reasoning is that it's impossible for two GADT constructors to yield the same type so the warning should be spurious. But wouldn't this require making Newtype1 a generative functor (i.e. adding "()")? Otherwise the type "t" could be seen as equivalent if Newtype1 is applied to the same module more than once, which would allow for more than one "Mk" case and could hence cause a runtime match error. I think for the while being I'll just stick to the syntactic approach. Users who want to extend the number of base types to be mapped over would have to include code with "Pair", "Option", etc. within an environment with augmented constraints. -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com