Subtyping

Subtyping

[Goswin von Brederlow]

Hi,

In the last 2 weeks I've been playing around with lots of different
ways to do the same thing to get a feel for what style suites me
best. If you have improvements or alternative ways of doing the two
things below let me know.


One of the things was trying to build a type hierachy with
coercion and subtyping.

The obvious case would be ocaml objects:

class base = object val x = 0 method print_x = print_int x end
class foo = object inherit base val y = 1 method print_y = print_int y end
let print_x o = o#print_x
let _ =
  print_x (new base); print_newline ();
  print_x (new foo); print_newline ();;


So what other ways are there of doing this? Records. Idealy I would
like to do this:

type base = { x : int }
let make_base x = { x = x }
let print_x r = print_int r.x
type foo = { base with y : int }
let make_foo x y = { x = x; y = y }
let _ =
  print_x (make_base 0); print_newline ();
  print_x (make_foo 0 1); print_newline ();;

Ocaml has no way of making this work like that, right?


But lets look at things that actually work:
(Some examples are more complicated than needed here but think about
what happens with mutables and multiple methods)

1) Magic

type base = { x : int }
let make_base x = { x = x }
let print_x r = print_int r.x
type foo = { x : int; y : int }
let make_foo x y = { x = x; y = y }
let as_base : foo -> base = Obj.magic
let _ =
  print_x (make_base 0); print_newline ();
  print_x (as_base (make_foo 0 1)); print_newline ();;

2) Polymorphic records

type 'a base = { x: int; y : 'a }
let make_a_base x y = { x = x; y = y }
let make_base x = make_a_base x ()
let print_x r = print_int r.x
type foo = int base
let make_foo x y = (make_a_base x y : foo)
let _ =
  print_x (make_base 0); print_newline ();
  print_x (make_foo 0 1); print_newline ();;

This wastest memory though if there are many base objects.

3) Closure records

type base_data = { x : int }
type base = { print_x : unit -> unit }
let make_base_fn print_x = { print_x = print_x }
let make_base x =
  let data = ref { x = x }
  in
    make_base_fn (fun () -> print_int !data.x)
let print_x r = r.print_x ()
type foo_data = { x : int; y : int }
type foo = { print_x : unit -> unit; print_y : unit -> unit }
let make_foo_fn print_x print_y = { print_x = print_x; print_y = print_y }
let make_foo x y =
  let data = ref { x = x; y = y }
  in
    make_foo_fn (fun () -> print_int !data.x) (fun () -> print_int !data.y)
let as_base foo = make_base_fn foo.print_x
let _ =
  print_x (make_base 0); print_newline ();
  print_x (as_base (make_foo 0 1)); print_newline ();;

This wastest memory for the reference and per object for every closure
being bound to it.

4) Combining 1+2+3 for a memory efficient heterogeneous type:

type 'a base_funs = { print : 'a base -> unit }
and 'a base = { x: int; y : 'a; funs : 'a base_funs }
let make_a_base x y funs = { x = x; y = y; funs = funs }
let unit_base_funs = { print = (fun (r : unit base) -> print_int r.x) }
let make_base x = make_a_base x () unit_base_funs
let print r = r.funs.print r
type foo = int base
let foo_funs = { print = fun r -> Printf.printf "%d %d" r.x r.y }
let make_foo x y = ((make_a_base x y foo_funs) : foo)
let as_base : foo -> unit base = Obj.magic
let lst = [make_base 0; as_base (make_foo 0 1)] in
  List.iter (fun r -> print r; print_newline ()) lst




Lets look another thing going in a similar direction. I want to
have a structure where I can store key value pairs. But just for fun
lets say I want to store values of different types and the key knows
the type of value. In short a heterogeneous associative container:

exception TypeError
type kind = Int | Float
class virtual key = object(self)
  val virtual x : int
  method x = x
  method virtual kind : kind
  method as_key = (self :> key)
  method compare : 'a. (<as_key : key; ..> as 'a) -> int =
   function o ->
    let o = o#as_key
    in
      Pervasives.compare (self#kind, self#x) (o#kind, o#x)
end
class int_key x_init = object
  inherit key
  val x = x_init
  method kind = Int
  method int_foo = 0
end
class float_key x_init = object
  inherit key
  val x = x_init
  method kind = Float
  method float_foo = 0
end
class virtual key_data = object
  inherit key
  method virtual as_int : int_key_data
  method virtual as_float : float_key_data
end
and int_key_data x_init i_init = object(self)
  inherit int_key x_init
  inherit key_data
  val i = i_init
  method i : int = i
  method as_int = (self :> int_key_data)
  method as_float = raise TypeError
end
and float_key_data x_init f_init = object(self)
  inherit float_key x_init
  inherit key_data
  val f : float = f_init
  method f = f
  method as_int = raise TypeError
  method as_float = (self :> float_key_data)
end

let empty = []
let add lst v = (v :> key_data)::lst
let find lst k = List.find (fun v -> (k :> key)#compare v = 0) lst

let lst = empty in
let lst = add lst (new int_key_data 1 23) in
let lst = add lst (new float_key_data 2 1.2) in
let o = find lst (new float_key 2)
in
  o#as_float#f



Wow, this is complex even as a trivial example. In my use case I even
have twice that many classes as for each class I have a variant that
constructs a new object and one that reads the object from disk. Also
I have a method to write each object to disk. But I left those out as
this is long enough already.

What I don't like about this is the shear size and the need for as_int
and as_float.


What I would like to do is this:

type key = Int of int | Float of int
type key_value = Int of int * int | Float of int * float
let as_key v = (v :> key)
let compare x y = Pervasives.compare (as_key x) (as_key y)

With that one could build an ('a, (#'a as 'b)) container.
Unfortunately the as_key needs Obj.magic and only works if the two
types are in sync and have no mutables or references and no type
specific closures.

One can use a functor with a 'module type = sig type k type v val
cmp : v -> v -> int val cmp_key : k -> v -> int : end' to get a magic
free solution.

The only other magic free solution I've come up with is using method 3
(closure records) from above. Again with an as_int and as_float
closure where one will always throw an exception.

Method 2 can't be used as that doesn't give a heterogeneous type.

MfG
        Goswin

Re: [Caml-list] Subtyping

[David MENTRE]

Hello,

On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> In the last 2 weeks I've been playing around with lots of different
> ways to do the same thing to get a feel for what style suites me
> best. If you have improvements or alternative ways of doing the two
> things below let me know.

Well, if you are learning OCaml, I would advise you to read regular
OCaml code, e.g. the standard library. You'll learn The Right OCaml
Style(tm).


> Lets look another thing going in a similar direction. I want to
> have a structure where I can store key value pairs. But just for fun
> lets say I want to store values of different types and the key knows
> the type of value. In short a heterogeneous associative container:

Well, why don't you just do:

# type k = Int_k of int | Float_k of int;;
type k = Int_k of int | Float_k of int
# type v = Int_v of int | Float_v of float;;
type v = Int_v of int | Float_v of float
# let h = Hashtbl.create 3;;
val h : ('_a, '_b) Hashtbl.t = <abstr>
# Hashtbl.add h (Int_k 3) (Int_v 4);;
- : unit = ()
# Hashtbl.add h (Float_k 5) (Float_v 0.6);;
- : unit = ()

Yours,
d.

Re: [Caml-list] Subtyping

[Peng Zang]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


On Tuesday 07 April 2009 03:41:32 am David MENTRE wrote:
> Hello,
>
> On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow <goswin-v-b@web.de> 
wrote:
> > In the last 2 weeks I've been playing around with lots of different
> > ways to do the same thing to get a feel for what style suites me
> > best. If you have improvements or alternative ways of doing the two
> > things below let me know.
>
> Well, if you are learning OCaml, I would advise you to read regular
> OCaml code, e.g. the standard library. You'll learn The Right OCaml
> Style(tm).

Certainly reading the standard library is good.  Useful for learning 
techniques, idioms, etc..  I wouldn't say that there is one Right OCaml 
Style(tm) though.  Actually part of why I like OCaml is that it supports 
imperative, object oriented and functional paradigms and you can switch 
between them depending on the task.

Cheers,

Peng
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.7 (GNU/Linux)

iD8DBQFJ21eifIRcEFL/JewRAptXAJwPec++ykZ6YjmLuUtdfrZw3IrXEwCbBkeB
juGHNPOqJds1rDZd8S1BQEQ=
=foQf
-----END PGP SIGNATURE-----

Re: [Caml-list] Subtyping

[Goswin von Brederlow]

Peng Zang <peng.zang@gmail.com> writes:

> On Tuesday 07 April 2009 03:41:32 am David MENTRE wrote:
>> Hello,
>>
>> On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow <goswin-v-b@web.de> 
> wrote:
>> > In the last 2 weeks I've been playing around with lots of different
>> > ways to do the same thing to get a feel for what style suites me
>> > best. If you have improvements or alternative ways of doing the two
>> > things below let me know.
>>
>> Well, if you are learning OCaml, I would advise you to read regular
>> OCaml code, e.g. the standard library. You'll learn The Right OCaml
>> Style(tm).
>
> Certainly reading the standard library is good.  Useful for learning 
> techniques, idioms, etc..  I wouldn't say that there is one Right OCaml 
> Style(tm) though.  Actually part of why I like OCaml is that it supports 
> imperative, object oriented and functional paradigms and you can switch 
> between them depending on the task.

Exactly. And so far I've been kind of stuck with one or the other so I
wanted to see how things look using different paradigms in ocaml.

> Cheers,
>
> Peng

MfG
        Goswin

Re: [Caml-list] Subtyping

[Goswin von Brederlow]

David MENTRE <dmentre@linux-france.org> writes:

> Hello,
>
> On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow <goswin-v-b@web.de> wrote:
>> In the last 2 weeks I've been playing around with lots of different
>> ways to do the same thing to get a feel for what style suites me
>> best. If you have improvements or alternative ways of doing the two
>> things below let me know.
>
> Well, if you are learning OCaml, I would advise you to read regular
> OCaml code, e.g. the standard library. You'll learn The Right OCaml
> Style(tm).

I've been using ocaml on and off for years now. Just trying out new
things.

>> Lets look another thing going in a similar direction. I want to
>> have a structure where I can store key value pairs. But just for fun
>> lets say I want to store values of different types and the key knows
>> the type of value. In short a heterogeneous associative container:
>
> Well, why don't you just do:
>
> # type k = Int_k of int | Float_k of int;;
> type k = Int_k of int | Float_k of int
> # type v = Int_v of int | Float_v of float;;
> type v = Int_v of int | Float_v of float
> # let h = Hashtbl.create 3;;
> val h : ('_a, '_b) Hashtbl.t = <abstr>
> # Hashtbl.add h (Int_k 3) (Int_v 4);;
> - : unit = ()
> # Hashtbl.add h (Float_k 5) (Float_v 0.6);;
> - : unit = ()

That would allow storing a float value under an int key or vice
versa. Something that would completly corrupt the on-disk format of my
data. One could add runtime checks that prevent this but I would
really like to have this ensured by the type system at compile time.

And I would like to avoid having to write a private insert functions
and public

let insert_int k v = insert (Int_k k) (Int_v v)
let insert_float k v = insert (Float_k k) (Float_v v)

For that the storing data structure would have to know that there are
int and float values and I would rather have the storing structure
polymorphic.

MfG
        Goswin

Re: [Caml-list] Subtyping

[Goswin von Brederlow]

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

> So what other ways are there of doing this? Records. Idealy I would
> like to do this:
>
> type base = { x : int }
> let make_base x = { x = x }
> let print_x r = print_int r.x
> type foo = { base with y : int }
> let make_foo x y = { x = x; y = y }
> let _ =
>   print_x (make_base 0); print_newline ();
>   print_x (make_foo 0 1); print_newline ();;
>
> Ocaml has no way of making this work like that, right?

Small extra question concerning this. Can I get ocaml to recognise a
type like this?

type base = 'a. {
  x : 'a;
  fn : 'a -> unit;
}

List.iter
  (fun r -> r.fn r)
  [{x = 1; fn = (fun r -> print_int r.x); };
   {x = 1.2; fn = (fun r -> print_float r.x); }]

The difference to a "'a base" type would be that the 'a is only
infered and fixed inside the record but remains abstract outside of
it.

For that reason this would not be allowed:

let cross_call x y = x.fn y

The 'a would have to escape the record which wouldn't be allowed.


So is there any syntax or trick to get the ocaml typesystem to
construct such a type?

MfG
        Goswin

Re: [Caml-list] Subtyping

[Jacques Garrigue]

From: Goswin von Brederlow <goswin-v-b@web.de>
> Small extra question concerning this. Can I get ocaml to recognise a
> type like this?
> 
> type base = 'a. {
>   x : 'a;
>   fn : 'a -> unit;
> }
> 
> List.iter
>   (fun r -> r.fn r)
>   [{x = 1; fn = (fun r -> print_int r.x); };
>    {x = 1.2; fn = (fun r -> print_float r.x); }]
> 
> The difference to a "'a base" type would be that the 'a is only
> infered and fixed inside the record but remains abstract outside of
> it.

First reaction: but your "base" type is just a closure. But this is
certainly not your question.

More disturbing: the rest of your code does not agree with base.
So I will assume you actually meant

List.iter
  (fun r -> r.fn r.x)
  [{x = 1; fn = print_int}; {x = 1.2; fn = print_float}]

Then what you are asking for is existential types. There is no syntax
for them in ocaml, but they can be encoded through universal types
(interestingly, the dual is not true).

type 'a base = {x : 'a; fn : 'a -> unit}
type 'b base_op = {bop: 'a. 'a base -> 'b}
type base_wrapper = {base: 'b. 'b base_op -> 'b}

let l =
  let a = {x = 1; fn = print_int}
  and b = {x = 1.2; fn = print_float} in
  [{base = fun x -> x.bop a}; {base = fun x -> x.bop b}]

List.iter (fun w -> w.base {bop = fun r -> r.fn r.x}) l

As you can see, the result is rather verbose, but this works.
Fortunately, closure and objects are usually enough...

Jacques Garrigue

Re: [Caml-list] Subtyping

[Jacques Garrigue]

Here is a slightly more usable version, using helper functions to
avoid writing intermediate closures by hand.

  type 'a base = {x : 'a; fn : 'a -> unit}
  (* 4 next lines are boilerplate, could be auto-generated *)
  type 'b base_op = {bop: 'a. 'a base -> 'b}
  type base_wrapper = {base: 'b. 'b base_op -> 'b}
  let wrap a = {base = fun x -> x.bop a}
  let apply op w = w.base op

  let l =
    [wrap {x = 1; fn = print_int}; wrap {x = 1.2; fn = print_float}];;

  List.iter (apply {bop = fun r -> r.fn r.x}) l

The only thing you cannot abbreviate is the {bop = ...} part, as this
is where universality is checked, to ensure that no cross application
can be done.

Jacques Garrigue

> Then what you are asking for is existential types. There is no syntax
> for them in ocaml, but they can be encoded through universal types
> (interestingly, the dual is not true).
> 
> type 'a base = {x : 'a; fn : 'a -> unit}
> type 'b base_op = {bop: 'a. 'a base -> 'b}
> type base_wrapper = {base: 'b. 'b base_op -> 'b}
> 
> let l =
>   let a = {x = 1; fn = print_int}
>   and b = {x = 1.2; fn = print_float} in
>   [{base = fun x -> x.bop a}; {base = fun x -> x.bop b}]
> 
> List.iter (fun w -> w.base {bop = fun r -> r.fn r.x}) l
> 
> As you can see, the result is rather verbose, but this works.
> Fortunately, closure and objects are usually enough...

Re: [Caml-list] Subtyping

[Goswin von Brederlow]

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

> type 'a base = {x : 'a; fn : 'a -> unit}
> type 'b base_op = {bop: 'a. 'a base -> 'b}
> type base_wrapper = {base: 'b. 'b base_op -> 'b}
>
> let l =
>   let a = {x = 1; fn = print_int}
>   and b = {x = 1.2; fn = print_float} in
>   [{base = fun x -> x.bop a}; {base = fun x -> x.bop b}]
>
> List.iter (fun w -> w.base {bop = fun r -> r.fn r.x}) l
>
> As you can see, the result is rather verbose, but this works.
> Fortunately, closure and objects are usually enough...
>
> Jacques Garrigue

That is exactly what I ment. I knew closures could have "'a. ..."
types but I didn't think of encoding the record and the method to
call both as closures.

MfG
        Goswin