private rows question

private rows question

[Keiko Nakata]

Hello.

Why the following functor G is not typable?
I thought that g could have a type something like int -> [< `A | `B ].

module G(X:sig type t = private [< `A ] val f : int -> t end) = struct
  let g x = if x = 0 then `B else X.f x 
end

This question comes from a wish to reuse my program codes 
using private rows in the following way:
(In my actual program, each branches of the function g of F 
performs much more verbose task. Thus, writing duplicate codes 
is a bit painful.)


module F(X:sig 
  type t = private [< `A | `B | `C] 
  val f : [`III of string] -> t   end) =
  struct
    let rec g binds = function
	[] -> []
      | `Var name :: tl -> (List.assoc name binds) :: (g binds tl)
      | (`I name) :: tl -> `A :: (g ((name, `A) :: binds) tl)
      | (`II name) :: tl -> `B :: (g ((name, `B) :: binds ) tl)
      | (`III _ as iii) :: tl  -> 
	  let iii' = X.f iii in
	  iii' :: (g ((name, iii') :: binds) tl)
  end

module ABC = struct 
  type t = [`A | `B | `C]
  let f = function `III name -> `C
end


module AB = struct
  type t = [`A | `B]
  let f = function `III name -> `A
end

module FABC = F(ABC)
module FAB = F(AB)

let abc : [`I | `II | `III] list -> [`A | `B | `C] list = FABC.g
      
let ab : [`I | `II | `III] list -> [`A | `B ] list = FBC.g


I thought that the reuse might be possible 
by making the function g take the function f as an argument, as in follows:


let rec g f binds = function
    [] -> []
  | `Var name :: tl -> (List.assoc name binds) :: (g f binds tl)
  | (`I name) :: tl -> `A :: (g f ((name, `A) :: binds) tl)
  | (`II name) :: tl -> `B :: (g f ((name, `B) :: binds ) tl)
  | (`III name as iii) :: tl  -> 
      let iii' = f iii in
      iii' :: (g f ((name, iii') :: binds) tl)

let f = function `III name -> `C
let abc binds ls  : [ `A | `B | `C]  = g f binds ls

However, this attempt also failed...
(Anyway, I do not find the addition of f to g's arguments pleasant,
since this could increase the number of g's formal parameters 
unnecessarily when I define more complicated functions.)



Best regards,
Keiko NAKATA

Re: [Caml-list] private rows question

[Jacques Garrigue]

From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>

> Why the following functor G is not typable?
> I thought that g could have a type something like int -> [< `A | `B ].
> 
> module G(X:sig type t = private [< `A ] val f : int -> t end) = struct
>   let g x = if x = 0 then `B else X.f x 
> end

Since g may return `B, and probably `A (the probably concerns your
intention), the expected type would be
  g : int -> [> `A | `B ]
Next, if you want f to have a private row type, then you should
disconnect its type from the type of g (otherwise the type of g must
be the same as f.) So I would expect something like:
   let g x = if x = 0 then `B else (X.f x : [< `A] :> [> `A])

Jacques

Re: [Caml-list] private rows question

[Keiko Nakata]

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

> From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>
> 
> > Why the following functor G is not typable?
> > I thought that g could have a type something like int -> [< `A | `B ].
> > 
> > module G(X:sig type t = private [< `A ] val f : int -> t end) = struct
> >   let g x = if x = 0 then `B else X.f x 
> > end
> 
> Since g may return `B, and probably `A (the probably concerns your
> intention), the expected type would be
>   g : int -> [> `A | `B ]
> Next, if you want f to have a private row type, then you should
> disconnect its type from the type of g (otherwise the type of g must
> be the same as f.) So I would expect something like:
>    let g x = if x = 0 then `B else (X.f x : [< `A] :> [> `A])

Thank you for the correction.
Obviously, the type checker is much more brilliant than me :-)
Private rows seem to give me more opportunities to reuse my program codes
than I expected.

Keiko NAKATA

Re: [Caml-list] again private rows question

[Keiko Nakata]

Sorry, again...

What is the difference beteen the functor F and the function f ?
(F is not typable, but f is)

module F(X:sig  
  type t = private [< `A | `B | `C ]
  val f : [`III ] -> t end) = 
  struct
    let rec g  = function
	[] -> []
      | `I  :: tl -> `A :: (g tl)
      | `II :: tl -> `B :: (g  tl)
      | (`III as iii) :: tl  -> 
	  let iii' = (X.f iii : [< `A | `B | `C ] :> [> `A | `B ]) in
	  iii' :: (g tl)
  end


let f (x : [< `A | `B | `C]) = (x : [< `A | `B | `C] :> [> `A | `B]);;

I also curious to know whether there is a way to 
make g's type depend on X.t in 

module G(X:sig type t = private [< `A ] val f : int -> t end) = struct
  let g x = if x = 0 then `B else X.f x 
end


Regards, 
Keiko NAKATA