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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

I have been a bit confused by this discussion, and found the relevant
part of the manual that may enlighten other list readers:

The OCaml Language, Type and exception definitions
  http://caml.inria.fr/pub/docs/manual-ocaml/manual016.html#toc54

  "If the type has either a representation or an equation, and the
  parameter is free (i.e. not bound via a type constraint to
  a constructed type), its variance constraint is checked but
  subtyping etc. will use the inferred variance of the parameter,
  which may be better; otherwise (i.e. for abstract types or
  non-free parameters), the variance must be given explicitly, and the
  parameter is invariant if no variance was given."


Note that this would not be needed if we had an explicit way to
express the variance of invariant (the variable appears in both
positive and negative positions) and irrelevant (the variable doesn't
appear except in irrelevant positions) explicitly. We could then
write, say:

  type 0'a t = {x : int} constraint 'a = [< `A | `B ]

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.

On Tue, Nov 27, 2012 at 3:08 PM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
>
> On 2012/11/27, at 20:00, Ivan Gotovchits <ivg@ieee.org> wrote:
>
> >
> > Hello,
> >
> > These simple signature
> >
> >   module type T = sig
> >       type 'a t constraint 'a = [< `A | `B ]
> >       val init: [`A] t
> >       val f: [`A] t -> [`B] t
> >   end
> >
> > can be used to constrain the following module
> >
> >   module T : T = struct
> >       type 'a t = unit constraint 'a = [< `A | `B]
> >       let init = ()
> >       let f x = x
> >   end
> >
> > where identity function successfully satisfies the constraint
> >
> >   [`A] t -> [`B] t
> >
> > but in the following module
> >
> >   module T : T = struct
> >       type 'a t = {x:int} constraint 'a = [< `A | `B]
> >       let init = {x=0}
> >       let f x = x
> >   end
> >
> > the same identity function doesn't satisfy.
>
> In the first case, a type abbreviation is used.
> Since ('a t) expands to (unit), the parameter is completely
> ignored, so that you can replace it by anything.
>
> In the second case, you define a concrete type,
> so that the parameter is not forgotten.
> Note that you cannot even use subtyping for that:
>   let f x = (x : [`A] t :> [`B] t)
> fails too.
> But there is an easy workaround, defining in two steps:
>   type u = {x:int}
>   type 'a t = u constraint 'a = [< `A | `B]
>
> Jacques Garrigue
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs