[Caml-list] phantom types and identity function

[Caml-list] phantom types and identity function

[Ivan Gotovchits]

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.

I'll be genuinelly happy, if somebody clarify this issue for me :) My
guess is that the problem lies in the field of higher order polymorpism,
and instead the identity function with signature 'a -> 'a, a more
polymorphic function 'a -> 'b should be used. Though this contradicts
with the fact that the identity function works fine in the first
example and brings up another problem, which is how to obtain such
polymorphic function...

Thanks in advance!

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

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

[Jacques Garrigue]

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

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

[Gabriel Scherer]

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

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

[Ivan Gotovchits]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
>   type u = {x:int}
>   type 'a t = u constraint 'a = [< `A | `B]

Thanks Jacques,
this workaround works fine! By the way, I've found another workaround,
which dirty of course, but interesting:

      let f x = {x=x.x}

works too.

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

[Ivan Gotovchits]

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?"...

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

[Gabriel Scherer]

On Wed, Nov 28, 2012 at 4:42 AM, Ivan Gotovchits <ivg@ieee.org> wrote:
> And now I'm confused much more =). Please, could you explain the
> relevance between subtyping and type restriction?

I was reacting mostly to Jacques' remark that "you cannot even use
subtyping for that".

The relation between subtyping and "constraint" is as explained in the
manual excerpt I quoted. The following is valid:
  type 'a t = {x : 'a} ;;
  let f x = (x : [ `A ] t :> [ `A | `B ] t);;

but the following is not:
  type 'a t = {x : 'a} constraint 'a = [< `A | `B ];;
  let f x = (x : [ `A ] t :> [ `A | `B ] t);;
    Error: Type [ `A ] t is not a subtype of [ `A | `B ] t
    The first variant type does not allow tag(s) `B

The reason for this behavior is that in the first case, t was inferred
covariant, while the presence of a constraint disables variance
inference (in the manual: "otherwise (ie. [...] for non-free
parameters) the variance must be given explicitly)"). You can make the
constrained version work with an explicit variance annotation:
  type +'a t = {x : 'a} constraint 'a = [< `A | `B ];;
  let f x = (x : [ `A ] t :> [ `A | `B ] t);;

Finally, while in this example 'a occurs positively in ('a t), in your
example 'a did not occur at all. In this case it is correct to coerce
from (foo t) to (bar t), whatever the type expression (foo) and (bar)
are -- they don't need to be in a subtyping relation. The following
works:
 type 'a t = { x : int };;
 let f x = (x : [ `A ] t :> [ `B ] t);;

I'm calling this form of variance "irrelevant" to highlight that the
parameter can simply be ignored when checking for subtyping (some
people call it "nonvariant", but it's kind of awkward if you already
use "invariant" for the opposite notion of appearing both in positive
and negative position).
The OCaml type checker can use some restricted form of it (eg. the
previous example), but you cannot abstract over it: there is no
variance annotation to express that.

Jacques' workaround replaces the definition of a new constrained type
with a constrained type synonym, that is not checked using variance
but direct expansion. But that works because you know what the
definition  expands to. In general there may be situation when you
want to say "type 'a t, where 'a is not used" but not expose a
(potentially abstract) non-parametrized type u such that "type 'a t =
u".


While we're at it: are you sure you need to play with phantom
polymorphic variant types now that we have GADTs? I have used phantom
types in the past, but my personal use cases would be profitably
rewritten using GADTs. They tend to produce hairy error messages, but
phantom polymorphic variants are not better in this regard.

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

[Ivan Gotovchits]

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

> The reason for this behavior is that in the first case, t was inferred
> covariant, while the presence of a constraint disables variance
> inference (in the manual: "otherwise (ie. [...] for non-free
> parameters) the variance must be given explicitly)"). You can make the
> constrained version work with an explicit variance annotation:
>   type +'a t = {x : 'a} constraint 'a = [< `A | `B ];;
>   let f x = (x : [ `A ] t :> [ `A | `B ] t);;

Well, now I understand this. Thanks!

> While we're at it: are you sure you need to play with phantom
> polymorphic variant types now that we have GADTs? I have used phantom
> types in the past, but my personal use cases would be profitably
> rewritten using GADTs. They tend to produce hairy error messages, but
> phantom polymorphic variants are not better in this regard.

I wish I could, but I'm bond to Ocaml 3.11 =(

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