[Caml-list] Implementation for a (nearly) typesafe shallow option type and a compiler bug?

[Goswin von Brederlow]

Hi,

as mentioned earlier I wanted to have a

type 'a shallow = NULL | 'a

that is like an 'a option but without the indirection.

The first idea was that no ocaml value can be the C NULL pointer (usualy
all bits set to 0) and the C NULL pointer points outside the ocaml heap
so the GC is fine with that too. So NULL could be encoded as C NULL
pointer and 'a used as is.

First problem is that this does not work for an 'a shallow shallow. And
there is no way to constrain 'a to not be a 'b shallow in the type
definition.

Second problem is that someone else might define a 'a shallow2 type with
the same idea and 'a shallow2 shallow would also not work. And with
abstract types it would be impossible to test for that even if ocaml
would allow negative constraints.


The common problem here is that NULL is not unique for each type. So I
thought of a way to make it unique. What I came up with is using a
functor to create a unique NULL value for each instance. Source code at
the end.

Output:
NULL -> None
Some 5 -> Some 5
NULL -> None
Some NULL -> Some None
Some Some 5 -> Some Some 5
1 2 3 4
a b c d
NULL -> Some 70221466564508

As you can see from the output this solves the problem of 'a shallow
shallow and would also solve the 'a shallow2 shallow case.

But in the last line a new problem appears. Each instance of the functor
has a unique NULL element. But instances of the functor with the same
type are compatible. So an IntShallow2.t can be used instead of an
IntShallow.t but then the NULL does not match.

To me this looks like a bug in ocaml because the resulting type of the
functor application does not match the type I specified for the functor:

module type SHALLOW =
sig
type -'a t
val null : 'a t
val make : 'a -> 'a t
val as_option : 'a t -> 'a option
end
module Make : functor (Type : TYPE) -> SHALLOW

module IntShallow2 :
sig
type 'a t = 'a Shallow.Make(Int).t
val null : 'a t
val make : 'a -> 'a t
val as_option : 'a t -> 'a option
end

The type I specified has 'a t abstract while the IntShallow2 has the
type 'a t more concret.

Restricting the type to what it should already be results in the correct
error:

module IntShallow2 = (Shallow.Make(Int) : Shallow.SHALLOW)
let () =
Printf.printf "NULL -> %s\n" (to_string (IntShallow2.null))

File "shallow.ml", line 91, characters 42-60:
Error: This expression has type 'a IntShallow2.t
but an expression was expected of type
int IntShallow.t = int Shallow.Make(Int).t

Why is that?

MfG
Goswin

======================================================================
module Shallow : sig
module type TYPE = sig type 'a t end
module type SHALLOW =
sig
type -'a t
val null : 'a t
val make : 'a -> 'a t
val as_option : 'a t -> 'a option
end
module type SHALLOWFUNCTOR = functor (Type : TYPE) -> SHALLOW
module Make : functor (Type : TYPE) -> SHALLOW
end = struct
module type TYPE = sig type 'a t end
module type SHALLOW =
sig
type -'a t
val null : 'a t
val make : 'a -> 'a t
val as_option : 'a t -> 'a option
end
module type SHALLOWFUNCTOR = functor (Type : TYPE) -> SHALLOW

module Make_intern =
functor (Type : TYPE) ->
struct
type -'a t
(* Dummy object unique to the type *)
let null = Obj.magic (ref 0)
let make x = Obj.magic x
let as_option x = if x == null then None else Some (Obj.magic x)
end
module Make = (Make_intern : functor (Type : TYPE) -> SHALLOW)
end

module Int = struct type 'a t = int end

module IntShallow = Shallow.Make(Int)
module IntShallowShallow = Shallow.Make(IntShallow)

let to_string x =
match IntShallow.as_option x with
| None -> "None"
| Some x -> Printf.sprintf "Some %d" x

let to_string2 x =
match IntShallowShallow.as_option x with
| None -> "None"
| Some x -> Printf.sprintf "Some %s" (to_string x)

module List = struct
module Item = struct
type 'a t = 'a
end

module Shallow = Shallow.Make(Item)

type 'a item = { mutable next : 'a list; data : 'a; }
and 'a list = 'a item Shallow.t

let null = Shallow.null
let cons x y = Shallow.make { next = y; data = x; }
let rec iter fn x =
match Shallow.as_option x with
| None -> ()
| Some { next; data; } -> fn data; iter fn next
end

