Re: [Caml-list] explicit polymorphic types in record fields

[Gerd Stolpmann <info@gerd-stolpmann.de>]

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

Am Montag, den 16.02.2015, 00:06 +0000 schrieb Jean Saint-Remy:
> Hi,
> 
> 
> I was reading the ocaml manual section 1.5 where an explicit
> polymorphic type can be declared.  I wanted to know if the trailing
> dot '.' is a special case "marker" only and does not have anything to
> do with how we distinguish floating point multiplication, division,
> subtraction, and addition, and nothing to do with accessing the
> elements of an array.

Yes, it is part of a special notation.

>  Without the trailing dot we cannot declare any such polymorphic
> fields no how, no way. I was also surprised to find this was possible.
> 
> 
> 
> [The manual says] In some special cases, you may need to store a
> polymorphic function in a data structure, keeping its polymorphism.
> Without user-provided type annotations, this is not allowed, as
> polymorphism is only introduced on a global level. 

It's not the global level, but the scope of the definition, e.g. compare
your idref with:

type 'a idref2 = { mutable id2 : 'a -> 'a }

Here, you need to instantiate 'a per use of idref2 (e.g. int idref2),
i.e. 'a is bound somewhere in the environment. This also allows
polymorphism if the environment generalizes 'a (e.g. when 'a is made
polymorphic in a let binding). The difference becomes more visible when
you embed idref/idref2 in other data structures, say a list:

type idreflist = idref list
type 'a idref2list = 'a idref2 list

As you see, the second form only permits lists where 'a is the same for
all elements, whereas in the first form 'a is polymorphic per element.

So:

# let identity x = x;;
val identity : 'a -> 'a = <fun>
# let identity2 x = prerr_endline "hi"; x;;   
val identity2 : 'a -> 'a = <fun>
# let l1 = [ { id = identity }; { id = identity2 } ];;
val l1 : idref list = [{id = <fun>}; {id = <fun>}]
# let l2 = [ { id2 = identity }; { id2 = identity2 } ];;
val l : '_a idref2 list = [{id2 = <fun>}; {id2 = <fun>}]
# (List.hd l1).id "string";;
- : string = "string"
# (List.hd l1).id 12;;      
- : int = 12
# (List.hd l2).id2 "string";;
- : string = "string"
# (List.hd l2).id2 34;;     
Error: This expression has type int but an expression was expected of
type string
# (List.nth l2 1).id2 34;;  
Error: This expression has type int but an expression was expected of
type string

Beware of this:

# [{id = String.copy }];;
Error: This field value has type string -> string which is less general
than 'a. 'a -> 'a
# [{id2 = String.copy }];;
- : string idref2 list = [{id2 = <fun>}]

This is why the per-element polymorphism is normally not the right
choice: it is not only possible but even required that the function is
polymorphic.

> However, you can give explicitly polymorphic types to record fields.
> # type idref = { mutable id: 'a. 'a -> 'a };;
> type idref = { mutable id : 'a. 'a -> 'a; }
> 
> # let r = {id = fun x -> x};;
> val r : idref = {id = <fun>}
> 
> # let g s = (s.id 1, s.id true);;
> val g : idref -> int * bool = <fun>
> 
> # r.id <- (fun x -> print_string "called id\n"; x);;
> - : unit = ()
> 
> # g r;;
> called id
> called id
> - : int * bool = (1, true)
> I am having difficulty reading the first line, the type declaration
> "type idref = { mutable id : 'a. 'a -> 'a } ;;"  When I look at the
> way we are accessing the field values on line 3, it does look like
> accessing member fields in other languages and it does superficially
> resemble array indexing as in "let str = "abcdef" ;; str.[1] ;; -:
> char = 'b'".  The two ways we are using the dot '.' are very distinct.
> Is that correct?

Yes. The dot in s.id is the normal record member access. It has nothing
to do with the dot in the polymorphic type expression.

>  The second is the common place indexing, whereas the first is just a
> "marker".  I could not declare the fields for example as a polymorphic
> tuple for instance: "type idref = { mutable 'a * 'b -> 'a }" nor "type
> idref = { mutable 'a. 'b -> 'a }".

type idref = { mutable 'a 'b . 'b -> 'a }

>  The latter is just nonsense, the 'b is undefined. But we could have a
> two field record by just repeating the type definitions. "let idref =
> { mutable 'a. 'a -> 'a; mutable 'b. 'b -> 'b }". The polymorphic type
> does not have any restriction, it appears we could have any
> fundamental type we wanted. The type 'a variable must be repeated, it
> is not enough to say "type idref = { mutable 'a. -> 'a };;" Is it
> correct then to read the declaration in this way: the type 'a
> polymorphic type as a polymorphic variable of type 'a. I know it
> sounds redundant, but that is how I am reading the syntax.

Yes. This notation actually picks up the notation for logical
quantification in mathematics (e.g. ∀ x ∊ S . p(x) ). On the left side
of the dot the variables are introduced which are used on the right
side.

Gerd



> 
> 
> Thank you for clarifying this for me.
> 
> 
> jean
> 

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]