[Caml-list] Naming polymorphic variant types

[Caml-list] Naming polymorphic variant types

[Nick Alexander]

Hi all,

Here's a file...

module type TEST = sig
  type outer = [`A | `B]
  type inner = [`B]

  val x : outer -> outer
  val y : inner
end

module Test : TEST = struct
  type outer = [`A | `B]
  and inner = [`B]

  let x o = match o with
  | `A -> `A
  | `B -> `A

  let y = `B
end

let p = Test.y
let q = Test.x p

That when evaluated, produces...

# #use "C:/Program Files/Objective Caml/test.ml";;
module type TEST =
  sig
    type outer = [ `A | `B]
    and inner = [ `B]
    val x : outer -> outer
    val y : inner
  end
module Test : TEST
val p : Test.inner = `B
File "C:/Program Files/Objective Caml/sql5.ml", line 21, characters 15-16:
This expression has type Test.inner = [ `B] but is here used with type
  Test.outer = [ `A | `B]
The first variant type does not allow tag(s) `A

I'm confused.  Can I get an explanation for why the parameter to a
function with a sum variant type needs all summands to be possible
arguments?  I'm sure I'm misunderstanding the subtyping relationship, but
I can't hack it.  This all grew out of a desire to document code by naming
polymorphic variant types, a questionable capability at best.
Any light appreciated,
Nick Alexander


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Naming polymorphic variant types

[Jacques Garrigue]

From: "Nick Alexander" <nalexander@amavi.com>

> module type TEST =
>   sig
>     type outer = [ `A | `B]
>     and inner = [ `B]
>     val x : outer -> outer
>     val y : inner
>   end
> module Test : TEST
> # let p = Test.y;;
> val p : Test.inner = `B
> # let q = Test.x p;;
>                  ^
> This expression has type Test.inner = [ `B] but is here used with type
>   Test.outer = [ `A | `B]
> The first variant type does not allow tag(s) `A
>
> I'm confused.  Can I get an explanation for why the parameter to a
> function with a sum variant type needs all summands to be possible
> arguments? 

Inner is a subtype of outer, but they cannot be unified (unification
requires equality, not subtyping).
 
You can get subtyping by writing explicit coercions:

# let q = Test.x (p :> Test.outer);;
val q : Test.outer = `A

You can also give polymorphic types to your values in the interface:
  val x : [< outer] -> outer
and
  val y : [> inner]
are both valid, and one of them is enough to allow (Test.x p) without
coercion. I.e., [< outer] can be unified with inner, and [> inner] can
be unified with outer.

        Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Naming polymorphic variant types

[Nick Alexander]

> From: "Nick Alexander" <nalexander@amavi.com>
>
>> module type TEST =
>>   sig
>>     type outer = [ `A | `B]
>>     and inner = [ `B]
>>     val x : outer -> outer
>>     val y : inner
>>   end
>> module Test : TEST
>> # let p = Test.y;;
>> val p : Test.inner = `B
>> # let q = Test.x p;;
>>                  ^
>> This expression has type Test.inner = [ `B] but is here used with type
>>   Test.outer = [ `A | `B]
>> The first variant type does not allow tag(s) `A
>>
>> I'm confused.  Can I get an explanation for why the parameter to a
>> function with a sum variant type needs all summands to be possible
>> arguments?
>
> Inner is a subtype of outer, but they cannot be unified (unification
> requires equality, not subtyping).
>
> You can get subtyping by writing explicit coercions:
>
> # let q = Test.x (p :> Test.outer);;
> val q : Test.outer = `A
>
> You can also give polymorphic types to your values in the interface:
>  val x : [< outer] -> outer
> and
>  val y : [> inner]
> are both valid, and one of them is enough to allow (Test.x p) without
> coercion. I.e., [< outer] can be unified with inner, and [> inner] can
> be unified with outer.

Thank you Jacques.  I didn't know that you could name < and > types in
type declarations.  Perfect :)
Now, can anyone point me at docs about polymorphic records?  I can't find
a thing :(  They were mentioned in the 3.05 release notes as'- Support for polymorphic methods and record fields.'
which could be an extension of the object-based polymorphic records or a
really useful extension like the polymorphic variants.
Cheers,
Nick


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Naming polymorphic variant types

[Jacques Garrigue]

From: "Nick Alexander" <nalexander@amavi.com>
> Now, can anyone point me at docs about polymorphic records?  I can't find
> a thing :(  They were mentioned in the 3.05 release notes as'-
> Support for polymorphic methods and record fields.' 
> which could be an extension of the object-based polymorphic records or a
> really useful extension like the polymorphic variants.

Oops, you didn't parser the above sentence correctly.
What 3.05 adds is "polymorphic methods" and "polymorphic record
fields", but not "polymorphic records" (you still have to simulate
them with objects).  Polymorphic record fields are shortly described
in the core language part of the tutorial; they provide explicit
polymorhism at the record field level, which may be light than going
through objects and methods.

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Naming polymorphic variant types -- additional questions

[Nick Alexander]

> From: "Nick Alexander" <nalexander@amavi.com>
>
>> module type TEST =
>>   sig
>>     type outer = [ `A | `B]
>>     and inner = [ `B]
>>     val x : outer -> outer
>>     val y : inner
>>   end
>> module Test : TEST
>> # let p = Test.y;;
>> val p : Test.inner = `B
>> # let q = Test.x p;;
>>                  ^
>> This expression has type Test.inner = [ `B] but is here used with type
>>   Test.outer = [ `A | `B]
>> The first variant type does not allow tag(s) `A
>>
>> I'm confused.  Can I get an explanation for why the parameter to a
>> function with a sum variant type needs all summands to be possible
>> arguments?
>
> Inner is a subtype of outer, but they cannot be unified (unification
> requires equality, not subtyping).
>
> You can get subtyping by writing explicit coercions:
>
> # let q = Test.x (p :> Test.outer);;
> val q : Test.outer = `A
>
> You can also give polymorphic types to your values in the interface:
>  val x : [< outer] -> outer
> and
>  val y : [> inner]
> are both valid, and one of them is enough to allow (Test.x p) without
> coercion. I.e., [< outer] can be unified with inner, and [> inner] can
> be unified with outer.

