Re: [Caml-list] [Q]: Co(ntra)variance and subtyping?

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Pixel <pixel@mandrakesoft.com>

> > While subtyping for module types is rather standard from a
> > superficial point of view, OCaml's treatment of subtyping in the
> > core language is somewhat special because it does not provide
> > so-called subsumption.
> 
> well, you forgot polymorphic variants, which do use subsumption:
> 
> # let switch = function `On -> `Off | x -> x;;
> val switch : ([> `Off | `On] as 'a) -> 'a = <fun>
> # (switch `On, switch `Whatever);;
> - : _[> `Off | `On] * _[> `Off | `On | `Whatever] = `Off, `Whatever

This, again, is row polymorphism, not subsumption.
The difference between (row/parametric) polymorphism and subsumption
is that for the former you must explicitely leave some free variable
in the type (the presence of which is proved by the "as 'a" or "_"),
while the latter also works on ground types (without variables).
Both polymorphic variants and objects uss both polymorphism and
subtyping, but without implicit subsumption.

> > Subsumption means that wherever a value of type t is expected you
> > may freely provide a value of some subtype t'. This is not the
> > case in OCaml: you have to explicitly coerce the value to the
> > required supertype first.  This is necessary to make type
> > inference feasible.
> 
> necessary is a small overstatement ;p

No, feasible should be defined more precisely :-)
In the ML world, we mean complete type inference. For this explicit
coercions are indeed necessary. If you're satisfied with partial
inference, then you may find disciplines where some coercions can be
inferred.

Cheers,

Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr