weird type behavior

weird type behavior

[Kirill]

Hi everyone,

I'm a novice user of OCaml and functional languages in general. While
playing with the interpreter, writing all kinds of functions, I've run
into a behavior that doesn't look quite right to me. Please excuse me,
if it is explained somewhere and I simply haven't gotten there yet.

In the following example, I define a simple function foo that returns
function bar, which, in turn, accepts 2 parameters. The weird part is
that after bar is being called for the first time, its signature changes
from polymorphic types to ints. Right after (foo 3) call it's
  '_a -> '_b -> '_b = <fun>
But after being called, it becomes
  (int -> int) -> int -> int = <fun>


# let foo n =
    let bar f x = x in bar;;
val foo : 'a -> 'b -> 'c -> 'c = <fun>

# let inc x = x + 1;;
val inc : int -> int = <fun>

# let z = foo 3;;
val z : '_a -> '_b -> '_b = <fun>

# z inc 0;;
- : int = 0
# z;;
- : (int -> int) -> int -> int = <fun>


I have also noticed that if foo doesn't accept parameters, everything
works as expected:

# let foo =
    let bar f x = x in bar;;
val foo : 'a -> 'b -> 'b = <fun>
# let inc x = x + 1;;
val inc : int -> int = <fun>
# let z = foo;;
val z : 'a -> 'b -> 'b = <fun>
# z inc 0;;
- : int = 0
# z;;
- : 'a -> 'b -> 'b = <fun>

I have tried this with 3.09.2 and 3.09.3 on X64 Ubuntu.

I have also noticed other things I don't see explanation for, but they
may be connected to this one. Will be grateful for any explanation. 

Thanks,
-Kirill

Re: [Caml-list] weird type behavior

[Richard Jones]

On Sat, Oct 28, 2006 at 05:49:08PM +0200, Kirill wrote:
> I'm a novice user of OCaml and functional languages in general. While
> playing with the interpreter, writing all kinds of functions, I've run
> into a behavior that doesn't look quite right to me. Please excuse me,
> if it is explained somewhere and I simply haven't gotten there yet.
> 
> In the following example, I define a simple function foo that returns
> function bar, which, in turn, accepts 2 parameters. The weird part is
> that after bar is being called for the first time, its signature changes
> from polymorphic types to ints. Right after (foo 3) call it's
>   '_a -> '_b -> '_b = <fun>
> But after being called, it becomes
>   (int -> int) -> int -> int = <fun>

Type variables like '_a are covered here:

http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles

There's a mailing list for beginners' questions:

http://tech.groups.yahoo.com/group/ocaml_beginners/

Rich.

-- 
Richard Jones, CTO Merjis Ltd.
Merjis - web marketing and technology - http://merjis.com
Internet Marketing and AdWords courses - http://merjis.com/courses - NEW!
Merjis blog - http://blog.merjis.com - NEW!

Re: [Caml-list] weird type behavior

[Kirill]

(resending to the mailing list - sorry for the duplicate message)


Hello Richard and thanks for your answer.

This does explain quite a bit, but I am still stuck with other,
seemingly related, problems, which I think are too complex for
beginners' list, so I'll post it here in hope someone has an answer.

What I was really trying to do is learn Church's lambda arithmetic by
implementing it in Ocaml. The things went quite well, until I approached
PRED operation, for which results turned out to be unexpected. I won't
post here all functions in the program - only the 3 most important ones.
I'm sure no one here will have problems with car, cdr and cons
functions.


let rec create_Lnum = function
  | 0 -> let num f x = x in num
  | n ->
    let prev = create_Lnum (n-1) in
    let num f x =
      f (prev f x)
    in num
;;


let succ lnum =
  let num f x =
    f (lnum f x)
  in num
;;


let pred lnum =
  let calc_last_pair =
    lnum (
      let next_pair pair =
        let curr = car pair
        in cons (succ curr) curr
      in next_pair
    ) (
      let first_pair =
        let zero = create_Lnum 0
        in cons zero zero
      in first_pair
    )
  in cdr calc_last_pair
;;


Now, there are many things that don't work right when I'm trying to use
the above code, so I'll just throw the first one right off and let's
see, where it gets us. For this, I'll define a short helper function
inc:

# let inc x = x + 1;;
val inc : int -> int = <fun>


Now I create a lambda number and use inc function to make sure it really
calls inc 5 times:

# let five = create_Lnum 5;;
val five : ('_a -> '_a) -> '_a -> '_a = <fun>
# five inc 10;;
- : int = 15
# five;;
- : (int -> int) -> int -> int = <fun>

So far, so good, everything worked as expected. I repeat the same thing,
but now also get a five's predecessor:

