From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q46DCO8S032489 for ; Sun, 6 May 2012 15:12:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlgBANt3pk/RVdU2kGdsb2JhbABEoG6RdQgiAQEBAQkJDQcUBCOCDAEBAQQSAhMZARsSCwEDDAYFCw0NISIBEQEFAQoSBhMSEIddAQMLC5tuCQOMJIJzhBMKGScDChVCiHYBBQuKdIYgBJV+gRGNUT2EDg X-IronPort-AV: E=Sophos;i="4.75,538,1330902000"; d="scan'208";a="156943880" Received: from mail-yw0-f54.google.com ([209.85.213.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 06 May 2012 15:12:18 +0200 Received: by yhgm50 with SMTP id m50so4918216yhg.27 for ; Sun, 06 May 2012 06:12:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=uha4zSq82c7Z1a23dFOmYGVQB0pgG031KcUf5ZEfnqA=; b=Yzdb8OTkLpaoEGPno30GifN6tGmM7OwR3j/juLRYV4nnuFhr1Mwg2YPlBDpDvf22n5 FTvD618Lb1XS/PnEDRh+Ii0sqXzGygI/o/GH85jmohfvP5LPZ/Fsy2Qc7uaHtodUE1X0 u0yufafMcWoxBHdAAjwhOlH2UtRDGlCZpI5kQ7QIjSUsNzNQzG/mPYEnXyaq2N/ubeNn HOwMl91CgL8UN0KqbAXjBU4wzbNqdUnGb4ghyA5rhc8MwsqYmOI6gvu2Ef05kHqM1PQm 2M1z8bO2okK9G4tjf1muoqA62uH2f0Jjc0K1qqarZFoGjG14anqodS8KzDa+UkoWcd1c r1tQ== Received: by 10.50.135.4 with SMTP id po4mr6490299igb.60.1336309937319; Sun, 06 May 2012 06:12:17 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.140.100 with HTTP; Sun, 6 May 2012 06:11:37 -0700 (PDT) In-Reply-To: <87sjfd31z9.fsf@frosties.localnet> References: <87sjfd31z9.fsf@frosties.localnet> From: Gabriel Scherer Date: Sun, 6 May 2012 15:11:37 +0200 Message-ID: To: Goswin von Brederlow Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q46DCO8S032489 Subject: Re: [Caml-list] Implementation for a (nearly) typesafe shallow option type and a compiler bug? 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 wrote: > 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 >