When I was trying this, I accidently tried:
type outer = [< 'A | 'B]
and was duly rewarded with
Unbound type parameter [..]

I understand that this is not what Jacques recommended!  I'm wondering if
someone can tell me what this means, and when this construction could
possibly be necessary.
I am also a neophyte polymorphic variants user.  It seems very intuitive
to me that [`A] is a subtype of [`A | `B].  Jacques informs me that
unification rejects the subtyping in favour of equality.  So, what is the
situation where [`A] is _not_ a subtype of [`A | `B]?  Ie, what common
construct, design pattern, or idiom reflects this?
Thanks for the great support,
Nick



-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Naming polymorphic variant types -- additional questions

[Jacques Garrigue]

From: "Nick Alexander" <nalexander@amavi.com>
> When I was trying this, I accidently tried:
> type outer = [< 'A | 'B]
> and was duly rewarded with
> Unbound type parameter [..]

OK, [< t] and [> t] types contain an hidden type variable.
If you really want to define a polymorphic type, you must write

   type 'a outer = 'a constraint 'a = [< `A | `B]

Looks a bit confusing? This just means that ('a outer) can unify with
anything included in [< `A | `B]

> I am also a neophyte polymorphic variants user.  It seems very intuitive
> to me that [`A] is a subtype of [`A | `B].  Jacques informs me that
> unification rejects the subtyping in favour of equality.  So, what is the
> situation where [`A] is _not_ a subtype of [`A | `B]?  Ie, what common
> construct, design pattern, or idiom reflects this?

[`A] _is_ a subtype of [`A | `B]. The point is just that in ocaml
subtyping is not implicit, like it is in most OO languages.
     fun (x : [`A]) -> (x :> [`A|`B]) ,
where :> denotes an explicit coercion, is typable, showing the
subtyping relation.

In ocaml, the implicit subsumption relation is instanciation rather
than subtyping. While subtyping makes function arguments
contravariant, with instanciation everything is "covariant", which has
some advantages, but clearly doesn't mix well with subtyping.

Polymorphic variants are based on instanciation: a polymorphic variant
type can be seen as a constraint on the values that may go through
this type. Unification refines it.
Another small point is that in ML quantification only occurs at
toplevel. This means that [< `A | `B] itself is not a closed type, and
that you cannot close it easily.  As a result, you cannot compare it
to [`A], other than say they are unifiable. On the other hand, if you
have a function whose type is All('a). ([< `A | `B] as 'a) -> t  (this
is the meaning of "val f : [< `A | `B] -> t") and another function
whose type is [`A] -> t (here there is nothing to quantify), then you
can see that the first one will accept more inputs, and as a result is
more general then the second one.

Not very clear, but this is the rough idea.

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners