[Caml-list] A shallow option type

[Caml-list] A shallow option type

[Goswin von Brederlow]

Hi,

I wish there was an option type that would work without extra
indirection (or more importantly without extra allocation of an ocaml
value when setting it to something).

Why? I'm interfacing with C in a multithreaded way. The data is
allocated on the C side so it won't be moved around by the GC. The ocaml
side will modify data and the C side will utilize it. Now if ocaml
changes a multable 'a option then it will allocate a block for "Some x"
and the GC will move that block around during compaction. Which means
the 'a option can't be safely used without holding the runtime system
lock. Which then means the threads can't run in parallel.

What I want is a

    type 'a shallow = NULL | 'a  (constraint 'a != 'b shallow)

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.

Is it possible to somehow declare the constraint that 'a in 'a shallow must
not be itself a 'b shallow?

MfG
        Goswin

Re: [Caml-list] A shallow option type

[Gabriel Scherer]

> Is it possible to somehow declare the constraint that 'a in 'a shallow
> must not be itself a 'b shallow?

If I understand correctly, this is not possible directly, and while
you could do that with a sufficiently clever layer of phantom types,
I'm not sure it is worth the additional complexity. In particular, you
would not be able to statically move from ('a shallow) to ('a) by the
imperative action of updating a reference (one would need a type
system with strong update, where state change may incur type change,
to do that).

I think that, given your constraints, the simplest solution is
probably to just use 'a, while informally specifying that it is not
always safe to use, and providing from the C side a null value of type
'a, so that you can dynamically test on the OCaml side that your
variable indeed is initialized.
(I suppose you need to expose yet-unitialized values to the OCaml
side, otherwise you wouldn't need to reason about nullability at all.)

On Sat, May 5, 2012 at 3:33 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> Hi,
>
> I wish there was an option type that would work without extra
> indirection (or more importantly without extra allocation of an ocaml
> value when setting it to something).
>
> Why? I'm interfacing with C in a multithreaded way. The data is
> allocated on the C side so it won't be moved around by the GC. The ocaml
> side will modify data and the C side will utilize it. Now if ocaml
> changes a multable 'a option then it will allocate a block for "Some x"
> and the GC will move that block around during compaction. Which means
> the 'a option can't be safely used without holding the runtime system
> lock. Which then means the threads can't run in parallel.
>
> What I want is a
>
>    type 'a shallow = NULL | 'a  (constraint 'a != 'b shallow)
>
> 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.
>
> Is it possible to somehow declare the constraint that 'a in 'a shallow must
> not be itself a 'b shallow?
>
> 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
>

Re: [Caml-list] A shallow option type

[Andreas Rossberg]

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".

> 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`?

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

Re: [Caml-list] A shallow option type

[Andreas Rossberg]

I should add that, even if "shallow options" where easy to achieve,  
they are really a bad idea. You can witness that in "dynamic"  
languages, where the lack of types leads everybody to just use the  
equivalent of non-disjoint unions, and thus shallow options. This can  
lead to an inflation of null-like sentinel values.

Consider e.g. JavaScript. Originally, there was `null`. Then they saw  
the need to distinguish an unbound variable from one bound to null  
(i.e., distinguish `None` from `Some None`) -- and `undefined` was  
born. Fast forward, `undefined` has proliferated to all sorts of APIs,  
and there is a desire to be able to treat it as proper value in many  
places, e.g. be able to store it in maps. Now there are recurring  
discussions how to introduce other sentinel values to distinguish  
"absent" from "mapped to `undefined`".

With a properly compositional, algebraic option type this mess cannot  
arise.

/Andreas


On May 5, 2012, at 16.48 h, Andreas Rossberg wrote:

> 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".
>
>> 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`?
>
> 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
>
>
> -- 
> 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
>

Re: [Caml-list] A shallow option type

[Goswin von Brederlow]

Andreas Rossberg <rossberg@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).

> 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

Re: [Caml-list] A shallow option type

[Gabriel Scherer]

Thanks for the clearer use-case example.

I think Andreas's comment is at a general level of language design:
no, we don't want to add something close to what you're asking for in
a language. His argumentation is spot on. What we could have is a type
system with strong update, but that's dreaming about another language,
not OCaml.

In your case, have you considered having a private option type, that
would be allocated by a call to a C primitive (building a genuine
OCaml option, but outside the heap) instead of (Some foo) on the OCaml
side? That would be completely safe, and you could still safely match
it on the OCaml side.

That said, it's only pushing the problem one step further: now you
still need to allocate your Unit.t value outside the OCaml heap,
otherwise you still have this problem. Is it the case in your
application?

On Sat, May 5, 2012 at 6:22 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> Andreas Rossberg <rossberg@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).
>
>> 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
>
> --
> 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
>

Re: [Caml-list] A shallow option type

[Goswin von Brederlow]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> Thanks for the clearer use-case example.
>
> I think Andreas's comment is at a general level of language design:
> no, we don't want to add something close to what you're asking for in
> a language. His argumentation is spot on. What we could have is a type
> system with strong update, but that's dreaming about another language,
> not OCaml.
>
> In your case, have you considered having a private option type, that
> would be allocated by a call to a C primitive (building a genuine
> OCaml option, but outside the heap) instead of (Some foo) on the OCaml
> side? That would be completely safe, and you could still safely match
> it on the OCaml side.

I have considered that shortly. Setting the option would be simple. A
call to a C primitive that mallocs a block, fills in the GC metadata,
tag and pointer to the unit.

But what about removing the unit, setting the option to None again? At
what point would it be save to free the old option? The other thread
might be using it right now. Any kind of dynamic memory allocation will
require some coordination between the threads to free the block.

Now that I think about it again (and with what I say below for units)
there can be at most one option per tile. So I could pre-allocate an
array of them and assign each tile one option block to be reused
whenever the tile needs one.

> That said, it's only pushing the problem one step further: now you
> still need to allocate your Unit.t value outside the OCaml heap,
> otherwise you still have this problem. Is it the case in your
> application?

Yes that is the plan. The world has a fixed number of tiles and there
can be at most one unit per tile so I can pre-allocate an array of units
outside the heap large enough to never run out.

MfG
        Goswin

> On Sat, May 5, 2012 at 6:22 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
>> Andreas Rossberg <rossberg@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).
>>
>>> 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
>>
>> --
>> 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
>>

Re: [Caml-list] A shallow option type

[Goswin von Brederlow]

Goswin von Brederlow <goswin-v-b@web.de> writes:

> Andreas Rossberg <rossberg@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

Re: [Caml-list] A shallow option type

[Jacques Garrigue]

Hi Goswin,

Actually I remember discussing this issue with Xavier Leroy a long time ago,
and we ended up concluding that this could be done in a clean way by using
a bit pattern not yet used for ocaml values.

Our idea was that rather than put some restriction on the shallowness of
types (which is very hard to implement), one should just allow arbitrary nesting
of option types, and represent the sequence "Some (Some (... ( Some None) ...))"
as an integer.
I think I even tried an implementation, but we then concluded that there
was not enough demand to put it in the compiler.

However there is nothing wrong with providing it as a library.
The basic idea is that you have only two kinds of values in ocaml:
integers, which have their lower bit to 1, and pointers, which must
all be multiples of 4 (on 32-bit architectures).
So  the pattern (v % 4) == 2 is not used.

Here is the code:

module Sopt : sig
  type +'a t
  val none : 'a t
  val some : 'a -> 'a t
  val is_none : 'a t -> bool
  val arg : 'a t -> 'a
  val is_sopt : 'a t -> bool
  val depth : 'a t -> int
