[Caml-list] typer strangeness (3.12.0)

[Caml-list] typer strangeness (3.12.0)

[rixed]

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?
And why didn't the compiler complain since I explicitely typed the function definition?

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

[Fabrice Le Fessant]

[-- Attachment #1: Type: text/plain, Size: 2714 bytes --]

The type constraint that you specified does not constraint the
polymorphism of the type. To declare a polymorphic constraint, you must
use (with OCaml >= 3.12.0) :

let pipe : 'a 'b 'c. ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =
  fun 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)
                | x -> x)

In which case you get the following error :
Error: This definition has type
         'a 'b. ('b, 'b) parzer -> ('a, 'b) parzer -> ('a, 'b) parzer
       which is less general than
         'c 'd 'e. ('e, 'd) parzer -> ('c, 'e) parzer -> ('c, 'd) parzer

Fabrice


On 08/06/2011 02:50 PM, 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?
> And why didn't the compiler complain since I explicitely typed the function definition?
> 
> 

[-- Attachment #2: fabrice_le_fessant.vcf --]
[-- Type: text/x-vcard, Size: 380 bytes --]

begin:vcard
fn:Fabrice LE FESSANT
n:LE FESSANT;Fabrice
org:INRIA Saclay -- Ile-de-France;P2P & OCaml
adr;quoted-printable:;;Parc Orsay Universit=C3=A9 ;Orsay CEDEX;;91893;France
email;internet:fabrice.le_fessant@inria.fr
title;quoted-printable:Charg=C3=A9 de Recherche
tel;work:+33 1 74 85 42 14
tel;fax:+33 1 74 85 42 49 
url:http://fabrice.lefessant.net/
version:2.1
end:vcard

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

[Guillaume Yziquel]

Le Saturday 06 Aug 2011 à 14:58:49 (+0200), Fabrice Le Fessant a écrit :
> The type constraint that you specified does not constraint the
> polymorphism of the type. To declare a polymorphic constraint, you must
> use (with OCaml >= 3.12.0) :
> 
> let pipe : 'a 'b 'c. ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =
>   fun 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)
>                 | x -> x)
> 
> In which case you get the following error :
> Error: This definition has type
>          'a 'b. ('b, 'b) parzer -> ('a, 'b) parzer -> ('a, 'b) parzer
>        which is less general than
>          'c 'd 'e. ('e, 'd) parzer -> ('c, 'e) parzer -> ('c, 'd) parzer
> 
> Fabrice

You can achieve a similar goal with stuff like:

# let f (type a) (type b) (x : a) = (x : b);;
Error: This expression has type a but an expression was expected of type b

The benefit of which is that you do not have f explicitely quantified as
opposed to the "let f : 'a 'b. ..." alternative. Feels more ocaml-ish to
me.

-- 
     Guillaume Yziquel

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

[rixed]

Thank you for your answers, but you aimed too high above my
understanding :-)

-[ Sat, Aug 06, 2011 at 02:58:49PM +0200, Fabrice Le Fessant ]----
> The type constraint that you specified does not constraint the
> polymorphism of the type. To declare a polymorphic constraint, you must
> use (with OCaml >= 3.12.0) :
> 
> let pipe : 'a 'b 'c. ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =

Never saw this notation before. I checked in the manual but beside in
the language grammar (in the definition of a poly-typexpr) I could find
more explanation.
Is it explained somewhere why this notation was required and why this:

let pipe : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =

is not enough? What's adding the "'a 'b 'c. " exactly ? I understand
that it forbids ocaml to consider that the various 'a (for instance) may
be differents 'a, but I don't understand why ocaml migh do that in the
first place (especially to produce a _less general_ type than the one
given) ? If it's not a bug, then what's the purpose ?

As for my second question, I received no answer (was: why changing the
pattern match for something that should be equivalent changes the infered
type). If you suspect this can be a bug then I can look for a simple
reproductible case.

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

[Guillaume Yziquel]

Le Sunday 14 Aug 2011 à 08:19:59 (+0200), rixed@happyleptic.org a écrit :
> Thank you for your answers, but you aimed too high above my
> understanding :-)
> 
> -[ Sat, Aug 06, 2011 at 02:58:49PM +0200, Fabrice Le Fessant ]----
> > The type constraint that you specified does not constraint the
> > polymorphism of the type. To declare a polymorphic constraint, you must
> > use (with OCaml >= 3.12.0) :
> > 
> > let pipe : 'a 'b 'c. ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =
> 
> Never saw this notation before. I checked in the manual but beside in
> the language grammar (in the definition of a poly-typexpr) I could find
> more explanation.
> Is it explained somewhere why this notation was required and why this:
> 
> let pipe : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =
> 
> is not enough? What's adding the "'a 'b 'c. " exactly ?

It does explicit universal quantification on the type. So you create a
monomorphic type out of that. \forall 'a. 'a -> 'a is a type for
functions that can be used as int -> int, float -> float, string ->
string, etc...

\forall 'a. 'a -> 'a is not a polymorphic type as 'a is bound.

By contrast, 'a -> 'a is polymorphic in the sense that is does depend on
the 'a to form a monomorphic type.

> I understand
> that it forbids ocaml to consider that the various 'a (for instance) may
> be differents 'a, but I don't understand why ocaml migh do that in the
> first place (especially to produce a _less general_ type than the one
> given) ? If it's not a bug, then what's the purpose ?

Allowing universal quantification of types allows you to have a richer
type system. Such as system F or ML^F. Typical issues it helps to solve
are existential types or polymorphic recursion.

It does more than simply force the various 'a to be distinct. It also
binds them to form a monomorphic type. If you just want the types to be
different, but not bound, you have the (type s) syntax to introduce
types explicitely.

> As for my second question, I received no answer (was: why changing the
> pattern match for something that should be equivalent changes the infered
> type). If you suspect this can be a bug then I can look for a simple
> reproductible case.

It's likely not a bug.

What you did is replace | Fail -> Fail | Wait -> Wait by | x -> x. If
you take into consideration the fact that Fail and Wait are constructors
for a polymorphic type, what you have in the clauses and what is
returned may have different types because you have not unified the type
parameters of this datatype. However, when you write | x -> x, you unify
x and x, and hence unify the type parameters.

That likely explains what you observe.

-- 
     Guillaume Yziquel

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

[rixed]

Thank you very much for these additional explanations.
Not that I understood much, but next time I encounter such
a strange behavior I will know that my simple programs are
made more complex because it's helping some superior lifeform
somewhere in the galaxy to make much more complex programs. :)

(that plus the browser cache-thing, I feel exta stupid this morning :))

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

[Jacques Garrigue]

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