Browse thread
Recursive subtyping issue
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-02-27 (16:53) |
From: | Andreas Rossberg <rossberg@m...> |
Subject: | Re: [Caml-list] Recursive subtyping issue |
On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote: >> # type q = private w and w = private q;; >> type q = private w >> and w = private q >> # let f (x : q) = (x : q :> w);; >> val f : q -> w = <fun> >> # let f (x : q) = (x : w);; >> Error: This expression has type q but an expression was expected of >> type w >> # Interesting, but these are vacuous type definitions. In fact, I would call it a bug that the compiler does not reject them (it does when you remove at least one of the "private"s). In any case, I don't quite understand how this pathological behaviour is supposed to help, because the types are uninhabited anyway. > I've been looking all over at this issue, but simply cannot find a > way out. While experimenting on this, I've stumbled on a number of > quirky issues with the type system. > > First one: http://ocaml.janestreet.com/?q=node/26 That's indeed a slight oversight in the design of the module type system. (FWIW, this is possible in SML.) > Second one: > >> # type 'a q = <m : 'a>;; >> type 'a q = < m : 'a > >> # let f : 'a q -> 'a q = fun x -> x;; >> val f : 'a q -> 'a q = <fun> >> # let o = object method m : 'a. 'a -> 'a = fun x -> x end;; val o : >> < m : 'a. 'a -> 'a > = <obj> >> # f o;; >> Error: This expression has type < m : 'a. 'a -> 'a > >> but an expression was expected of type 'b q >> The universal variable 'a would escape its scope This example would require full impredicative polymorphism, because you would need to instantiate 'a q with a polymorphic type. The ML type system does not support that, because it generally makes type inference undecidable. But see e.g. Le Botlan & Remy's work on ML^F for a more powerful approach than what we have today. /Andreas