[Caml-list] Type generalization problem

[Caml-list] Type generalization problem

[Ruslan Ledesma Garza]

Dear list,

Consider the following OCaml session.

        Objective Caml version 3.12.0

# let f : 'v . 'v -> 'v = fun x -> x;;
val f : 'a -> 'a = <fun>
# let g : 'v . 'v -> 'v = (fun x -> x) (fun x -> x);;
Error: This definition has type 'a -> 'a which is less general than
         'b. 'b -> 'b
# 

Why doesn't OCaml generalize the type 'a -> 'a? According to the typing rules in "Principal type-schemes for functional programs" ( http://portal.acm.org/citation.cfm?id=582176 ), the type 'a -> 'a can be generalized.

Something similar happens in the following OCaml session.

        Objective Caml version 3.12.0

# let f : 'v . 'v -> 'v = fun x -> x;;
val f : 'a -> 'a = <fun>
# let h = f f;;
val h : '_a -> '_a = <fun>
# h 1;;
- : int = 1
# h h;;
Error: This expression has type int -> int
       but an expression was expected of type int
# 

I want the type of h to be \forall 'a . 'a -> 'a.         :'(

Best regards,
Ruslán.

Re: [Caml-list] Type generalization problem

[Gabriel Scherer]

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

You have hit the "value restriction":
  http://caml.inria.fr/resources/doc/faq/core.en.html#eta-expansion

# let g = (fun x -> x) (fun x -> x);;
val g : '_a -> '_a = <fun>
# let g x = (fun x -> x) (fun x -> x) x;;
val g : 'a -> 'a = <fun>

Polymorphism annotation ( : 'a . 'a -> 'a ) have no use here, as you can
easily see in the return type if the value is polymorphic (type variables
'a, implicitly quantified at the beginning of the type) or not ("weak" type
variable '_a, which are just unknowns waiting to be unified).

On Sun, Aug 14, 2011 at 3:46 PM, Ruslan Ledesma Garza <
ruslanledesmagarza@gmail.com> wrote:

> Dear list,
>
> Consider the following OCaml session.
>
>        Objective Caml version 3.12.0
>
> # let f : 'v . 'v -> 'v = fun x -> x;;
> val f : 'a -> 'a = <fun>
> # let g : 'v . 'v -> 'v = (fun x -> x) (fun x -> x);;
> Error: This definition has type 'a -> 'a which is less general than
>         'b. 'b -> 'b
> #
>
> Why doesn't OCaml generalize the type 'a -> 'a? According to the typing
> rules in "Principal type-schemes for functional programs" (
> http://portal.acm.org/citation.cfm?id=582176 ), the type 'a -> 'a can be
> generalized.
>
> Something similar happens in the following OCaml session.
>
>        Objective Caml version 3.12.0
>
> # let f : 'v . 'v -> 'v = fun x -> x;;
> val f : 'a -> 'a = <fun>
> # let h = f f;;
> val h : '_a -> '_a = <fun>
> # h 1;;
> - : int = 1
> # h h;;
> Error: This expression has type int -> int
>       but an expression was expected of type int
> #
>
> I want the type of h to be \forall 'a . 'a -> 'a.         :'(
>
> Best regards,
> Ruslán.
>
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

Re: [Caml-list] Type generalization problem

[Ruslan Ledesma Garza]

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

I'm so happy now. :D 

Thanks a lot!
Ruslán.

On Aug 14, 2011, at 3:55 PM, Gabriel Scherer wrote:

> You have hit the "value restriction":
>   http://caml.inria.fr/resources/doc/faq/core.en.html#eta-expansion
> 
> # let g = (fun x -> x) (fun x -> x);;
> val g : '_a -> '_a = <fun>
> # let g x = (fun x -> x) (fun x -> x) x;;
> val g : 'a -> 'a = <fun>
> 
> Polymorphism annotation ( : 'a . 'a -> 'a ) have no use here, as you can easily see in the return type if the value is polymorphic (type variables 'a, implicitly quantified at the beginning of the type) or not ("weak" type variable '_a, which are just unknowns waiting to be unified).
> 
> On Sun, Aug 14, 2011 at 3:46 PM, Ruslan Ledesma Garza <ruslanledesmagarza@gmail.com> wrote:
> Dear list,
> 
> Consider the following OCaml session.
> 
>        Objective Caml version 3.12.0
> 
> # let f : 'v . 'v -> 'v = fun x -> x;;
> val f : 'a -> 'a = <fun>
> # let g : 'v . 'v -> 'v = (fun x -> x) (fun x -> x);;
> Error: This definition has type 'a -> 'a which is less general than
>         'b. 'b -> 'b
> #
> 
> Why doesn't OCaml generalize the type 'a -> 'a? According to the typing rules in "Principal type-schemes for functional programs" ( http://portal.acm.org/citation.cfm?id=582176 ), the type 'a -> 'a can be generalized.
> 
> Something similar happens in the following OCaml session.
> 
>        Objective Caml version 3.12.0
> 
> # let f : 'v . 'v -> 'v = fun x -> x;;
> val f : 'a -> 'a = <fun>
> # let h = f f;;
> val h : '_a -> '_a = <fun>
> # h 1;;
> - : int = 1
> # h h;;
> Error: This expression has type int -> int
>       but an expression was expected of type int
> #
> 
> I want the type of h to be \forall 'a . 'a -> 'a.         :'(
> 
> Best regards,
> Ruslán.
> 
> 
> 
> 
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> 
> 


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