Re: [Caml-list] typer strangeness (3.12.0)

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2011/08/06, at 21:50, rixed@happyleptic.org wrote:

> Given these types:
> 
> (* A parser is given a list of items and returns either a Failure indication, a
>   Wait for more inputs indication, or a result (composed of a new value and the list
>   of tokens that were unused) *)
> type ('a, 'b) parzer_result = Wait | Res of ('a * 'b list) | Fail
> type ('a, 'b) parzer = 'b list -> ('a, 'b) parzer_result
> 
> And this function used to pipe two parsers together:
> 
> (* Use the results of the first parser as the input elements of the second.
>   Stop as soon as p2 returns a result or fails.
>   Notice that if p1 is a ('a, 'b) parzer and p2 a ('c, 'a) parzer
>   then pipe p1 p2 is a ('c, 'b) parzer, which comes handy but p2 is then
>   forced to consume everything ! *)
> let (pipe : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer) p1 p2 =
>    let p1_rem = ref [] in
>    fun bs -> match p1 (!p1_rem @ bs) with
>        | Fail -> Fail
>        | Wait -> Wait
>        | Res (res, rem) ->
>            p1_rem := rem ;
>            (match p2 [res] with
>                | Res (res', rem') ->
>                    if rem' <> [] then Printf.printf "WRN: second end of a pipe did not consume eveything !\n" ;
>                    Res (res', !p1_rem)
>                | Fail -> Fail | Wait -> Wait)
> 
> This pipe function has the expected type :
> 
> # pipe;;
> - : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer = <fun>
> 
> Now, if I change it's last line for : "| x -> x)", ie not repeating Wait and Fail, the result is
> very different :
> 
> # pipe;;
> - : ('a, 'a) parzer -> ('b, 'a) parzer -> ('b, 'a) parzer = <fun>
> 
> How come?

If you write "x -> x", the output of p1 is forced to be the same type as the output of the function,
which forces the unification of 'a and 'b. Note that this second type is equivalent to
> - : ('a, 'a) parzer -> ('c, 'a) parzer -> ('c, 'a) parzer = <fun>

If you explicitly write "Fail -> Fail | Wait -> Wait", no such unification happens, and you get
the intended type.
You can get the same behaviour by writing "Fail | Wait as x -> x", i.e. the type checker is clever
enough to not unify the pattern type and the variable type.

> And why didn't the compiler complain since I explicitely typed the function definition?


You already got your answer. A simple type annotation does not enforce polymorphism.

Hope this helps,

	Jacques