Re: [Caml-list] Row-polymorphic type declarations

[Leo White <lpw25@cam.ac.uk>]

> 1. Does anyone know how can we later instantiate the polymorphic row variables ".." with particular rows (both for obj
> methods and variants). Any good docs on this? How do we assert that another type/expression is equivalent to 'a t with
> 'a being a particular set of rows.
>
> Could someone give an example with a 2D point type
>
> type 'a twoDimensionalPoint constraint 'a = <x:int; y:int; ..>;;
>
> How would we create another type threeDimensionalPoint that we assert is a two dimensional point with the polymorphic
> row variables being set to `z:int`? I understand type inference/checking automates most of this, but I often like to
> explicitly write type definitions to verify my own understanding of the program/inference.

You can never get your hands on the row variable itself, you can only
ever refer to polymorphic types containing row variables. For example,
in your definition of `twoDimensionalPoint` you capture the row variable
`..` by instead refering the the polymorphic type `<x: int; y: int; ..>`.

Similarly, you cannot instantiate the row variable directly, but instead
you must instantiate a polymorphic type containing the row variable.

For your example, I can think of a few ways to specify this.

1. Using a constraint on a `twoDimensionalPoint`:

       type 'a threeDimensionalPoint = 'a twoDimensionalPoint
         constraint 'a = <z: int; ..>

2. Using two constraints on the type parameter:

       type 'a threeDimensionalPoint = 'a
         constraint 'a = 'a twoDimensionalPoint
         constraint 'a = <z: int; ..>;;

3. Since your example uses object types, class types provide an alternative
   mechanism:

       class type twoDimensionalPoint = object
         method x: int
         method y: int
       end

       class type threeDimensionalPoint = object
         inherit twoDimensionalPoint
         method z: int
       end

   which allows you to use the `#t` syntax to refer to the polymorphic
   object types:

     let foo (p : #twoDimensionalPoint) = p#x + p#y

     let bar (p : #threeDimensionalPoint) = p#z + foo p

   A similar thing can also be achieved for polymorphic variants:

     type t = [`X of int]

     type s = [t | `Y of int]

     let foo (v : [> t]) =
       match v with
       | `X i -> i
       | _ -> 0

     let bar (v : [> s]) =
       match v with
       | `Y i -> i
       | x -> foo x

> 3. Also curious why annotations in arguments don't require acknowledgment of row polymorphism
>
>   let f (o:<x:int; y:int; ..>) = o#x + o#y;;

The row polymorphism is acknowledged by the `..` which represents the
row variable.

> 4. It appears there are two ways to write the row-polymorphic type annotation:
> type 'a t = ([> `Red ] as 'a) and type 'a t constraint 'a = [> `Red ]. Why are there two ways and what are the
> advantages?

They are completely equivalent.

Regards,

Leo