Re: [Caml-list] let rec and polymorphic functions

Re: [Caml-list] let rec and polymorphic functions

[David Allsopp]

> There are many problems with this. Google for ad-hoc polymorphism,
> polymorphic recursion and generic printing.
>
> On Wednesday 27 June 2007 09:40:31 David Allsopp wrote:
> >   out "TEST";
>
> val out : string -> unit
>
> >   out "%d" 0;
>
> val out : format -> int -> unit

The type-checker doesn't see that surely? Surely on that expression it sees
out : string -> int -> unit?? Note that changing the sequence to

out "%b" true;
out "%d" 0;

and removing the out "TEST" still causes problems - although O'Caml manages
to infer the [format4] first argument for [out], it fixes the first
parameter of the [format4] as being [bool -> unit] and so prevents [out]
from being used with anything other than a single "%b" argument and hence
gives a type error on the next application.

> As printf is ad-hoc polymorphic, you must supply the format specifier 
> immediately and OCaml will generate a custom printer for you. OCaml does
> not use run-time types so you cannot have a generic print function: you
> must specific print functions for each of your (possibly higher-order)
> types.

Yes, except that what's odd to me is that the type-checker doesn't behave as
the manual says it ought to with [let rec]. BUT... 

> Also, recursive calls ossify the function to a monomorphic type, so you 
> cannot do polymorphic recursion in OCaml. There are workaround using 
> recursive modules or objects but I don't think this is what you want here.

That does explain it - which I didn't know. Consider this which is also
broken (and simpler because it has nothing to do with the ad-hoc
polymorphism of printf)

let rec id x = x
and _ = id 0
in
  id (); (* *** *)
  id 1;;

Gives a type error for *** because id is already inferred as int -> int
because of the monomorphic nature of the recursive definition. This is
over-guarded but I never got an answer on a previous post as to why. The
equivalent SML does type polymorphically:

let fun id x = x
val _ = id 0
in
  id ();
  id 1
end;

Incidentally, it's lucky that this is polymorphic in SML because all
function definitions are recursive IIRC.

But no-one posted an explanation as to why there's this difference in the
let construct between the two flavours of ML :(


David

Re: [Caml-list] let rec and polymorphic functions

[Jeremy Yallop]

David Allsopp wrote:
> That does explain it - which I didn't know. Consider this which is also
> broken (and simpler because it has nothing to do with the ad-hoc
> polymorphism of printf)
> 
> let rec id x = x
> and _ = id 0
> in
>   id (); (* *** *)
>   id 1;;
> 
> Gives a type error for *** because id is already inferred as int -> int
> because of the monomorphic nature of the recursive definition. 

Right.  In particular, it gives a type error because `id' is used at the 
type int -> int within its own definition (the rhs of every binding in 
the group), so that's the type that it's given for the rest of the 
program (the part following "in").

> This is
> over-guarded but I never got an answer on a previous post as to why. The
> equivalent SML does type polymorphically:
> 
> let fun id x = x
> val _ = id 0
> in
>   id ();
>   id 1
> end;

This isn't really "the equivalent SML", since the definition of `id x' 
and the application `id 0' aren't in the same recursive group.  The 
equivalent in SML would be something like

    let val rec id = fn x => x
            and _  = id 0
        in
           id ();
           id 1
    end

although this actual program isn't valid; SML only allows syntactic 
function expressions on the rhs of `let rec'.  If you throw in a "fn" to 
avoid the restriction you'll find that SML behaves essentially the same 
as OCaml:

     let val rec id = fn x => x
             and x = fn _ => id 0
         in
           id ();
           id 1
     end



OCaml seems a little inconsistent here, actually.  The application `id 
0' is only valid as the rhs of let rec because the compiler can 
determine that there's no actual recursion involved.  There doesn't seem 
to be a reason not to apply a similar analysis to type checking, 
allowing more polymorphism for functions in the same recursive group 
that aren't actually part of a cycle.

Jeremy.

RE: [Caml-list] let rec and polymorphic functions

[David Allsopp]

> This isn't really "the equivalent SML", since the definition of `id x' 
> and the application `id 0' aren't in the same recursive group.  The 
> equivalent in SML would be something like

Thanks for this. I see the SML difference now - 

let fun id x = x
    and g x = id 0 + x
in
  id ()
end;

similarly doesn't work in SML with a pair of functions instead.

> OCaml seems a little inconsistent here, actually.  The application `id 
> 0' is only valid as the rhs of let rec because the compiler can 
> determine that there's no actual recursion involved.  There doesn't 
> seem to be a reason not to apply a similar analysis to type checking, 
> allowing more polymorphism for functions in the same recursive group 
> that aren't actually part of a cycle.

Which is what SML did in my "equivalent" example - and it would certainly be
nice if OCaml did the same. Is it worth raising a bug (well, feature
request) for or am I the only person who (ab)uses [let rec] in this way?

Many thanks,


David

Re: [Caml-list] let rec and polymorphic functions

[Virgile Prevosto]

Le mer 27 jun 2007 12:12:34 CEST,
Jeremy Yallop <jeremy.yallop@ed.ac.uk> a écrit :

> David Allsopp wrote:
> > let rec id x = x
> > and _ = id 0
> > in
> >   id (); (* *** *)
> >   id 1;;
> > 
> This isn't really "the equivalent SML", since the definition of `id
> x' and the application `id 0' aren't in the same recursive group.
> The equivalent in SML would be something like
> 
>     let val rec id = fn x => x
>             and _  = id 0
>         in
>            id ();
>            id 1
>     end
> 
> 
> OCaml seems a little inconsistent here, actually.  The application
> `id 0' is only valid as the rhs of let rec because the compiler can 

Well, it just seems that Ocaml performs type inference before checking
the validity of the recursive definition. If you give a well-typed
term, it will complain about a forbidden rhs of let rec:

        Objective Caml version 3.10.0

#  let rec id = fun x -> x and _foo = id 0 in id 1;;
This kind of expression is not allowed as right-hand side of `let rec'
-- 
E tutto per oggi, a la prossima volta.
Virgile

Re: [Caml-list] let rec and polymorphic functions

[Jeremy Yallop]

Virgile Prevosto wrote:
> Le mer 27 jun 2007 12:12:34 CEST,
> Jeremy Yallop <jeremy.yallop@ed.ac.uk> a écrit :
>> OCaml seems a little inconsistent here, actually.  The application
>> `id 0' is only valid as the rhs of let rec because the compiler can 
> 
> Well, it just seems that Ocaml performs type inference before checking
> the validity of the recursive definition. If you give a well-typed
> term, it will complain about a forbidden rhs of let rec:

You're right; I'd overestimated the extent of the analysis.  Note that 
applications on the rhs of let rec are acceptable if there's no 
recursion at all involved in the application:

   let id x = x in
   let rec f = id id
       and g x = g (f x)
    in g

Jeremy.

> 
>         Objective Caml version 3.10.0
> 
> #  let rec id = fun x -> x and _foo = id 0 in id 1;;
> This kind of expression is not allowed as right-hand side of `let rec'

Re: [Caml-list] let rec and polymorphic functions

[Jon Harrop]

On Wednesday 27 June 2007 11:24:53 David Allsopp wrote:
> The type-checker doesn't see that surely? Surely on that expression it sees
> out : string -> int -> unit?? Note that changing the sequence to
>
> out "%b" true;
> out "%d" 0;
>
> and removing the out "TEST" still causes problems - although O'Caml manages
> to infer the [format4] first argument for [out], it fixes the first
> parameter of the [format4] as being [bool -> unit] and so prevents [out]
> from being used with anything other than a single "%b" argument and hence
> gives a type error on the next application.

Yes. This is the polymorphic recursion part of your problem. You cannot 
call "f" polymorphically from inside the "let" binding.

Look at this:

# let rec f x = Printf.printf x and g() = f "%d" 3;;
val f : (int -> unit, out_channel, unit) format -> int -> unit = <fun>
val g : unit -> unit = <fun>

Note how "f" has been made specific to the type "int" because of its call 
inside "g".

If you separate the calls (which you can do in this special case) you recover 
the polymorphic "f":

# let rec f x = Printf.printf x;;
val f : ('a, out_channel, unit) format -> 'a = <fun>
# let g() = f "%d" 3;;
val g : unit -> unit = <fun>

The critical difference is whether or not the call to "f" appears inside its 
definition, and that includes inside the body of "g" when "g" is defined at 
the same time as "f" using "let rec". If you want more details, read papers 
about the implementation of non-generalized type variables in the 
Hindley-Milner type system.

I'll try to ossify this by example. You can do:

# let f _ = () in f 0; f "foo";;
- : unit = ()

but not:

# let rec f _ = () and g = f 0; f "foo";;
This expression has type string but is here used with type int

> > Also, recursive calls ossify the function to a monomorphic type, so you
> > cannot do polymorphic recursion in OCaml. There are workaround using
> > recursive modules or objects but I don't think this is what you want
> > here.
>
> That does explain it - which I didn't know. Consider this which is also
> broken (and simpler because it has nothing to do with the ad-hoc
> polymorphism of printf)
>
> let rec id x = x
> and _ = id 0
> in
>   id (); (* *** *)
>   id 1;;

Exactly, yes.

> Gives a type error for *** because id is already inferred as int -> int
> because of the monomorphic nature of the recursive definition. This is
> over-guarded but I never got an answer on a previous post as to why. The
> equivalent SML does type polymorphically:
>
> let fun id x = x
> val _ = id 0
> in
>   id ();
>   id 1
> end;

No, that is equivalent to the OCaml that does work:

# let f _ = () in f 0; f "foo";;
- : unit = ()

> Incidentally, it's lucky that this is polymorphic in SML because all
> function definitions are recursive IIRC.
>
> But no-one posted an explanation as to why there's this difference in the
> let construct between the two flavours of ML :(

SML does not support polymorphic recursion either:

$ sml
Standard ML of New Jersey v110.62 [built: Thu Feb 22 13:17:37 2007]
- fun f x = f 1; f 1.0; ()
val f = fn : int -> 'a
stdIn:1.16-1.21 Error: operator and operand don't agree [tycon mismatch]
  operator domain: int
  operand:         real
  in expression:
    f 1.0

The reason is basically that both OCaml and Standard ML were designed around 
the Hindley-Milner type system, which made the deliberate design decision to 
push the limits of a decideable type system as far as possible. So they were 
designed to infer as much as possible whilst ensuring that type annotations 
are never required. Polymorphic recursion oversteps this boundary.

The designers of Haskell decided to ditch decideability in favour of (much) 
more power in the type system. So Haskell sometimes requires you to write 
explicit type annotations. Indeed, Haskell programmers almost always write 
type annotations, which is one of the reasons why idiomatic Haskell is 
comparatively verbose.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
The OCaml Journal
http://www.ffconsultancy.com/products/ocaml_journal/?e

Re: [Caml-list] let rec and polymorphic functions

[Arnaud Spiwack]

Jon Harrop a écrit :
> There are many problems with this. Google for ad-hoc polymorphism, polymorphic 
> recursion and generic printing.
>
> On Wednesday 27 June 2007 09:40:31 David Allsopp wrote:
>   
>>   out "TEST";
>>     
>
> val out : string -> unit
>   
Actually it seems to infer properly "out : (unit, out_channel, unit) 
format -> unit". So the magic is pulled here (which surprises me a lot, 
but well). The problem seems more related to the fact that mutual 
recursive function are monomorphic.
>   
>>   out "%d" 0;
>>     
>
> val out : format -> int -> unit
>
> As printf is ad-hoc polymorphic, you must supply the format specifier 
> immediately and OCaml will generate a custom printer for you. OCaml does not 
> use run-time types so you cannot have a generic print function: you must 
> specific print functions for each of your (possibly higher-order) types.
>
> Also, recursive calls ossify the function to a monomorphic type, so you cannot 
> do polymorphic recursion in OCaml. There are workaround using recursive 
> modules or objects but I don't think this is what you want here.
>
>   

Re: [Caml-list] let rec and polymorphic functions

[Jon Harrop]

There are many problems with this. Google for ad-hoc polymorphism, polymorphic 
recursion and generic printing.

On Wednesday 27 June 2007 09:40:31 David Allsopp wrote:
>   out "TEST";

val out : string -> unit

>   out "%d" 0;

val out : format -> int -> unit

As printf is ad-hoc polymorphic, you must supply the format specifier 
immediately and OCaml will generate a custom printer for you. OCaml does not 
use run-time types so you cannot have a generic print function: you must 
specific print functions for each of your (possibly higher-order) types.

Also, recursive calls ossify the function to a monomorphic type, so you cannot 
do polymorphic recursion in OCaml. There are workaround using recursive 
modules or objects but I don't think this is what you want here.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
The OCaml Journal
http://www.ffconsultancy.com/products/ocaml_journal/?e