Re: [Caml-list] weird type behavior

[Kirill <kirillkh@gmail.com>]

(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.
>