Goswin von Brederlow <goswin-...@web.de> writes: > Andreas Rossberg <rossb...@mpi-sws.org> 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 != <abstract>" 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 <caml/mlvalues.h> 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 -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs