Why type inference fails in this code

Why type inference fails in this code

[rouanvd]

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.

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

[Vincent Aravantinos]

Le 9 oct. 09 à 07:25, rouanvd@softwarerealisations.com a écrit :

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

BTW:

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

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

[Gabriel Kerneis]

On Fri, Oct 09, 2009 at 07:25:41AM +0200, rouanvd@softwarerealisations.com wrote:
> ======================================================
> 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.

> 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,
-- 
Gabriel Kerneis

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

[Virgile Prevosto]

Hello,

Le ven. 09 oct. 2009 09:09:35 CEST,
Gabriel Kerneis <kerneis@pps.jussieu.fr> a écrit :

> On Fri, Oct 09, 2009 at 07:25:41AM +0200, rouanvd@softwarerealisations.com wrote:
> > ======================================================
> > 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.
> 

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
;;

but personally I'd do the same thing as you:
> 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
> ;;

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

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

[Gabriel Kerneis]

On Fri, Oct 09, 2009 at 10:22:18AM +0200, Virgile Prevosto wrote:
> 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

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

[Gabriel Kerneis]

On Fri, Oct 09, 2009 at 10:41:35AM +0200, Gabriel Kerneis wrote:
> 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!
-- 
Gabriel

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

[Jeremy Yallop]

Dear Rouan,

2009/10/9  <rouanvd@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.