[Caml-list] Why type inference fails in this code

[r***@softwarerealisations.com]

Hi everyone

I am trying to decide what language to use to write a compiler for my own
programming language.
I am leaning towards OCaml, but I don’t want the type system or debugging
tools to be a problem.

I found this code snippet in a post and was wondering why the type
inference messes up with
The following code:

======================================================
type t = MyInt of int | MyFloat of float | MyString of string ;;

let foo printerf = function
| MyInt i -> printerf string_of_int i
| MyFloat x -> printerf string_of_float x
| MyString s -> printerf (fun x -> x) s
;;
======================================================

I have done the same thing in Haskell and it correctly infers the type of
foo.

I read that there are lots of workarounds for the above code snippet, but
I would like to
Know why this code fails and what is the best workaround for this type of
code.

Regards
Rouan.


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Vincent Aravantinos]

Post by r***@softwarerealisations.com
======================================================
type t = MyInt of int | MyFloat of float | MyString of string ;;
let foo printerf = function
| MyInt i -> printerf string_of_int i
| MyFloat x -> printerf string_of_float x
| MyString s -> printerf (fun x -> x) s
;;
======================================================
I read that there are lots of workarounds for the above code
snippet, but
I would like to
Know why this code fails and what is the best workaround for this type of
code.

You might find some answers here:
http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#arguments_polymorphes
Though this won't clearly tell you "why", and I sadly don't know the
answer.

From my experience the type system limitations are not so big
hindrance in practice,
you may have to work a bit to get what you want fit in the type system,
but I've never found a thing that wouldn't work at all.

Post by r***@softwarerealisations.com
I have done the same thing in Haskell and it correctly infers the type of
foo.

It doesn't work for me with ghc 6.10.3.
I mean, unless you provided the Haskell compiler with some type
annotations the same error occurs.
But I am not a haskell expert so I may be wrong.

V.
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Gabriel Kerneis]

Post by r***@softwarerealisations.com
======================================================
type t = MyInt of int | MyFloat of float | MyString of string ;;
let foo printerf = function
| MyInt i -> printerf string_of_int i
| MyFloat x -> printerf string_of_float x
| MyString s -> printerf (fun x -> x) s
;;
======================================================

Type-inference has nothing to do with it, it's the type system itself
which fails.

What is the type you would expect? I guess:
(forall 'a. ('a -> string) -> 'a -> 'b) -> t -> 'b

This is impossible with Ocaml: you cannot have a universal quantifier,
type variables are existantially quantified.

Post by r***@softwarerealisations.com
I read that there are lots of workarounds for the above code snippet,
but I would like to Know why this code fails and what is the best
workaround for this type of code.

You have many ways to emulate universal types in Ocaml (objects,
records) and browsing the archives of this list should provide many good
examples.

In you very specific case, though, I guess refactoring it is possible:
let foo printerf = function
| MyInt i -> printerf (string_of_int i)
| MyFloat x -> printerf (string_of_float x)
| MyString s -> printerf s
;;

(depending on what your printerf function does, but I can't find any
counter-example)

Regards,

[Virgile Prevosto]

Hello,

Le ven. 09 oct. 2009 09:09:35 CEST,

Post by Gabriel Kerneis

Post by r***@softwarerealisations.com
======================================================
type t = MyInt of int | MyFloat of float | MyString of string ;;
let foo printerf = function
| MyInt i -> printerf string_of_int i
| MyFloat x -> printerf string_of_float x
| MyString s -> printerf (fun x -> x) s
;;
======================================================

Type-inference has nothing to do with it, it's the type system itself
which fails.
(forall 'a. ('a -> string) -> 'a -> 'b) -> t -> 'b
This is impossible with Ocaml: you cannot have a universal quantifier,
type variables are existantially quantified.

Well, I'm afraid this the other way round: a polymorphic type in Ocaml
is implicitly universally quantified: (fun x->x : 'a -> 'a) means the
identity function can be applied to an argument of any type, not that
there exists a type 'a on which you can apply it.
In addition, the desired type for printerf is indeed an existential
one (printerf: exists 'a. 'a -> string -> 'a -> 'b): you don't want the
first argument to convert any type to a string, just the type of the
second argument.

A possible but very heavy solution would be to use functors and local
modules everywhere (I guess that Haskell's typeclasses would help here).

type t = MyInt of int | MyFloat of float | MyString of string ;;

module type Printerf=functor(A:sig type t val to_string: t -> string
end) -> sig val print: A.t -> unit
end

module Foo(Printerf:Printerf) = struct
let foo = function
| MyInt i ->
let module M = Printerf(struct type t = int
let to_string = string_of_int end)
in M.print i
| MyFloat x ->
let module M = Printerf(struct type t = float
let to_string = string_of_float end)
in M.print x
| MyString s ->
let module M = Printerf(struct type t = string
let to_string = fun x -> x end)
in M.print s
end
;;

Post by Gabriel Kerneis
let foo printerf = function
| MyInt i -> printerf (string_of_int i)
| MyFloat x -> printerf (string_of_float x)
| MyString s -> printerf s
;;

--
E tutto per oggi, a la prossima volta.
Virgile

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Gabriel Kerneis]

Post by Virgile Prevosto
Well, I'm afraid this the other way round

Yes, sorry, I should have checked before posting since I always get it
wrong, confusing forall and exists.

Regards,

[Gabriel Kerneis]

Post by Gabriel Kerneis
Yes, sorry, I should have checked before posting since I always get it
wrong, confusing forall and exists.

And just in case someone else on this list does not understand (or
remember) the difference, he should read the following thread:
http://caml.inria.fr/pub/ml-archives/caml-list/2007/05/08f6ca7a2c045d2801f2a2cc0ae8aa63.en.html

Enlighting!

[Jeremy Yallop]

Dear Rouan,

Post by r***@softwarerealisations.com
type t = MyInt of int | MyFloat of float | MyString of string ;;
let foo printerf = function
 | MyInt i -> printerf string_of_int i
 | MyFloat x -> printerf string_of_float x
 | MyString s -> printerf (fun x -> x) s

This fails because the variable "printerf" is used at different types
inside the body of foo. OCaml's type system requires function
arguments to be used at the same type everywhere they appear in the
body of the function. The reason is simple: without this restriction
type inference becomes undecidable.

The most reasonable type for foo seems like the following:

forall 'b. (forall 'a. ('a -> string) -> 'a -> 'b) -> t -> 'b

which is the type of a function that constructs a value of type 'b
from a value of type t using its argument function; this argument
function takes a printer for any type 'a and a value of type 'a and
constructs a value of type 'b.

We can make two adjustments to "foo" to turn it into something that
OCaml will accept. The first adjustment is to turn the argument
"printerf" into an object with a single method; polymorphic types
(i.e. types that use "forall") in OCaml must be wrapped in object or
record types. The second adjustment is to provide a type signature,
which changes the impossible problem of type /inference/ into the
easier problem of type /checking/. Here is the revised definition:

let foo : < p : 'a . ('a -> string) -> 'a -> 'b > -> t -> 'b =
fun printerf -> function
| MyInt i -> printerf#p string_of_int i
| MyFloat x -> printerf#p string_of_float x
| MyString s -> printerf#p (fun x -> x) s

In order to call this function we must, of course, ensure that the
first argument is an object. Here is a simple example, where the
argument just returns the constructed string:

foo (object method p : 'a. ('a -> string) -> 'a -> string = fun x
-> x end) (MyInt 3)

Hope this helps,

Jeremy.

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs