"ocaml_beginners"::[] Syntax for polymorphic methods

The Ocaml manual introduces polymorphic methods using a syntax of the
form " 'a. <stuff involving 'a>&quot;. What is the meaning of the " 'a. "
syntax (with a dot after the type variable)? I can find only one prior
reference to this syntax, in a passage on storing polymorphic
functions in records, but neither mention of this syntax explains it,
and Chapter 6 (the formal language spec) is, as far as I can tell,
equally silent.

Messages in this topic (1) Reply (via web post) | Start a new topic

.

On 2/26/07, Geoffrey Romer < geoff.romer%40gmail.com">geoff.romergmail.com> wrote:
&gt;
> The Ocaml manual introduces polymorphic methods using a syntax of the
> form " 'a. <stuff involving 'a>&quot;. What is the meaning of the " 'a. "
&gt; syntax (with a dot after the type variable)? I can find only one prior
&gt; reference to this syntax, in a passage on storing polymorphic
> functions in records, but neither mention of this syntax explains it,
> and Chapter 6 (the formal language spec) is, as far as I can tell,
&gt; equally silent.

This means "for all 'a . <stuff involving 'a>&quot; (universal
quantification) and is a form of second-order polymorphism. It allows
you to have polymorphic recursion.
Here is an example:

type 'a typed_val =
| TVal of 'a | TInt of int typed_val | TBool of bool typed_val
| TIntFun of (int -> 'a) typed_val
| TBoolFun of (bool -> 'a) typed_val
;;
type boxed_val =
| BInt of int | BBool of bool | BFun of (boxed_val -> boxed_val)
;;
type boxing_function =
{mutable b_f :
'a. (('a -> boxed_val) -> 'a typed_val -> boxed_val) option}
;;
let b_f = {b_f = None}
;;
let box acc tv = match b_f.b_f with
| None -> failwith "not implemented yet"
| Some f -> f acc tv
;;
let box acc = function
| TVal v -> acc v
| TInt ti -> box (fun i -> BInt i) ti
| TBool tb -> box (fun b -> BBool b) tb
| TIntFun tf ->
box
(fun f -> BFun (function (BInt i) -> acc (f i))) tf
| TBoolFun tf ->
box
(fun f -> BFun (function (BBool b) -> acc (f b))) tf
;;
b_f.b_f <- Some box;;

let test = TInt (TIntFun (TIntFun (TBoolFun (TVal (
fun b i1 i2 -> if b then i1 else i2)))));;
let boxed = box (fun () -> failwith "unreachable&quot;) test;;

type expr = EAp of expr * expr | EVal of boxed_val;;

let rec eval = function
| EVal v -> v
| EAp (e_f, e_a) ->
match eval e_f with
| BFun f -> f (eval e_a)
| _ -> failwith "eval: function expected&quot;
;;

eval
(EAp (EAp (EAp ((EVal boxed), EVal (BBool true)), EVal (BInt 7)),
EVal (BInt 13)));;

Messages in this topic (2) Reply (via web post) | Start a new topic

.

So what's the difference between 'a. <stuff&gt; and just plain <stuff&gt;? Aren't
type variables implicitly universally quantified (i.e. isn't the whole point
of a polymorphic type that it applies for any possible 'a)?

On 2/26/07, Lukasz Stafiniak < lukstafi%40gmail.com">lukstafigmail.com> wrote:
&gt;
> On 2/26/07, Geoffrey Romer < geoff.romer%40gmail.com">geoff.romergmail.com<geoff.romer%40gmail.com>>
>; wrote:
&gt; >
>; > The Ocaml manual introduces polymorphic methods using a syntax of the
> > form " 'a. <stuff involving 'a>&quot;. What is the meaning of the " 'a. "
&gt; > syntax (with a dot after the type variable)? I can find only one prior
&gt; > reference to this syntax, in a passage on storing polymorphic
> > functions in records, but neither mention of this syntax explains it,
> > and Chapter 6 (the formal language spec) is, as far as I can tell,
&gt; > equally silent.
>
> This means "for all 'a . <stuff involving 'a>&quot; (universal
> quantification) and is a form of second-order polymorphism. It allows
&gt; you to have polymorphic recursion.
> Here is an example:
>
>; type 'a typed_val =
> | TVal of 'a | TInt of int typed_val | TBool of bool typed_val
> | TIntFun of (int -> 'a) typed_val
> | TBoolFun of (bool -> 'a) typed_val
> ;;
> type boxed_val =
> | BInt of int | BBool of bool | BFun of (boxed_val -> boxed_val)
> ;;
> type boxing_function =
> {mutable b_f :
> 'a. (('a -> boxed_val) -> 'a typed_val -> boxed_val) option}
> ;;
> let b_f = {b_f = None}
&gt; ;;
> let box acc tv = match b_f.b_f with
>; | None -> failwith "not implemented yet"
> | Some f -> f acc tv
> ;;
> let box acc = function
> | TVal v -> acc v
> | TInt ti -> box (fun i -> BInt i) ti
> | TBool tb -> box (fun b -> BBool b) tb
> | TIntFun tf ->
&gt; box
> (fun f -> BFun (function (BInt i) -> acc (f i))) tf
> | TBoolFun tf ->
&gt; box
> (fun f -> BFun (function (BBool b) -> acc (f b))) tf
> ;;
> b_f.b_f <- Some box;;
&gt;
> let test = TInt (TIntFun (TIntFun (TBoolFun (TVal (
> fun b i1 i2 -> if b then i1 else i2)))));;
> let boxed = box (fun () -> failwith "unreachable&quot;) test;;
&gt;
> type expr = EAp of expr * expr | EVal of boxed_val;;
>
> let rec eval = function
> | EVal v -> v
> | EAp (e_f, e_a) ->
&gt; match eval e_f with
>; | BFun f -> f (eval e_a)
>; | _ -> failwith "eval: function expected&quot;
> ;;
>
> eval
>; (EAp (EAp (EAp ((EVal boxed), EVal (BBool true)), EVal (BInt 7)),
>; EVal (BInt 13)));;
>
>

[Non-text portions of this message have been removed]

Messages in this topic (3) Reply (via web post) | Start a new topic

.

On 2/26/07, Geoffrey Romer < geoff.romer%40gmail.com">geoff.romergmail.com> wrote:
&gt;
> So what's the difference between 'a. <stuff&gt; and just plain <stuff&gt;? Aren't
&gt; type variables implicitly universally quantified (i.e. isn't the whole point
&gt; of a polymorphic type that it applies for any possible 'a)?
>;
You've got me here...

Objective Caml version 3.09.3

# type pty = {pv : 'a . 'a list};;
type pty = { pv : 'a. 'a list; }
# let px = {pv = []};;
val px : pty = {pv = []}
# match px with
{pv=[]} -> "OK&quot;
| {pv=5::_} -> "int&quot;
| {pv=true::_} -> "bool";;
Fatal error: exception Assert_failure(";typing/parmatch.ml&quot;, 784, 55)

Process caml-toplevel exited abnormally with code 2

Messages in this topic (4) Reply (via web post) | Start a new topic

.

On 2/26/07, Geoffrey Romer < geoff.romer%40gmail.com">geoff.romergmail.com> wrote:
&gt;
> So what's the difference between 'a. <stuff&gt; and just plain <stuff&gt;? Aren't
&gt; type variables implicitly universally quantified (i.e. isn't the whole point
&gt; of a polymorphic type that it applies for any possible 'a)?
>;
When <stuff&gt; is a type of a variable (by variable I mean a parameter
of a function), then type variables in it are existentially quantified
(in the sense that they are "solved for"). When you define a recursive
function, the recursive function's self type behaves like a type of a
variable in this respect.

Here comes an experiment:

# type 'a mty = {mv : 'a list};;
type 'a mty = { mv : 'a list; }
# type pty = {pv : 'a . 'a list};;
type pty = { pv : 'a. 'a list; }
# let f x = ignore (5:.mv); ignore (true:.mv);;
Characters 42-46:
let f x = ignore (5:.mv); ignore (true:.mv);;
^^^^
This expression has type int list but is here used with type bool list
# let pf x = ignore (5:.pv); ignore (true:.pv);;
val pf : pty -> unit = <fun>;

Messages in this topic (5) Reply (via web post) | Start a new topic

.

On 2/26/07, Lukasz Stafiniak < lukstafi%40gmail.com">lukstafigmail.com> wrote:
&gt; When <stuff&gt; is a type of a variable (by variable I mean a parameter
> of a function), then type variables in it are existentially quantified

(or a mutable value)

Messages in this topic (6) Reply (via web post) | Start a new topic

.

On Sun, Feb 25, 2007 at 05:11:23PM -0800, Geoffrey Romer wrote:
&gt; The Ocaml manual introduces polymorphic methods using a syntax of the
> form " 'a. <stuff involving 'a>&quot;. What is the meaning of the " 'a. "
&gt; syntax (with a dot after the type variable)? I can find only one prior
&gt; reference to this syntax, in a passage on storing polymorphic
> functions in records, but neither mention of this syntax explains it,
> and Chapter 6 (the formal language spec) is, as far as I can tell,
&gt; equally silent.

There's only one place where ordinary programmers are going to be
using 'a . ... methods, and that is when defining a polymorphic map
method.

Consider this example from ocamldbi:

class statement ->
object
(*...*)
method map : 'a . (sql_t list -> 'a) -> 'a list
end

If you don't use the 'a . universal qualification then the 'a
";escapes&quot; out to the level of the whole object, so you would end up
having a definition like:

class ['a] statement ->
object
(*...*)
method map : (sql_t list -> 'a) -> 'a list
end

which doesn't work (it results in a map method which can only work on
one type, in other words it's wouldn't be polymorphic).

Rich.

--
Richard Jones
Red Hat UK Limited

Messages in this topic (7) Reply (via web post) | Start a new topic

.

On 2/26/07, Richard Jones < rich%40annexia.org">richannexia.org> wrote:
&gt;
> There's only one place where ordinary programmers are going to be
> using 'a . ... methods, and that is when defining a polymorphic map
> method.
>
> Consider this example from ocamldbi:
>
&gt; class statement ->
&gt; object
&gt; (*...*)
> method map : 'a . (sql_t list -> 'a) -> 'a list
>; end
>
> If you don't use the 'a . universal qualification then the 'a
> "escapes" out to the level of the whole object, so you would end up
> having a definition like:
&gt;
> class ['a] statement ->
&gt; object
&gt; (*...*)
> method map : (sql_t list -> 'a) -> 'a list
>; end
>
> which doesn't work (it results in a map method which can only work on
> one type, in other words it's wouldn't be polymorphic).
>
But this doesn't answer why it is happening, why are the types
restricted to monomorphic, what are the counter-examples in:

class ['a] lmap =
object
method map (l : 'a list) = List.map (fun x -> x) l
end;;
let ob = new lmap;;

and:

let f = List.map (fun x -> x);;

Messages in this topic (8) Reply (via web post) | Start a new topic

.