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 A50DC7ED11 for ; Mon, 19 Sep 2016 03:52:28 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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-it0-f51.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.214.51; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.214.51 as permitted sender) identity=mailfrom; client-ip=209.85.214.51; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f51.google.com) identity=helo; client-ip=209.85.214.51; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-it0-f51.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Aw6AbJxIxrfvwXgyCG9mcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgVKv7xwZ3uMQTl6Ol3ixeRBMOAuqsC27Cd7/qoGTRZp83Q6DZaKN0EfiRGoP?= =?us-ascii?q?1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJL?= =?us-ascii?q?L+j4UrTfk96wn7jrvcaCOkMY3nHhO/sydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeu?= =?us-ascii?q?BblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1e0h83sDgtAHC?= =?us-ascii?q?QA2T/TNcFzxOylsbSzTCuVvCU4vtvzGyn6w15TOZMMH/Sfp8DSyr8r1oRRPhjA?= =?us-ascii?q?8IMjc49Cfcjckm34xBpxf0ghVlwJPPKKSSKOZ6NvfYdMkZWHEHW8FNSyhpDYa1?= =?us-ascii?q?bo9JBO0Ea7UL57LhrkcD+EPtTTKnA/nin3oR3if7?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BnAQBtQ99XhjPWVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFwEBBAEBCgEBgw8BAQEBATw5bQ8HuGmCAyCFfgKBMAc5EwEBAQEBAQE?= =?us-ascii?q?BAQEBEgEBAQgLCwkZL4IyBAEVAQSCEQEBBBIRBBkBFAcdAQMMBgULDQICJgICI?= =?us-ascii?q?QEBEQEFARwGExsHiA0BAxeoAIEyPjKLPYFrgl8Fg1UKGScNVIJTAQEBAQEBAQM?= =?us-ascii?q?BAQEBAQEZAgYQdoUxhFSCR4R/gloBBIg0kQY1gWWEQYZGgnCPaoRYg32ED4I5E?= =?us-ascii?q?x6BESADgyMegXYiNIVrgUABAQE?= X-IPAS-Result: =?us-ascii?q?A0BnAQBtQ99XhjPWVdFdGgEBAQECAQEBAQgBAQEBFwEBBAE?= =?us-ascii?q?BCgEBgw8BAQEBATw5bQ8HuGmCAyCFfgKBMAc5EwEBAQEBAQEBAQEBEgEBAQgLC?= =?us-ascii?q?wkZL4IyBAEVAQSCEQEBBBIRBBkBFAcdAQMMBgULDQICJgICIQEBEQEFARwGExs?= =?us-ascii?q?HiA0BAxeoAIEyPjKLPYFrgl8Fg1UKGScNVIJTAQEBAQEBAQMBAQEBAQEZAgYQd?= =?us-ascii?q?oUxhFSCR4R/gloBBIg0kQY1gWWEQYZGgnCPaoRYg32ED4I5Ex6BESADgyMegXY?= =?us-ascii?q?iNIVrgUABAQE?= X-IronPort-AV: E=Sophos;i="5.30,360,1470693600"; d="scan'208";a="193843831" Received: from mail-it0-f51.google.com ([209.85.214.51]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 Sep 2016 03:52:27 +0200 Received: by mail-it0-f51.google.com with SMTP id 186so58879181itf.0 for ; Sun, 18 Sep 2016 18:52:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=bV26L37eEVWd/sX5vxXSKmzK1G3lH7YNeF+1jvihlCE=; b=qNo3DUmZTUVfjyhTbqklmMwXP9xpOENpEykoia479kzNQvrBxf4yDDaOpz6Dj/3RQQ hUYGFcWgjZlkQz2wHFEi3eeiwuygFEzNtPkeG1H6/rRj9gvokPwgXrMBZTF0JNakI052 S4u8RkH0W9if3qkEuv0JXQD4fQDuZdca+q8werPvVDfDGNxU0shb/qmr7sX/WPO1l1vK aV5R5m1TCEI14J2TKichsCbwcJ5CkTY9e5eU/Y8W2t9eA2l/3RYVk1On/uNt1NI8UIvE 1VoLjV55rjC4BV/DApN9H0x/3BBhGBlPU8LnxUMt2Q66QzvhqchQDTV1aBlKZJTVegtE f3mA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=bV26L37eEVWd/sX5vxXSKmzK1G3lH7YNeF+1jvihlCE=; b=VMxWz5k74B6z+ATcYY7AxZTU28GNgg7BS3tQnjk6LGZe+KbLZi0kljBcdqBDLv7RFM 3HL3gYnTopY2ytigOhoEZWDG63xHB2FGKEL7xqMtSmLOOdqxfLiPnNdQ0/8f/mRMYyT3 l6n+/UIJAxEaFmkbHdVlhdr6WyrkwFYTsKZFschsJyaXnoWb3V7m+zmXAdyDA5Li8X91 DwuHnsNFkmngARmdCYuhPWgmRBQ8zL0xFDSlsp1yNVVst3C09fHlnHHdWZGPcP4X0jCF em0EniIj1k2Ca/VerfI6MfVkQxdQTm4wXv0geonfGgQL+E0RGRk12hY/zjMIpu5e9KO2 xPOg== X-Gm-Message-State: AE9vXwPbftELg/LIJ7dZxkg7SdMqhBJgEo0nppiGd6phShh3pYPCotQA6EmkGymNhn7tQx19asoOP/1AJi3UZg== X-Received: by 10.36.163.193 with SMTP id p184mr7786754ite.102.1474249945469; Sun, 18 Sep 2016 18:52:25 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Sun, 18 Sep 2016 18:52:24 -0700 (PDT) In-Reply-To: References: From: Markus Mottl Date: Sun, 18 Sep 2016 21:52:24 -0400 Message-ID: To: "Petter A. Urkedal" Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Covariant GADTs Hi Petter, thanks, the above approach obviously works with my previous example, which I had sadly oversimplified. In my case I was actually dealing with inlined, mutable records where the above won't work, because then I can't overwrite fields. The somewhat more complete example also contains strange type system behavior I don't understand that may even be a bug. The example below shows how GADTs + inline records + (if available) covariance could help implement doubly linked lists much more efficiently. The memory representation using mutable inline records is essentially optimal. Taking an element link can be done without having to introduce superfluous pattern matches, because the GADT guarantees via the type system that a link is non-empty. I had to use "Obj.magic" due to the lack of covariance support with GADTs in the "coerce" function, which I believe to be sound. The strange behavior is in the "insert_first" function and also the "create" function: "Empty" is not of covariant type, but nevertheless can be used for allocation in that way (e.g. in the "let res = ..." part). But the commented out lines show that I cannot overwrite the exact same field in the just allocated value with the exact same value. I can understand the reason why the latter is not possible, but why is allocation allowed that way? Maybe a type system guru can explain what's going on. ---------- module Link = struct type kind = [ `empty | `elt ] type ('el, _) t = | Empty : ('el, [ `empty ]) t | Elt : { mutable prev : ('el, [< kind ]) t; el : 'el; mutable next : ('el, [< kind ]) t; } -> ('el, [ `elt ]) t let coerce (t : ('el, [< kind ]) t) : ('el, [< kind ]) t = Obj.magic t let get_opt_elt : type a. ('el, a) t -> ('el, [ `elt ]) t option = function | Empty -> None | Elt _ as elt -> Some elt let cut : type a. ('el, a) t -> unit = function | Empty -> () | Elt { prev = prev_elt; next = next_elt } -> match prev_elt, next_elt with | Empty, Empty -> () | Empty, Elt next -> next.prev <- coerce Empty | Elt prev, Empty -> prev.next <- coerce Empty | Elt prev, Elt next -> prev.next <- coerce next_elt; next.prev <- coerce prev_elt end (* Link *) module Doubly_linked : sig type 'el t type 'el elt val create : unit -> 'el t val first : 'el t -> 'el elt option val insert_first : 'el t -> 'el -> unit val remove : 'el elt -> unit end = struct open Link type 'el t = Head : { mutable head : ('el, [< Link.kind ]) Link.t } -> 'el t type 'el elt = ('el, [ `elt ]) Link.t let create () = Head { head = Empty } let first (Head h) = Link.get_opt_elt h.head let insert_first (Head h) el = h.head <- match h.head with | Empty -> let res = Elt { prev = Empty; el; next = Empty } in (* let Elt foo = res in *) (* foo.prev <- Empty; *) coerce res | Elt _ as next -> coerce (Elt { prev = Empty; el; next }) let remove = Link.cut end (* Doubly_linked *) ---------- Regards, Markus On Sun, Sep 18, 2016 at 4:17 AM, Petter A. Urkedal wrote: > Hi Markus, > > On 17 September 2016 at 19:38, Markus Mottl wrote: >> Hi, >> >> GADTs currently do not allow for variance annotations so I wondered >> whether there are any workarounds for what I want: >> >> ----- >> type +_ t = >> | Z : [ `z ] t >> | S : [ `z | `s ] t -> [ `s ] t >> >> let get_next (s : [ `s ] t) = >> match s with >> | S next -> next >> ----- >> >> The above compiles without the variance annotation, but then you >> cannot express "S Z", because there is no way to coerce Z to be of >> type [`z | `s] t. >> >> Another approach I tried is the following: >> >> ----- >> type _ t = >> | Z : [ `z ] t >> | S : [< `z | `s ] t -> [ `s ] t >> >> let get_next (s : [ `s ] t) : [< `z | `s ] t = >> match s with >> | S next -> next >> ----- >> >> The above gives the confusing error: >> >> ----- >> Error: This expression has type [< `s | `z ] t >> but an expression was expected of type [< `s | `z ] t >> The type constructor $S would escape its scope >> ----- >> >> There are apparently two type variables associated with [< `s | `z ] >> t: the locally existential one introduced by matching the GADT, and >> the one in the type restriction of the function, but the compiler >> cannot figure out that these can be safely unified. There is >> currently no way of specifying locally abstract types that have type >> constraints, which could possibly also help here. > > In this case, you can supply the needed type information to `get_next` > with structural type matching: > > type _ t = Z : [`z] t | S : 'a t -> [`s of 'a] t > let get_next : [`s of 'a] t -> 'a t = function S next -> next > > This gives you a richer type which also allows defining get_next_pair, etc. > >> Are there workarounds to achieve the above? Are there any plans to >> add variance annotations for GADTs? > > I had a similar problem myself and found a paper [1] explaining the > issue and a possible solution. Haven't really studied it, but as I > understand the issue is that the current GADTs only introduce type > equality, which is too strict to verify variance. What is needed is > more like (my ASCIIfication) > > type +'a t = > | Z when 'a >= [`z] > | S when 'a >= [`s] of [< `z | `s] t > > allowing 'a in each case to be a supertype rather than equal to the > specified type. In that spirit, I tried > > type +_ t = > | Z : [> `z] t > | S : [< `s | `z] t -> [> `s] t;; > > but that does not check for variance either. > > Best, > Petter > > [1] https://arxiv.org/abs/1301.2903 -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com