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

[Fabrice Le Fessant <Fabrice.Le_fessant@inria.fr>]

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