# let five = create_Lnum 5;;
val five : ('_a -> '_a) -> '_a -> '_a = <fun>
# let four = pred five;;
val four : ('_a -> '_a) -> '_a -> '_a = <fun>
# five inc 10;;
This expression has type int -> int but is here used with type
  (((('a -> 'a) -> 'a -> 'a) ->
    (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a) ->
   ('a -> 'a) -> 'a -> 'a) ->
  ((('a -> 'a) -> 'a -> 'a) ->
   (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a) ->
  ('a -> 'a) -> 'a -> 'a

It doesn't work now, and the error message isn't really helpful =(
Q1: why?
Q2: how can I make it work in the expected way?

Thanks in advance,
-Kirill



On Sat, 2006-10-28 at 17:12 +0100, Richard Jones wrote:
> On Sat, Oct 28, 2006 at 05:49:08PM +0200, Kirill wrote:
> > I'm a novice user of OCaml and functional languages in general. While
> > playing with the interpreter, writing all kinds of functions, I've run
> > into a behavior that doesn't look quite right to me. Please excuse me,
> > if it is explained somewhere and I simply haven't gotten there yet.
> > 
> > In the following example, I define a simple function foo that returns
> > function bar, which, in turn, accepts 2 parameters. The weird part is
> > that after bar is being called for the first time, its signature changes
> > from polymorphic types to ints. Right after (foo 3) call it's
> >   '_a -> '_b -> '_b = <fun>
> > But after being called, it becomes
> >   (int -> int) -> int -> int = <fun>
> 
> Type variables like '_a are covered here:
> 
> http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles
> 
> There's a mailing list for beginners' questions:
> 
> http://tech.groups.yahoo.com/group/ocaml_beginners/
> 
> Rich.
> 

Re: [Caml-list] weird type behavior

[Kirill]

Hi,

Unfortunately, I wasn't able to infer, how to solve my problem from the
FAQ, nor from other sources. I can see that partial application somehow
interferes with polymorphism, and partial application does look
necessary for my task. Does it mean it's completely impossible in OCaml?
Or is there still some way to overcome the problem?

-Kirill


On Sun, 2006-10-29 at 03:05 +0200, Kirill wrote:
> On Sat, 2006-10-28 at 17:15 +0100, Richard Jones wrote:
> > I think the answer to the second part of your question is here:
> > 
> > http://caml.inria.fr/resources/doc/faq/core.en.html#eta-expansion
> > 
> > Rich.
> > 

Re: [Caml-list] weird type behavior

[Kirill]

Here's the same code as in my second message, in shorter and arguably
more readable form. createln function creates a Church's "lambda
number". succ and pred, respectively, produce successive and preceding
numbers to the given.


let rec createln = function
  | 0 -> fun f x -> x
  | n -> fun f x -> f (createln (n-1) f x)
;;

let succ lnum f x = f (lnum f x);;

let pred lnum =
  let calc_last_pair =
    lnum (
      fun pair ->
        let curr = car pair in
          cons (succ curr) curr
    ) (
      cons (createln 0) (createln 0)
    )
  in cdr calc_last_pair
;;


On Sun, 2006-10-29 at 03:12 +0200, Kirill wrote:
> Hi,
> 
> Unfortunately, I wasn't able to infer, how to solve my problem from the
> FAQ, nor from other sources. I can see that partial application somehow
> interferes with polymorphism, and partial application does look
> necessary for my task. Does it mean it's completely impossible in OCaml?
> Or is there still some way to overcome the problem?
> 
> -Kirill
> 
> 
> On Sun, 2006-10-29 at 03:05 +0200, Kirill wrote:
> > On Sat, 2006-10-28 at 17:15 +0100, Richard Jones wrote:
> > > I think the answer to the second part of your question is here:
> > > 
> > > http://caml.inria.fr/resources/doc/faq/core.en.html#eta-expansion
> > > 
> > > Rich.
> > > 

Re: [Caml-list] weird type behavior

[skaller]

On Sun, 2006-10-29 at 03:12 +0200, Kirill wrote:
> Hi,
> 
> Unfortunately, I wasn't able to infer, how to solve my problem from the
> FAQ, nor from other sources. I can see that partial application somehow
> interferes with polymorphism, and partial application does look
> necessary for my task. Does it mean it's completely impossible in OCaml?
> Or is there still some way to overcome the problem?

A limitation of Hindley-Milner type inference: 
you cannot pass a polymorphic function to a function. 

The Ocaml run-time supports this fine, but the
type inference engine is only able to cope with universal
quantification. [To be clear: the Ocaml *type system* allows it
but the inference engine cannot infer it and there's currently
no way to override the inference engine: a coercion would be
unsafe, and an annotation on the argument is a constraint applied
after inference so doesn't help]

So when you DO pass a polymorphic function
to a function, it is specialised (monomorphised) inside
the function, depending on its use. For example:

# let g x = x,x in
        let f g x y = g x, g y in
        f g 1 1.2;;
This expression has type float but is here used with type int

# let g x = x,x in
  g 1, g 1.2;;
- : (int * int) * (float * float) = ((1, 1), (1.2, 1.2))

The function g really is polymorphic here, but not inside f.
The notation 

	'_a

generally means this monormorphised version of type variable 'a:
it happens to be 'int' in the first example, so the system
prints that instead: '_a means 'some ground type we don't
know' as opposed to 'a which means 'any type'.

Ocaml will allow you to pass a polymorphic function provided
you wrap it in a class or record:

# type poly = { h : 'a . 'a -> 'a * 'a };;
type poly = { h : 'a. 'a -> 'a * 'a; }

You can see here the quantifier 'a . is localised to
the record field. Note the type 'poly' is in fact
quite monomorphic -- there's no type parameter,
one of the fields just happens to be a polymorphic
function.


# let g x = x,x in
  let f k x y = k.h x, k.h y in
  f {h=g} 1 1.2;;
- : (int * int) * (float * float) = ((1, 1), (1.2, 1.2))



-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] weird type behavior

[Boris Yakobowski]

On Sat, Oct 28, 2006 at 05:12:27PM +0100, Richard Jones wrote:
> Type variables like '_a are covered here:
> 
> http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles

Note that on this particular topic the new faq is slightly more up-to-date,
as it covers the use of objetcs or polymorphic recors to emulate first-order
polymorphism.

http://caml.inria.fr/resources/doc/faq/core.en.html#typing

(section "How to write a function with polymorphic arguments?", as well as
the two previous ones).

-- 
Boris