let () =
Printf.printf "NULL -> %s\n" (to_string (IntShallow.null));
Printf.printf "Some 5 -> %s\n" (to_string (IntShallow.make 5));
Printf.printf "NULL -> %s\n" (to_string2 (IntShallowShallow.null));
Printf.printf "Some NULL -> %s\n"
(to_string2 (IntShallowShallow.make IntShallow.null));
Printf.printf "Some Some 5 -> %s\n"
(to_string2 (IntShallowShallow.make (IntShallow.make 5)));
let x = List.null in
let x = List.cons 4 x in
let x = List.cons 3 x in
let x = List.cons 2 x in
let x = List.cons 1 x in
List.iter (Printf.printf "%d ") x;
print_newline ();
let y = List.null in
let y = List.cons "d" y in
let y = List.cons "c" y in
let y = List.cons "b" y in
let y = List.cons "a" y in
List.iter (Printf.printf "%s ") y;
print_newline ()

module IntShallow2 = Shallow.Make(Int)

let () =
Printf.printf "NULL -> %s\n" (to_string (IntShallow2.null))

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

[Gabriel Scherer]

What you observe is the so-called "strengthening" of type equalities
in functor applications. See papers 5 or 6 in this list:
http://caml.inria.fr/about/papers.en.html

It is not a bug, but a feature: you can write functors F such that
applying F(X) twice yields compatible, rather than incompatible,
types. If you want to recover incompatible types, you can seal the
functor result as you did in your workaround, or pass a non-path
functor expression (that behave in a more generative way): F(struct
include X end).

