UsingPolymorphic Variants

UsingPolymorphic Variants

[Christian Stork]

Basic Question:  

    Why aren't polymorphic variants coerced by default?

My Situation:

I am automatically generating some code that uses polymorphic variants
extensively.  The inferred types are very complicated.  Unfortunatly, at
some points in my code coercions are needed for it to compile.  Since I
don't have the types available when I generate the code (and I don't
think it's possible to refer to inferred types in coercions) I can't
coerce explicitly.  I'd like to be able to say something like:

    ... f (x: type_of_x :> type_expected_by_f) ...

Anyway, that's why I'm wondering why the compiler doesn't automatically
coerce or, at least, offer a switch with this functionality.

Thanks for your time,
Chris

-- 
Chris Stork   <>  Support eff.org!  <>   http://www.ics.uci.edu/~cstork/
OpenPGP fingerprint:  B08B 602C C806 C492 D069  021E 41F3 8C8D 50F9 CA2F

Re: [Caml-list] Using Polymorphic Variants

[Christian Stork]

On Sun, Oct 02, 2005 at 10:43:42AM +0200, Jean-Marie Gaillourdet wrote:
> Christian Stork schrieb:
> > Basic Question:  

> >     Why aren't polymorphic variants coerced by default?

> I guess there is some undecidability involved.

My guess too, but I'd like to be sure. ;-)

> > I am automatically generating some code that uses polymorphic variants
> > extensively.  The inferred types are very complicated.  Unfortunatly, at
> > some points in my code coercions are needed for it to compile.  Since I
> > don't have the types available when I generate the code (and I don't
> > think it's possible to refer to inferred types in coercions) I can't
> > coerce explicitly.  I'd like to be able to say something like:

> >     ... f (x: type_of_x :> type_expected_by_f) ...
> Isn't it possible to write something like that:

>  (f: 'a) (x: type_of_x :> 'a)

> I didn't test that trick.

Nice idea.  Let's see:


# type ab  = [ `Apple | `Banana ]
  type abo = [ ab | `Orange]
  let f (x:abo) = match x with #ab -> "ab" | #abo -> "orange"
  let a = (`Apple:ab);;
type ab = [ `Apple | `Banana ]
type abo = [ `Apple | `Banana | `Orange ]
val f : abo -> string = <fun>
val a : ab = `Apple
# f (a:>abo);;
- : string = "ab"
# (f:'a->_) (a:ab:>'a);;
Characters 10-20:
  (f:'a->_) (a:ab:>'a);;
            ^^^^^^^^^^
Type ab = [ `Apple | `Banana ] is not a subtype of type
  abo = [ `Apple | `Banana | `Orange ] 
The first variant type does not allow tag(s) `Orange
# (f:'a->_) (a:>'a);;
Characters 11-12:
  (f:'a->_) (a:>'a);;
             ^
This expression cannot be coerced to type
  abo = [ `Apple | `Banana | `Orange ];
it has type ab but is here used with type abo
The first variant type does not allow tag(s) `Orange


I'm confused about the error message saying that ab is not a subtype of
abo.  I thought it is...

-- 
Chris Stork   <>  Support eff.org!  <>   http://www.ics.uci.edu/~cstork/
OpenPGP fingerprint:  B08B 602C C806 C492 D069  021E 41F3 8C8D 50F9 CA2F

Re: [Caml-list] Using Polymorphic Variants

[Jacques Garrigue]

From: Christian Stork <cstork@ics.uci.edu>
> On Sun, Oct 02, 2005 at 10:43:42AM +0200, Jean-Marie Gaillourdet wrote:
> > Christian Stork schrieb:
> > > Basic Question:  
> 
> > >     Why aren't polymorphic variants coerced by default?
> 
> > I guess there is some undecidability involved.
> 
> My guess too, but I'd like to be sure. ;-)

Not really undecidable, but you would have to completely change the
way types are inferred, and accept type schemes with subtyping
constraints (cf. HM(X)).
Keeping all the subtyping explicit makes things simpler.
So there is no plan to change this.

> > >     ... f (x: type_of_x :> type_expected_by_f) ...
> > Isn't it possible to write something like that:
> >  (f: 'a) (x: type_of_x :> 'a)

The subtyping algorithm only looks at explicit types, so the sharing of
'a has no effect. In simple cases (with no recursive types), the
following will work:
  (c : type_of_x :> [> type_of_x ])

Jacques Garrigue