[Caml-list] Recursive fixed polymorphic variants

[Caml-list] Recursive fixed polymorphic variants

[Jacques-Pascal Deplaix]

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

Hi,

I have a problem with this test-case which doesn't compile:

module M : sig
  type a = [`A]
  type 'a b = [`B of 'a]

  val a : unit -> a
  val b : 'a -> 'a b
end = struct
  type a = [`A]
  type 'a b = [`B of 'a ]

  let a () = `A
  let b x = `B x
end;;

let rec f = function `B x -> f x | `A -> ();;

f (M.b (M.a ()));;

and produce the following error:

Error: This expression has type M.a M.b = [ `B of M.a ]
       but an expression was expected of type [< `B of 'a ] as 'a
       Type M.a = [ `A ] is not compatible with type M.a M.b = [ `B of
M.a ]
       These two variant types have no intersection

The thing is, if we define M.a and M.b with « unit -> [> a ] » and « 'a
-> [> 'a b ] », it does compile but I don't know why the previous code
doesn't.

Does somebody have any hints ?

[-- Attachment #2: Type: text/html, Size: 1343 bytes --]

Re: [Caml-list] Recursive fixed polymorphic variants

[Erkki Seppala]

Hello,

Jacques-Pascal Deplaix <jp.deplaix@gmail.com> writes:

> let rec f = function `B x -> f x | `A -> ();;

The problem is that 'f' has two final types in the same scope - or
that's the best way I can describe it, someone can maybe chime in
:). One way to solve it for this instance would be:

let rec f = function `B x -> g x | `A -> ()
and g = function `B x -> f x | `A -> ();;

# f (M.b (M.a ()))
- : unit = ()

This gives f (and g) the inferred type ([< `A | `B of [< `A | `B of 'a
] ] as 'a) -> unit.

I was under the impression I should be able to describe using the type
variable syntax in function type, but I was unable to.

-- 
  _____________________________________________________________________
     / __// /__ ____  __               http://www.modeemi.fi/~flux/\   \
    / /_ / // // /\ \/ /                                            \  /
   /_/  /_/ \___/ /_/\_\@modeemi.fi                                  \/

Re: [Caml-list] Recursive fixed polymorphic variants

[Leo White]

> let rec f = function `B x -> g x | `A -> ()
> and g = function `B x -> f x | `A -> ();;
>
> # f (M.b (M.a ()))
> - : unit = ()
>
> This gives f (and g) the inferred type ([< `A | `B of [< `A | `B of 'a
> ] ] as 'a) -> unit.
>
> I was under the impression I should be able to describe using the type
> variable syntax in function type, but I was unable to.

Note that you can use polymorphic recursion to give f a very similar
type that also works for this particular example:

  # let rec f : 'a. ([< `A | `B of ([< `A | `B of 'b ] as 'b) ] as 'a) -> unit = 
      function `B x -> f x | `A -> ();;
    val f : [< `A | `B of [< `A | `B of 'a ] as 'a ] -> unit = <fun>
  # f (M.b (M.a ()));;
  - : unit = ()

Regards,

Leo

Re: [Caml-list] Recursive fixed polymorphic variants

[Leo White]

>
> The thing is, if we define M.a and M.b with « unit -> [> a ] » and « 'a -> [> 'a b ] », it does compile but I don't
> know why the previous code doesn't.
>
> Does somebody have any hints ?

Your f function expects an argument of type:

  ([< `A | `B of 'a ] as 'a)

whilst (M.b (M.a ())) has type:

  [`B of [`A]]

If you try to unify these two types, you have to unify 'a with both [`A]
and [`B of [`A]]. These types can't be unified since they are both
closed and are not equal.

If you change the definitions of M.a and M.b as you described, then (M.b
(M.a ())) has type:

  [> `B of [> `A]]

If you try to unify this with the type of f's argument, you unify 'a
with [> `A] and [> `B of [> `A]]. These types can be unified because
they are both open and are not incompatible.

Note that you can use subtyping to give the original (M.b (M.a ())) the
type:

  ([`A | `B of 'a] as 'a)

which *is* unifiable with the argument type of f:

  f (M.b (M.a ()) :> [`A | `B of 'a] as 'a)

Regards,

Leo

Re: [Caml-list] Recursive fixed polymorphic variants

[Jacques-Pascal Deplaix]

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

Mmmh I see. Thanks for your answer.

I spent hours to understand how ([< `A | `B of 'a ] 'a) was transformed
into ([< `B of 'a ] as 'a) and I did not saw the influence of the
polymorphism in the type-checking.

Thanks again.

On 05/28/2013 10:13 AM, Leo White wrote:
>> The thing is, if we define M.a and M.b with « unit -> [> a ] » and « 'a -> [> 'a b ] », it does compile but I don't
>> know why the previous code doesn't.
>>
>> Does somebody have any hints ?
> Your f function expects an argument of type:
>
>   ([< `A | `B of 'a ] as 'a)
>
> whilst (M.b (M.a ())) has type:
>
>   [`B of [`A]]
>
> If you try to unify these two types, you have to unify 'a with both [`A]
> and [`B of [`A]]. These types can't be unified since they are both
> closed and are not equal.
>
> If you change the definitions of M.a and M.b as you described, then (M.b
> (M.a ())) has type:
>
>   [> `B of [> `A]]
>
> If you try to unify this with the type of f's argument, you unify 'a
> with [> `A] and [> `B of [> `A]]. These types can be unified because
> they are both open and are not incompatible.
>
> Note that you can use subtyping to give the original (M.b (M.a ())) the
> type:
>
>   ([`A | `B of 'a] as 'a)
>
> which *is* unifiable with the argument type of f:
>
>   f (M.b (M.a ()) :> [`A | `B of 'a] as 'a)
>
> Regards,
>
> Leo


[-- Attachment #2: Type: text/html, Size: 1847 bytes --]