From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q46AKJ3i024802 for ; Sun, 6 May 2012 12:20:19 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AssBALlPpk/ZSMDjgGdsb2JhbABEsmsiAQELCwsbAySCDAEBBAEnEz8FCwsYCSUPAQQoIROGEoFtAQMGCa8/HysiiT6KfwGGHwSbYY1KgVw X-IronPort-AV: E=Sophos;i="4.75,538,1330902000"; d="scan'208";a="142728498" Received: from fmmailgate02.web.de ([217.72.192.227]) by mail4-smtp-sop.national.inria.fr with ESMTP; 06 May 2012 12:20:14 +0200 Received: from moweb002.kundenserver.de (moweb002.kundenserver.de [172.19.20.108]) by fmmailgate02.web.de (Postfix) with ESMTP id 208DF1C44F2E1 for ; Sun, 6 May 2012 12:20:14 +0200 (CEST) Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb002) with ESMTPA (Nemesis) id 0M3Slc-1S9Rin3wvY-00r1iZ; Sun, 06 May 2012 12:20:14 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.77) (envelope-from ) id 1SQyZZ-00087M-E3; Sun, 06 May 2012 12:20:13 +0200 From: Goswin von Brederlow To: Goswin von Brederlow Cc: Andreas Rossberg , caml-list@inria.fr References: <87r4uykb09.fsf@frosties.localnet> <8A61AE0A-950A-4AE0-912F-2B7A233C7E8A@mpi-sws.org> <87havu4mxu.fsf@frosties.localnet> Date: Sun, 06 May 2012 12:20:13 +0200 In-Reply-To: <87havu4mxu.fsf@frosties.localnet> (Goswin von Brederlow's message of "Sat, 05 May 2012 18:22:53 +0200") Message-ID: <87k40psjaa.fsf@frosties.localnet> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Provags-ID: V02:K0:mPVeVUkjEgyR4po40fiyNynIOfBo1RdtrHNsmcT//t5 D0eGAIf5m/nnjwO756B8JYkMBqCnZSdv05+RDUuKnfNRgYrwmV Oek+76LoN9POP6gudTLbC/JtLst2OOCDmxfHiV2F4RW23VK8Q/ kaCkuYjoQp1Q7qcXiRlEl+nykZlQpcQkAlUP3CKDerMthfOhuZ e1n8EEuunm8+TJFG/tAbw== Subject: Re: [Caml-list] A shallow option type Goswin von Brederlow writes: > Andreas Rossberg writes: > >> On May 5, 2012, at 15.33 h, Goswin von Brederlow wrote: >>> What I want is a >>> >>> type 'a shallow = NULL | 'a (constraint 'a != 'b shallow) >> >> This is a form of negation, which cannot be expressed in conventional >> type systems. Just consider what it should mean in the presence of >> type abstraction: if you have >> >> M : sig >> type t >> ... >> end >> >> would `M.t shallow` be a legal type? You couldn't decide that properly >> without requiring that _every_ abstract type in every signature is >> annotated with a constraint saying that it is "not shallow". > > True, so abstract types would have to be forbidden too becauseit can't > be decided wether they are save or not. Since 'a shallow is an abstract > type that would also forbid 'a shallow shallow. > > So "constraint 'a != " would be the right thing. > >>> I have some ideas on how to implement this in a module as abstract >>> type >>> providing get/set/clear functions, which basically means I map None >>> to a >>> C NULL pointer and Some x to plain x. I know x can never be the NULL >>> pointer, except when someone creates a 'a shallow shallow and sets >>> Some >>> None. That would turn into simply None. >> >> And how do you know that nobody else implements a _different_ type, >> say shallow2, that does the same thing? And a third party then >> constructs a value of type `int shallow2 shallow`? > > I don't and I can't. But such a type would be abstract so wouldn't be > allowed by the above (reject abstract types). Actualy this could be solved. The problem of a int shallow2 shallow is that both would be using NULL for None. But nobody says I must use NULL. All it needs is a bit pattern that can't be a valid value. Any pointer will do: #include static value nil = Val_unit; CAMLprim value caml_shallow_null(value unit) { (void)unit; // unused return &nil; } Now if shallow2 uses my &nil as well that would be a serious bug in shallow2 and pretty hard to do. >> It seems to me that what you want effectively is a special case of non- >> disjoint union. Unfortunately, those are known to come with all kinds >> of problems, such as not being compositional. >> >> /Andreas > > What I want is to have an array of > > type t ={ ... } (* Unit.t *) > > and a matrix of > > type tile = { ... mutable unit : Unit.t option; } > > that I can safely access from a C thread in parallel with ocaml without > having to look the runtime system or individual tiles (the array and > matrix would both be created outside the ocaml heap). > > The problem I have is that > > tile.unit <- Some unit > > will allocate an option block on the heap and accessing that from C > while the GC runs causes a race condition. > > > What I don't want to do is use > > type tile = { ... mutable unit : Unit.t; } > tile.unit <- Obj.magic 0 > > since then trying things out in the toplevel causes segfaults when the > pretty printer prints the tile.unit and it would be easy to forget to > compare the tile.unit to Obj.magic 0 on every use. I know my shallow > type is basically nothing else but it adds a level of savety to it. > > Idealy I would even love to write > > match tile.unit with > | NULL -> () > | unit -> do_something unit > > I guess some camlp4 magic could be used to transform such a match into > > match Shallow.as_option tile.unit with > | None -> () > | Some unit -> do_something unit > > or similar constructs. > > MfG > Goswin MfG Goswin