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 sympa.inria.fr (Postfix) with ESMTPS id 065767ED11 for ; Mon, 19 Sep 2016 12:06:25 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=goswin-v-b@web.de; spf=Pass smtp.mailfrom=goswin-v-b@web.de; spf=None smtp.helo=postmaster@mout.web.de Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=217.72.192.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of goswin-v-b@web.de designates 217.72.192.78 as permitted sender) identity=mailfrom; client-ip=217.72.192.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; 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@mout.web.de) identity=helo; client-ip=217.72.192.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3APKBdshLtC03zA5MU8NmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgXLfvxwZ3uMQTl6Ol3ixeRBMOAuqsC27ad6vyoGTRZp83e4DZaKN0EfiRGoP?= =?us-ascii?q?tVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blIt?= =?us-ascii?q?daymUrLV2s++0uT3/5zIfy1JgiC8aPV8NkaYtwLU4+YRmpRjLO4vzR2BiGFFd+?= =?us-ascii?q?lMwWR3bQacmA3j58H14ttp2ztdsbQt+pgTAu3BY60kQOkAX3wdOGcv6ZizuA?= =?us-ascii?q?=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CRAAAquN9Xh07ASNlcHAEBBAEBCgEBF?= =?us-ascii?q?wEXAQYBgwMBAQEBAY8koxSILIIDhh4CgUY4FAEBAQEBAQEBAQEBEgEBAQgNCQk?= =?us-ascii?q?ZL4IyGIIYAQEEJxNECwsYCSUPBSiIYwEevRcfg18BCyWLC4dxgi8BBIg0kTuPU?= =?us-ascii?q?olhCoYJjGSDex6DRoFciFIBAQE?= X-IPAS-Result: =?us-ascii?q?A0CRAAAquN9Xh07ASNlcHAEBBAEBCgEBFwEXAQYBgwMBAQE?= =?us-ascii?q?BAY8koxSILIIDhh4CgUY4FAEBAQEBAQEBAQEBEgEBAQgNCQkZL4IyGIIYAQEEJ?= =?us-ascii?q?xNECwsYCSUPBSiIYwEevRcfg18BCyWLC4dxgi8BBIg0kTuPUolhCoYJjGSDex6?= =?us-ascii?q?DRoFciFIBAQE?= X-IronPort-AV: E=Sophos;i="5.30,361,1470693600"; d="scan'208";a="237352721" Received: from mout.web.de ([217.72.192.78]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 19 Sep 2016 12:06:00 +0200 Received: from frosties.localnet ([78.43.233.192]) by smtp.web.de (mrweb103) with ESMTPSA (Nemesis) id 0LfztP-1bDuN21csN-00pf72 for ; Mon, 19 Sep 2016 12:05:59 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.87) (envelope-from ) id 1blvSY-0007Hu-Na for caml-list@inria.fr; Mon, 19 Sep 2016 12:05:58 +0200 Date: Mon, 19 Sep 2016 12:05:58 +0200 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20160919100558.GC27810@frosties> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.6.0 (2016-04-01) X-Provags-ID: V03:K0:7Ne7Ja7/ZnnUbWzagYtt1JoAMel+0MAKnOz/Rz8Q2+Q1McEET9j YD2V7sJbxXdvU1STHra5iwxbkMhqmc8XVoCI+++oL1KkTD/ZX8eiAfW7NlMEoi8tTii0pRN wUtpHW86Y8NTRNyBOx/7gDnOBgLxF6wEdq5wE/BsZies9/3whnUXeYOfnInmgyQFkku5dw3 7/9iPjgBV9iSSZrHGh5BQ== X-UI-Out-Filterresults: notjunk:1;V01:K0:JU3DymBqkdo=:QxmzMNvoyphGsj9ril0GcU z6FxjazoyI8c8z5EvfYb6QlT7Iph5soQF9U0/EPB5xvoTToaf49AhqBa8cPjzqBdJDJ0pARV/ PDf/Q33+J8m1YS+DCJ56hjoO232kznVxh4sde8dInZyZ4dQTU4sFcREWABrq6UoaTYE9ctWkq gPGwDPF0wUMCHGKGtbBb5SuckH27N1ZbYAD4a6IJHnVAHXbCTtEoE6hYK49ljamF1Loos5AVF lFChOVl8jmH8n+kOH3W2eQDqsw6fSISjcWjJRSfghVbvMs4r7G3/46OdymjWklfD8vD6W4v/R leP6JmwfFNSZ2ZMVDDFmsM7rCqjZbKtSwn2cPxUML4I0FPb8RuiR+bjBL3fvexKvQIAPEocEv QQ1VJTEmeSYWa6/Z3JEUOHdM3PB18bs1/g2llYiIGVneKKMAMQKJV2b0Av2S4RpqddzgU2WQT FNMBsLJZKSTTM6vGHefQH0yqZLfA9K9xv9lK8qRYP6GTx2fxWjEj1Huwys6T3rfpe3Fy77kDI zP4cXWBEZIOTlgdukVqV82hUVavi1q2Nu8UKE3SRA/sBEOOGMDMtSzusR2x3A5uvtK1UwjTjW Rr6tfGNOtj4wMDAYEeK3Vu47CMtzNEm6BGXkm+0wDUu0iwKUdsxgza17CJhNiyR/OWA80NfNW nDnczErTTfKy9F9DQZnz6Urs70Z3BOe2GKIzkwvKUUfRHrUD082W2vq3tPA1/xNiZQ8oAMoG2 TyMZtuojtdjrYmApOGq5yaNtNPqh/WS2wpJdPLybtghh8a6HX8tJC9KCLdg= Subject: Re: [Caml-list] Covariant GADTs On Sun, Sep 18, 2016 at 09:52:24PM -0400, Markus Mottl wrote: > 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 I think here you are trying to encode into the type system if the next/prev point to Empty or Elt. But you don't encode this information into the resulting type at all. How will you know the type of prev/next from an Elt? Problem is that you then need to do that recursively. You not only need to know if next is Empty or Elt but how many Elt there are before you hit Empty and in both directions. E.g. ('el, [`elt] -> [`empty], [`elt] -> [`elt] -> [`empty]) t Also inserting into the list would change the type of every item in the list. Since some other item could be stored somewhere it's type would change and we can't have that. That would rule out using mutables and you would have to copy the whole list on every change. Seems to me like you are on a dead end here. > 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 MfG Goswin