end = struct
  type 'a t = int
  let null = (Obj.magic (Some 0) land 2) land 1
  let none = null + 1
  let is_none x = x > 0 && x < 1
  let is_sopt x = is_none (x land 1)
  let some (x : 'a) : 'a t =
    let y : 'a t = Obj.magic x in
    if is_sopt y then y+2 else y
  let arg (x : 'a t) : 'a =
    if is_sopt x then Obj.magic (x-2) else Obj.magic x
  let depth x =
    if is_sopt x then x lsr 1 else 0
end

The code for null tricks the compiler into creating a null pointer.
I avoiding using the simpler (Obj.magic (Some 0) land 0) in case land is optimized.
By adding 1 to this value, one creates a 2 at the C level.
For ocaml this value is "strictly between" 0 (i.e. 1) and 1 (i.e. 3).
Sopt.some checks whether a value is such an sopt, in which case it adds 2 to it to
add a Some constructor, otherwise it returns the value itself.
Sopt.arg does just the opposite.
Sopt.is_sopt and Sopt.depth are only exported for demonstrative purposes.

# Sopt.depth (Sopt.some (Sopt.some (Sopt.some Sopt.none)));;
- : int = 3
# Sopt.depth (Sopt.some (Sopt.some (Sopt.some 0)));;
- : int = 0

Of course this precludes using the above bit pattern for anything else,
but otherwise this should be completely type-safe.
(At the theoretical level at least, I'm not 100% sure of the trickery used here
to have the compiler work on C level integers)

Cheers,

Jacques Garrigue


On 2012/05/05, at 22:33, Goswin von Brederlow wrote:

> Hi,
> 
> I wish there was an option type that would work without extra
> indirection (or more importantly without extra allocation of an ocaml
> value when setting it to something).
> 
> Why? I'm interfacing with C in a multithreaded way. The data is
> allocated on the C side so it won't be moved around by the GC. The ocaml
> side will modify data and the C side will utilize it. Now if ocaml
> changes a multable 'a option then it will allocate a block for "Some x"
> and the GC will move that block around during compaction. Which means
> the 'a option can't be safely used without holding the runtime system
> lock. Which then means the threads can't run in parallel.
> 
> What I want is a
> 
>    type 'a shallow = NULL | 'a  (constraint 'a != 'b shallow)
> 
> 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.
> 
> Is it possible to somehow declare the constraint that 'a in 'a shallow must
> not be itself a 'b shallow?
> 
> 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
> 

Re: [Caml-list] A shallow option type

[Goswin von Brederlow]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:

> Hi Goswin,
>
> Actually I remember discussing this issue with Xavier Leroy a long time ago,
> and we ended up concluding that this could be done in a clean way by using
> a bit pattern not yet used for ocaml values.
>
> Our idea was that rather than put some restriction on the shallowness of
> types (which is very hard to implement), one should just allow arbitrary nesting
> of option types, and represent the sequence "Some (Some (... ( Some None) ...))"
> as an integer.
> I think I even tried an implementation, but we then concluded that there
> was not enough demand to put it in the compiler.

The advantage of providing it by the compiler would be to allow pattern
matching.

> However there is nothing wrong with providing it as a library.
> The basic idea is that you have only two kinds of values in ocaml:
> integers, which have their lower bit to 1, and pointers, which must
> all be multiples of 4 (on 32-bit architectures).
> So  the pattern (v % 4) == 2 is not used.

Actualy isn't (v % 4) == 2 an exception?

caml/callback.h:
#define Make_exception_result(v) ((v) | 2)
#define Is_exception_result(v) (((v) & 3) == 2)
#define Extract_exception(v) ((v) & ~3)

So returning an Sopt.none in a callback would be taken as exception. :)

> Here is the code:
>
> module Sopt : sig
>   type +'a t
>   val none : 'a t
>   val some : 'a -> 'a t
>   val is_none : 'a t -> bool
>   val arg : 'a t -> 'a
>   val is_sopt : 'a t -> bool
>   val depth : 'a t -> int
> end = struct
>   type 'a t = int
>   let null = (Obj.magic (Some 0) land 2) land 1
>   let none = null + 1
>   let is_none x = x > 0 && x < 1
>   let is_sopt x = is_none (x land 1)
>   let some (x : 'a) : 'a t =
>     let y : 'a t = Obj.magic x in
>     if is_sopt y then y+2 else y
>   let arg (x : 'a t) : 'a =
>     if is_sopt x then Obj.magic (x-2) else Obj.magic x
>   let depth x =
>     if is_sopt x then x lsr 1 else 0
> end

WOW. That is some code. Thanks for sharing that.

> The code for null tricks the compiler into creating a null pointer.
> I avoiding using the simpler (Obj.magic (Some 0) land 0) in case land is optimized.
> By adding 1 to this value, one creates a 2 at the C level.
> For ocaml this value is "strictly between" 0 (i.e. 1) and 1 (i.e. 3).
> Sopt.some checks whether a value is such an sopt, in which case it adds 2 to it to
> add a Some constructor, otherwise it returns the value itself.
> Sopt.arg does just the opposite.
> Sopt.is_sopt and Sopt.depth are only exported for demonstrative purposes.
>
> # Sopt.depth (Sopt.some (Sopt.some (Sopt.some Sopt.none)));;
> - : int = 3
> # Sopt.depth (Sopt.some (Sopt.some (Sopt.some 0)));;
> - : int = 0
>
> Of course this precludes using the above bit pattern for anything else,
> but otherwise this should be completely type-safe.
> (At the theoretical level at least, I'm not 100% sure of the trickery used here
> to have the compiler work on C level integers)
>
> Cheers,
>
> Jacques Garrigue

The implementation relies on specific aspect of the compiler to
construct those values. I would give it a 99% chance to fail with an
llvm backend for ocaml for example. Using C stubs that directly
manipulate the bits seems a better approach.

For example nothing says x + 2 can't be implemented as

value add(value x, value y) {
    return (x & ~1) + y;
}

as opposed to

value add(value x, value y) {
    return x + y - 1;
}

MfG
        Goswin

Re: [Caml-list] A shallow option type

[Jacques Garrigue]

On 2012/05/07, at 0:34, Goswin von Brederlow wrote:

> Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
> 
>> Hi Goswin,
>> 
>> Actually I remember discussing this issue with Xavier Leroy a long time ago,
>> and we ended up concluding that this could be done in a clean way by using
>> a bit pattern not yet used for ocaml values.
>> 
>> Our idea was that rather than put some restriction on the shallowness of
>> types (which is very hard to implement), one should just allow arbitrary nesting
>> of option types, and represent the sequence "Some (Some (... ( Some None) ...))"
>> as an integer.
>> I think I even tried an implementation, but we then concluded that there
>> was not enough demand to put it in the compiler.
> 
> The advantage of providing it by the compiler would be to allow pattern
> matching.

And also being compatible with the default option type, and proper marshaling support.
It's really a cost vs. usefulness discussion.

I see no good solution for marshaling.
It would be nice to be able to add hooks to the marshaler for handling
pointers outside of the value area...

>> However there is nothing wrong with providing it as a library.
>> The basic idea is that you have only two kinds of values in ocaml:
>> integers, which have their lower bit to 1, and pointers, which must
>> all be multiples of 4 (on 32-bit architectures).
>> So  the pattern (v % 4) == 2 is not used.
> 
> Actualy isn't (v % 4) == 2 an exception?
> 
> caml/callback.h:
> #define Make_exception_result(v) ((v) | 2)
> #define Is_exception_result(v) (((v) & 3) == 2)
> #define Extract_exception(v) ((v) & ~3)
> 
> So returning an Sopt.none in a callback would be taken as exception. :)

Well-spotted.
It seems that this use of the second bit was added after our discussion.

But the fundamental idea is just to represent "Some (Some (... ( Some None) ...))"
by a special collection of pointers, and this can be done in other ways,
like allocating a region in the C heap, or using a non-allocatable region (you only
need to now that these pointers will never be used).

Here is a version using Bigarray to allocate such a protected region:

module Sopt : sig
  type +'a t
  val none : 'a t
  val some : 'a -> 'a t
  val is_none : 'a t -> bool
  val arg : 'a t -> 'a
  val is_sopt : 'a t -> bool
  val depth : 'a t -> int
end = struct
  type 'a t = int
  let area = Bigarray.(Array1.create int32 c_layout 1024)
  let none : int = Obj.obj (Obj.field (Obj.repr area) 1)
  let is_none x = (x = none)
  let is_sopt x = (x >= none) && (x < none + 2048)
  let some (x : 'a) : 'a t =
    let y : 'a t = Obj.magic x in
    if is_sopt y then
      if y = none + 2047 then invalid_arg "Sopt.some" else y + 2
    else y
  let arg (x : 'a t) : 'a =
    if is_sopt x then
      if is_none x then invalid_arg "Sopt.arg" else Obj.magic (x-2)
    else Obj.magic x
  let depth x =
    if is_sopt x then ((x - none) lor 1) lsr 1 else -1
end

> The implementation relies on specific aspect of the compiler to
> construct those values. I would give it a 99% chance to fail with an
> llvm backend for ocaml for example. Using C stubs that directly
> manipulate the bits seems a better approach.
> 
> For example nothing says x + 2 can't be implemented as
> 
> value add(value x, value y) {
>    return (x & ~1) + y;
> }
> 
> as opposed to
> 
> value add(value x, value y) {
>    return x + y - 1;
> }


Actually I'm confident that any backend using a data representation compatible
with ocaml is going to implement addition the same way.
There are two reasons:
* most processors can add two registers and a small constant in one operation
* there is no reason to depart from the already published approach

But of course there is nothing wrong to writing those as C primitives if you
are already writing stubs. You might just want to add the "noalloc" qualifier
to make calling them more efficient.

	Jacques

Re: [Caml-list] A shallow option type

[Jacques Garrigue]

Here is another variant using normal values.
The advantage is that it does no tricks with bits, and supports
marshaling.
It is less efficient because the search is linear, but by using as
tag (lazy_tag -1) we can avoid being too inefficient in most cases.
Note however that after marshaling the values are going to
have the same tag, so this is going to be much less efficient.

Jacques

module Sopt : sig
  type +'a t
  val none : 'a t
  val some : 'a -> 'a t
  val is_none : 'a t -> bool
  val arg  : 'a t -> 'a
  val depth : 'a t -> int
end = struct
  type 'a t = Obj.t
  let sopt_tag = Obj.lazy_tag - 1
  let none = Obj.new_block sopt_tag 0
  let last = 255
  let area = Array.create (last+1) none
  let () =
    for i = 1 to last do
      let stub = Obj.new_block sopt_tag 1 in
      Obj.set_field stub 0 area.(i-1);
      area.(i) <- stub
    done
  let is_none x = (x == none)
  let rec some_aux x i =
    if i < last then
      if x == area.(i) then area.(i+1) else some_aux x (i+1)
    else (* i = last *)
      if x == area.(last) then invalid_arg "Sopt.some" else x
  let some (x : 'a) : 'a t =
    let x = Obj.repr x in
    if Obj.is_int x || Obj.tag x <> sopt_tag then Obj.obj x
    else Obj.obj (some_aux x 0)
  let rec arg_aux x i =
    if i <= last then
      if x == area.(i) then area.(i-1) else arg_aux x (i+1)
    else
      if x == area.(0) then invalid_arg "Sopt.arg" else x
  let arg (x : 'a t) : 'a =
    let x = Obj.repr x in
    if Obj.is_int x || Obj.tag x <> sopt_tag then Obj.obj x
    else Obj.obj (arg_aux x 1)
  let rec depth_aux x i =
    if i <= last then
      if x == area.(i) then i else depth_aux x (i+1)
    else -1
  let depth x = depth_aux (Obj.repr x) 0
end

Re: [Caml-list] A shallow option type

[Jacques Garrigue]

Sorry, the marshaling part was wrong.
Of course we need to do something about received values.
So here is a version that automatically attempts to internalize values
with tag sopt_tag when we apply either some or arg to them.
This should be safe, as if sopt_tag was used for another
type, this should be in a functional way.

	Jacques

module Sopt : sig
 type +'a t
 val none : 'a t
 val some : 'a -> 'a t
 val is_none : 'a t -> bool
 val arg  : 'a t -> 'a
 val intern : 'a t -> 'a t
 val depth : 'a t -> int
end = struct
 type 'a t = Obj.t
 let sopt_tag = Obj.lazy_tag - 1
 let none = Obj.new_block sopt_tag 0
 let last = 31
 let area = Array.create (last+1) none
 let () =
   for i = 1 to last do
     let stub = Obj.new_block sopt_tag 1 in
     Obj.set_field stub 0 area.(i-1);
     area.(i) <- stub
   done
 let is_none x = (x == none)
 let rec intern_aux x i =
   if i > last || Obj.is_int x || Obj.tag x <> sopt_tag || Obj.size x > 1 then
     invalid_arg "Sopt.intern"
   else
     if Obj.size x = 0 then i else intern_aux (Obj.field x 0) (i+1)
 let intern x = Obj.obj area.(intern_aux (Obj.repr x) 0)
 let rec some_aux x i =
   if i < last then
     if x == area.(i) then area.(i+1) else some_aux x (i+1)
   else (* i = last *)
     if x == area.(last) then invalid_arg "Sopt.some" else
     let i = intern_aux x 0 in
     if i >= last then invalid_arg "Sopt.some" else area.(i+1)
 let some (x : 'a) : 'a t =
   let x = Obj.repr x in
   if Obj.is_int x || Obj.tag x <> sopt_tag then Obj.obj x
   else Obj.obj (some_aux x 0)
 let rec arg_aux x i =
   if i <= last then
     if x == area.(i) then area.(i-1) else arg_aux x (i+1)
   else
     if x == area.(0) then invalid_arg "Sopt.arg" else
     let i = intern_aux x 0 in
     if i = 0 then invalid_arg "Sopt.arg" else area.(i-1)
 let arg (x : 'a t) : 'a =
   let x = Obj.repr x in
   if Obj.is_int x || Obj.tag x <> sopt_tag then Obj.obj x
   else Obj.obj (arg_aux x 1)
 let rec depth_aux x i =
   if i <= last then
     if x == area.(i) then i else depth_aux x (i+1)
   else -1
 let depth x = depth_aux (Obj.repr x) 0
end


On 2012/05/07, at 10:27, Jacques Garrigue wrote:

> Here is another variant using normal values.
> The advantage is that it does no tricks with bits, and supports
> marshaling.
> It is less efficient because the search is linear, but by using as
> tag (lazy_tag -1) we can avoid being too inefficient in most cases.
> Note however that after marshaling the values are going to
> have the same tag, so this is going to be much less efficient.
> 
> Jacques

[...]

Re: [Caml-list] A shallow option type

[Jacques Garrigue]

Sorry for all these mails.
Looks like I don't think well when I'm sleepy...

Anyway, I think that at last I have a reasonable (much simpler) solution.
This still uses sopt_tag (i.e. lazy_tag-1), but this time the argument is
the number of "some" constructors, so there is no extra cost for marshaling.
The only values on which Sopt.some is not the identity are those with a
single argument, which is additionally represented by an integer between 0 and last.
Moreover, even if for some reason you build such a value using a real sum
type, you still have Sopt.arg (Sopt.some v) = v, the only change being a loss
of sharing (which is anyway not guaranteed by the ocaml specification).

Jacques

module Sopt : sig
 type +'a t
 val none : 'a t
 val some : 'a -> 'a t
 val is_none : 'a t -> bool
 val arg  : 'a t -> 'a
 val depth : 'a t -> int
end = struct
 type 'a t = Obj.t
 let sopt_tag = Obj.lazy_tag - 1
 let none = Obj.new_block sopt_tag 1
 let last = 255
 let area = Array.create (last+1) none
 let () =
   Obj.set_field none 0 (Obj.repr 0);
   for i = 1 to last do
     let stub = Obj.new_block sopt_tag 1 in
     Obj.set_field stub 0 (Obj.repr i);
     area.(i) <- stub
   done
 let is_none x = (x = none)
 let is_sopt x =
   Obj.is_block x && Obj.tag x = sopt_tag && Obj.size x = 1 &&
   let i = Obj.obj (Obj.field x 0) in i >= 0 && i <= last
 let depth x =
   let x = Obj.repr x in
   if is_sopt x then Obj.obj (Obj.field x 0) else -1
 let some (x : 'a) : 'a t =
   let i = depth x in
   if i < 0 then Obj.magic x else
   if i = last then invalid_arg "Sopt.some" else Obj.obj area.(i+1)
 let arg (x : 'a t) : 'a =
   let i = depth x in
   if i < 0 then Obj.magic x else
   if i = 0 then invalid_arg "Sopt.arg" else Obj.obj area.(i-1)
end

Re: [Caml-list] A shallow option type

[Goswin von Brederlow]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:

> Sorry for all these mails.
> Looks like I don't think well when I'm sleepy...
>
> Anyway, I think that at last I have a reasonable (much simpler) solution.
> This still uses sopt_tag (i.e. lazy_tag-1), but this time the argument is
> the number of "some" constructors, so there is no extra cost for marshaling.
> The only values on which Sopt.some is not the identity are those with a
> single argument, which is additionally represented by an integer between 0 and last.
> Moreover, even if for some reason you build such a value using a real sum
> type, you still have Sopt.arg (Sopt.some v) = v, the only change being a loss
> of sharing (which is anyway not guaranteed by the ocaml specification).
>
> Jacques
>
> module Sopt : sig
>  type +'a t
>  val none : 'a t
>  val some : 'a -> 'a t
>  val is_none : 'a t -> bool
>  val arg  : 'a t -> 'a
>  val depth : 'a t -> int
> end = struct
>  type 'a t = Obj.t
>  let sopt_tag = Obj.lazy_tag - 1
>  let none = Obj.new_block sopt_tag 1
>  let last = 255
>  let area = Array.create (last+1) none
>  let () =
>    Obj.set_field none 0 (Obj.repr 0);
>    for i = 1 to last do
>      let stub = Obj.new_block sopt_tag 1 in
>      Obj.set_field stub 0 (Obj.repr i);
>      area.(i) <- stub
>    done
>  let is_none x = (x = none)
>  let is_sopt x =
>    Obj.is_block x && Obj.tag x = sopt_tag && Obj.size x = 1 &&
>    let i = Obj.obj (Obj.field x 0) in i >= 0 && i <= last
>  let depth x =
>    let x = Obj.repr x in
>    if is_sopt x then Obj.obj (Obj.field x 0) else -1
>  let some (x : 'a) : 'a t =
>    let i = depth x in
>    if i < 0 then Obj.magic x else
>    if i = last then invalid_arg "Sopt.some" else Obj.obj area.(i+1)
>  let arg (x : 'a t) : 'a =
>    let i = depth x in
>    if i < 0 then Obj.magic x else
>    if i = 0 then invalid_arg "Sopt.arg" else Obj.obj area.(i-1)
> end

What exactly is the point of specially tagged blocks? All you need is a
bunch of pointers to values to encode the depth. You can use the value
pointed at to encode the index the pointer is at and physical equality
to ensure it actualy is one of your pointers:

let area = Array.init (last+1) (fun i -> ref i)

let is_sopt x =
  let r = Obj.repr x in
  Obj.is_block r && Obj.size x = 1 && Obj.is_int (Obj.field r 0) &&
  let i = Obj.obj (Obj.field r 0) in
  i >= 0 && i <= last && Obj.obj r == area.(i)

# is_sopt 1;;
- : bool = false
# is_sopt area.(5);;
- : bool = true
# is_sopt (ref 5);;
- : bool = false

MfG
        Goswin

Re: [Caml-list] A shallow option type

[Jacques Garrigue]

On 2012/05/08, at 2:08, Goswin von Brederlow <goswin-v-b@web.de> wrote:

> Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
>
>> Sorry for all these mails.
>> Looks like I don't think well when I'm sleepy...
>>
>> Anyway, I think that at last I have a reasonable (much simpler) solution.
>> This still uses sopt_tag (i.e. lazy_tag-1), but this time the argument is
>> the number of "some" constructors, so there is no extra cost for marshaling.
>> The only values on which Sopt.some is not the identity are those with a
>> single argument, which is additionally represented by an integer between 0 and last.
>> Moreover, even if for some reason you build such a value using a real sum
>> type, you still have Sopt.arg (Sopt.some v) = v, the only change being a loss
>> of sharing (which is anyway not guaranteed by the ocaml specification).
>>
>> Jacques
>>
>> module Sopt : sig
>> type +'a t
>> val none : 'a t
>> val some : 'a -> 'a t
>> val is_none : 'a t -> bool
>> val arg  : 'a t -> 'a
>> val depth : 'a t -> int
>> end = struct
>> type 'a t = Obj.t
>> let sopt_tag = Obj.lazy_tag - 1
>> let none = Obj.new_block sopt_tag 1
>> let last = 255
>> let area = Array.create (last+1) none
>> let () =
>>   Obj.set_field none 0 (Obj.repr 0);
>>   for i = 1 to last do
>>     let stub = Obj.new_block sopt_tag 1 in
>>     Obj.set_field stub 0 (Obj.repr i);
>>     area.(i) <- stub
>>   done
>> let is_none x = (x = none)
>> let is_sopt x =
>>   Obj.is_block x && Obj.tag x = sopt_tag && Obj.size x = 1 &&
>>   let i = Obj.obj (Obj.field x 0) in i >= 0 && i <= last
>> let depth x =
>>   let x = Obj.repr x in
>>   if is_sopt x then Obj.obj (Obj.field x 0) else -1
>> let some (x : 'a) : 'a t =
>>   let i = depth x in
>>   if i < 0 then Obj.magic x else
>>   if i = last then invalid_arg "Sopt.some" else Obj.obj area.(i+1)
>> let arg (x : 'a t) : 'a =
>>   let i = depth x in
>>   if i < 0 then Obj.magic x else
>>   if i = 0 then invalid_arg "Sopt.arg" else Obj.obj area.(i-1)
>> end
>
> What exactly is the point of specially tagged blocks? All you need is a
> bunch of pointers to values to encode the depth. You can use the value
> pointed at to encode the index the pointer is at and physical equality
> to ensure it actualy is one of your pointers:
>
> let area = Array.init (last+1) (fun i -> ref i)
>
> let is_sopt x =
>  let r = Obj.repr x in
>  Obj.is_block r && Obj.size x = 1 && Obj.is_int (Obj.field r 0) &&
>  let i = Obj.obj (Obj.field r 0) in
>  i >= 0 && i <= last && Obj.obj r == area.(i)

Marshaling.
Without the distinctive tag, there is no way to know that a value you receive
was a special one.
Without the marshaling requirement there are indeed many solutions.
Also I should be honest, and point that my solution does interfere with some
values of tag sopt_tag. Namely, applying Sopt.some to the block
(sopt_tag, last) is going to fail whereas it might be representing a perfectly
safe value. But this looks like a very exceptional condition.
If you don't need marshaling, you can use your stronger criterion to avoid
any interference. Using a special tag still allows a faster test.

Jacques