On your more general code:
- I do not understand why you specify the abstract type ('a t) to be
contravariant, and I suspect this will be unsound (is an (< m : int >
t) also an (< m : int; s : string > t)?)
- I am not sure using (Obj.magic (ref 0)) is safe wrt. types whose
representation is not always a pointer (ie. floats)

On Sun, May 6, 2012 at 2:53 PM, Goswin von Brederlow <goswi...@web.de> wrote:
> Hi,
>
> as mentioned earlier I wanted to have a
>

> á átype 'a shallow = NULL | 'a

> ámodule type SHALLOW =
> á ásig
> á á átype -'a t
> á á ával null : 'a t
> á á ával make : 'a -> 'a t
> á á ával as_option : 'a t -> 'a option
> á áend
> ámodule Make : functor (Type : TYPE) -> SHALLOW
>
> module IntShallow2 :
> ásig
> á átype 'a t = 'a Shallow.Make(Int).t
> á ával null : 'a t
> á ával make : 'a -> 'a t
> á ával as_option : 'a t -> 'a option
> áend

>
> The type I specified has 'a t abstract while the IntShallow2 has the
> type 'a t more concret.
>
> Restricting the type to what it should already be results in the correct
> error:
>
> module IntShallow2 = (Shallow.Make(Int) : Shallow.SHALLOW)
> let () =

> áPrintf.printf "NULL -> %s\n" (to_string (IntShallow2.null))

>
> File "shallow.ml", line 91, characters 42-60:
> Error: This expression has type 'a IntShallow2.t

> á á á but an expression was expected of type
> á á á á int IntShallow.t = int Shallow.Make(Int).t
>
> Why is that?
>
> MfG
> á á á áGoswin
>
> ======================================================================
> module Shallow : sig
> ámodule type TYPE = sig type 'a t end
> ámodule type SHALLOW =
> á ásig
> á á átype -'a t
> á á ával null : 'a t
> á á ával make : 'a -> 'a t
> á á ával as_option : 'a t -> 'a option
> á áend
> ámodule type SHALLOWFUNCTOR = functor (Type : TYPE) -> SHALLOW
> ámodule Make : functor (Type : TYPE) -> SHALLOW
> end = struct
> ámodule type TYPE = sig type 'a t end
> ámodule type SHALLOW =
> á ásig
> á á átype -'a t
> á á ával null : 'a t
> á á ával make : 'a -> 'a t
> á á ával as_option : 'a t -> 'a option
> á áend
> ámodule type SHALLOWFUNCTOR = functor (Type : TYPE) -> SHALLOW
>
> ámodule Make_intern =
> á áfunctor (Type : TYPE) ->
> á á ástruct
> á á á átype -'a t
> á á á á(* Dummy object unique to the type *)
> á á á álet null = Obj.magic (ref 0)
> á á á álet make x = Obj.magic x
> á á á álet as_option x = if x == null then None else Some (Obj.magic x)
> á á áend
> ámodule Make = (Make_intern : áfunctor (Type : TYPE) -> SHALLOW)

> end
>
> module Int = struct type 'a t = int end
>
> module IntShallow = Shallow.Make(Int)
> module IntShallowShallow = Shallow.Make(IntShallow)
>
> let to_string x =

> ámatch IntShallow.as_option x with
> á á| None -> "None"
> á á| Some x -> Printf.sprintf "Some %d" x
>
> let to_string2 x =
> ámatch IntShallowShallow.as_option x with
> á á| None -> "None"
> á á| Some x -> Printf.sprintf "Some %s" (to_string x)
>
> module List = struct
> ámodule Item = struct
> á átype 'a t = 'a
> áend
>
> ámodule Shallow = Shallow.Make(Item)
>
> átype 'a item = { mutable next : 'a list; data : 'a; }
> áand 'a list = 'a item Shallow.t
>
> álet null = Shallow.null
> álet cons x y = Shallow.make { next = y; data = x; }
> álet rec iter fn x =
> á ámatch Shallow.as_option x with
> á á á| None -> ()
> á á á| Some { next; data; } -> fn data; iter fn next
> end
>
> let () =
> áPrintf.printf "NULL -> %s\n" (to_string (IntShallow.null));
> áPrintf.printf "Some 5 -> %s\n" (to_string (IntShallow.make 5));
> áPrintf.printf "NULL -> %s\n" (to_string2 (IntShallowShallow.null));
> áPrintf.printf "Some NULL -> %s\n"
> á á(to_string2 (IntShallowShallow.make IntShallow.null));
> áPrintf.printf "Some Some 5 -> %s\n"
> á á(to_string2 (IntShallowShallow.make (IntShallow.make 5)));
> álet x = List.null in
> álet x = List.cons 4 x in
> álet x = List.cons 3 x in
> álet x = List.cons 2 x in
> álet x = List.cons 1 x in
> áList.iter (Printf.printf "%d ") x;
> áprint_newline ();
> álet y = List.null in
> álet y = List.cons "d" y in
> álet y = List.cons "c" y in
> álet y = List.cons "b" y in
> álet y = List.cons "a" y in
> áList.iter (Printf.printf "%s ") y;
> áprint_newline ()

>
> module IntShallow2 = Shallow.Make(Int)
>
> let () =

> áPrintf.printf "NULL -> %s\n" (to_string (IntShallow2.null))
>
> --
> Caml-list mailing list. áSubscription management and archives:

[Goswin von Brederlow]

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

> What you observe is the so-called "strengthening" of type equalities
> in functor applications. See papers 5 or 6 in this list:
> http://caml.inria.fr/about/papers.en.html
>
> It is not a bug, but a feature: you can write functors F such that
> applying F(X) twice yields compatible, rather than incompatible,
> types. If you want to recover incompatible types, you can seal the
> functor result as you did in your workaround, or pass a non-path
> functor expression (that behave in a more generative way): F(struct
> include X end).

Good to know. I found that surprising. I think it is bad that you can't
specify the type of the functor so that both compatible and incompatible
types would be an option. Just like you can use 'a, +'a and -'a to fine
tune variance in types there could be some syntax to make the functor
type strengthened or not.

> On your more general code:
> - I do not understand why you specify the abstract type ('a t) to be
> contravariant, and I suspect this will be unsound (is an (< m : int >
> t) also an (< m : int; s : string > t)?)

Left over from trying to make the functor type not strengthened.

> - I am not sure using (Obj.magic (ref 0)) is safe wrt. types whose
> representation is not always a pointer (ie. floats)

(Obj.magic (ref 0)) is always a pointer that is unique to the instance
of the functor. No other value can legally have this bit pattern.

As for floats: Manual 18.3.1 Atomic types

Caml type Encoding
float Blocks with tag Double_tag.

A float is always a pointer and that can't be legally pointing to our
(Obj.magic (ref 0)).

MfG
Goswin

[Richard W.M. Jones]

On Sun, May 06, 2012 at 02:53:14PM +0200, Goswin von Brederlow wrote:
> The common problem here is that NULL is not unique for each type. So I
> thought of a way to make it unique.

I don't know whether or not it'll solve your problem, but there is
another way to generate unique pointers that the OCaml runtime won't
follow. That is, in C create a pointer to some static item:

static char foo;
value get_null (value ignored) { return &foo; }

external get_null : unit -> null = "get_null" "noalloc"

Rich.

--
Richard Jones
Red Hat

[Richard W.M. Jones]

OK! I guess I should read back over the earlier thread first ...