On 2012/02/13, at 2:36, Gabriel Scherer wrote:
> Thank you, Jacques and Jeremy, for the examples. Indeed that looks quite
> subtle.
>
> I found it helpful to write an informal proof of covariance of the
> following type:
>
> type +_ expr =
> | Val : 'a -> 'a expr
> | Prod : 'a expr * 'b expr -> ('a * 'b) expr
>
> Or, in a more explicit formulation using imaginary syntax with
> explicit existential variables and equalities.
>
> type +'a expr =
> | Val of 'b . 'b with ('a = 'b)
> | Prod of 'b 'c. 'b expr * 'c expr with ('a = 'b * 'c)
>
> The informal proof goes as follow: assuming α ≤ α', we wish to show
> that α expr ≤ β expr. For a given (t : α expr):
> - if (t) is (Val (v : α)), then by α ≤ α' we have (v : α') so (Val v
> : α' expr)
> - if (t) is Prod((t1 : β expr), (t2 : γ expr)), with (α = β * γ), then
> we have (β * γ ≤ α'). *By inversion* we know that there must exist
> β', γ' with
> α' = β' * γ', β ≤ β' and γ ≤ γ'. We therefore have (t1 : β' expr),
> (t2 : γ' expr),
> and therefore (Prod(t1,t2) : α' expr)
>
> The core of the proof is an inversion lemma for subtyping at product types:
> if β*γ ≤ α' then α' is of the form β'*γ' with β≤β', γ≤γ'
>
> The strength of the inversion lemma depends a lot on the details of
> the theory. For example, if α = int and α ≤ α', do we have α' = int?
> And if α ≥ α'? I believe the answer to the α ≤ α' case is "yes", which
> would make the (type +_ expr = Const : int -> int expr) case correctly
> covariant, but as Jacques showed the answer is no in the contravariant
> case α ≥ α', we have (int ≥≠ private int).
[...]
> I'm going to think a bit more about this. What do you think of the
> "proof" in the Prod case? Is there such an inversion principle for the
> OCaml type theory?
The proof looks fine.
Subtyping in OCaml has not been much studied.
You can find a short draft attempting to specify the current behavior
on my publication page.
Again I wonder whether you are not going to get problems with abstraction.
At first sight, no: if when you define a GADT t, the type u is abstract, then
it will have no supertype in any environment where we use t.
But if you think more carefully, you realize that if in the future we allow
(gadt-)unification between abstract types, everything breaks, since abstract
types may end up having supertypes in a local environment.
So it looks like the only types you can allow for instantiation are concrete
datatypes and well-known types (abstract types defined in the initial
environment
or in the current module).
Jacques Garrigue
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
