Why is this coercion necessary?

Why is this coercion necessary?

[Jacques Carette]

Here is a much simplified version from a (much) larger problem I have 
recently encountered:

type 'a a = [`A of 'a b]
and 'a b  = [`B of 'a a]
and 'a c  = [`C ]

type 'a d = [ 'a a | 'a b | 'a c]
type e = e d

# this code gives an error (details below)
let f1 (x:e) : e = match x with
    | `A n -> n
    | `B n -> n
    | `C   -> `C

# this works
let f2 (x:e) : e = match x with
    | `A n -> (n :> e)
    | `B n -> (n :> e)
    | `C   -> `C

f1 gives an error  on the "| `B n -> n" line, pointing to the second 'n' 
with
This expression has type e a but is used with type e b
These two variant types have no intersection

Indeed, they have no intersection, but they have a union!  That is what 
it seems the coercion in f2 'forces' the type-checker to realize, and 
all works fine.  But of course, such coercions end up polluting my code 
all over the place (since the actual example is made of 9 types with 20 
tags in total, and the 'recursive knot' requires 2 parameters to close 
properly).

So, is this a bug?  Is there a way to avoid these coercions?

Jacques

Re: [Caml-list] Why is this coercion necessary?

[Lukasz Stafiniak]

There is no way to avoid coercions altogether: OCaml doesn't have
inference for subtyping, using unification with row variables gives
the intersection behavior. But the language could be changed, with a
syntax like

match x return e with
| ... -> ...
| ... -> ...

meaning that all branches should be coerced to e.

On Thu, Aug 14, 2008 at 4:18 AM, Jacques Carette <carette@mcmaster.ca> wrote:
> Here is a much simplified version from a (much) larger problem I have
> recently encountered:
>
> type 'a a = [`A of 'a b]
> and 'a b  = [`B of 'a a]
> and 'a c  = [`C ]
>
> type 'a d = [ 'a a | 'a b | 'a c]
> type e = e d
>
> # this code gives an error (details below)
> let f1 (x:e) : e = match x with
>   | `A n -> n
>   | `B n -> n
>   | `C   -> `C
>
> # this works
> let f2 (x:e) : e = match x with
>   | `A n -> (n :> e)
>   | `B n -> (n :> e)
>   | `C   -> `C
>
> f1 gives an error  on the "| `B n -> n" line, pointing to the second 'n'
> with
> This expression has type e a but is used with type e b
> These two variant types have no intersection
>
> Indeed, they have no intersection, but they have a union!  That is what it
> seems the coercion in f2 'forces' the type-checker to realize, and all works
> fine.  But of course, such coercions end up polluting my code all over the
> place (since the actual example is made of 9 types with 20 tags in total,
> and the 'recursive knot' requires 2 parameters to close properly).
>
> So, is this a bug?  Is there a way to avoid these coercions?
>
> Jacques
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Why is this coercion necessary?

[Lukasz Stafiniak]

Of course OCaml doesn't need to be changed, just write a syntax
extension in campl4.

On Thu, Aug 14, 2008 at 1:21 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> There is no way to avoid coercions altogether: OCaml doesn't have
> inference for subtyping, using unification with row variables gives
> the intersection behavior. But the language could be changed, with a
> syntax like
>
> match x return e with
> | ... -> ...
> | ... -> ...
>
> meaning that all branches should be coerced to e.
>

Re: [Caml-list] Why is this coercion necessary?

[Martin Jambon]

On Wed, 13 Aug 2008, Jacques Carette wrote:

> Here is a much simplified version from a (much) larger problem I have 
> recently encountered:
>
> type 'a a = [`A of 'a b]
> and 'a b  = [`B of 'a a]
> and 'a c  = [`C ]
>
> type 'a d = [ 'a a | 'a b | 'a c]
> type e = e d
>
> # this code gives an error (details below)
> let f1 (x:e) : e = match x with
>   |  `A n -> n
>   |  `B n -> n
>   |  `C   -> `C
>
> # this works
> let f2 (x:e) : e = match x with
>   |  `A n -> (n :> e)
>   |  `B n -> (n :> e)
>   |  `C   -> `C
>
> f1 gives an error  on the "| `B n -> n" line, pointing to the second 'n' with
> This expression has type e a but is used with type e b
> These two variant types have no intersection
>
> Indeed, they have no intersection, but they have a union!  That is what it 
> seems the coercion in f2 'forces' the type-checker to realize, and all works 
> fine.  But of course, such coercions end up polluting my code all over the 
> place (since the actual example is made of 9 types with 20 tags in total, and 
> the 'recursive knot' requires 2 parameters to close properly).
>
> So, is this a bug?  Is there a way to avoid these coercions?


The following works, but I doubt it would make your code shorter:


type 'a a = [`A of 'a b]
and 'a b  = [`B of 'a a]
and 'a c  = [`C ]

type 'a d = [ 'a a | 'a b | 'a c]
type e = e d

type f = [`A of e | `B of e | `C ]

let f3 (x:e) : e = match (x :> f) with
    | `A n -> n
    | `B n -> n
    | `C   -> `C


Martin

--
http://mjambon.com/