Re: [Caml-list] phantom types and identity function

[Ivan Gotovchits <ivg@ieee.org>]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> The absence of such a variance marker means that some OCaml code is
> hard to abstract through a module boundary: in presence of the
> explicit definition, the type-checker will accept to subtype between
> any instances of the type (by simple expansion), but if you abstract
> over its definition you cannot express this property anymore. Your
> workaround corresponds to statically expressing this irrelevance
> through an exported equation, but there are (arguably somewhat
> unnatural) scenarios where this isn't convenient.

And now I'm confused much more =). Please, could you explain the
relevance between subtyping and type restriction?

When I try to restrict type [t -> t'] by the some type [r -> r'] does
the compiler checks that [r -> r'] is a subtype of [t -> t']? And even
if it does, in my example 
   [`A] t -> [`B] t

[[`A]] is clearly not a subtype of [[`B]] (and vice versa). So I do not
see how an explicit variance specification can help.


-- 
         (__) 
         (oo) 
   /------\/ 
  / |    ||   
 *  /\---/\ 
    ~~   ~~   
...."Have you mooed today?"...