[Caml-list] Row-polymorphic type declarations

[Caml-list] Row-polymorphic type declarations

[Jordan W]

[-- Attachment #1: Type: text/plain, Size: 1507 bytes --]

I'd like to hear the answers to some questions asked on Twitter, that Anil
began replying to:

The original question was: Does anyone know why OCaml doesn't allow
defining types with polymorphic row variables: <red: int; ..> or [> `Red ]
but will infer them?

Anil's answer was to use:

    type 'a t constraint 'a = [> `Red ]
    type 'a t constraint 'a = <x:int; ..>

Here are the follow up questions that could still use some clarification:

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.

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

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?

[-- Attachment #2: Type: text/html, Size: 1762 bytes --]

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

[Goswin von Brederlow]

On Mon, Jun 09, 2014 at 11:50:22AM -0700, Jordan W wrote:
> I'd like to hear the answers to some questions asked on Twitter, that Anil
> began replying to:
> 
> The original question was: Does anyone know why OCaml doesn't allow
> defining types with polymorphic row variables: <red: int; ..> or [> `Red ]
> but will infer them?
> 
> Anil's answer was to use:
> 
>     type 'a t constraint 'a = [> `Red ]
>     type 'a t constraint 'a = <x:int; ..>
> 
> Here are the follow up questions that could still use some clarification:
> 
> 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.

I think you can't assert that in the definition of the
threeDimensionalPoint type. But you can add a dummy function that
takes a threeDimensionalPoint and returns it as a twoDimensionalPoint.
If the types can't be unified then the function will give an error.
 
> 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;;

Not sure what you ask there. You are annotating a type. period.
 
> 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?

I'm not sure if both are identical and in what cases you can only use
the one form or the other. But I think only the constraint syntax can
be used when declaring the type of functions.

MfG
	Goswin

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

[Leo White]

> 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

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

[Jacques Garrigue]

Others answered your questions, but they have missed what I think is probably just a typo:

On 2014/06/10 03:50, Jordan W wrote:

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


type 'a t = ([> `Red ] as 'a) and type 'a t = 'a constraint 'a = [> `Red ] are equivalent,
where the parameter is just a trick to allow a row variable inside a definition,
but type 'a t constraint 'a = [> `Red ] is an abstract type, whose parameter is constrained,
so it is different from any other type.

	Jacques