[Caml-list] inference and phantom types

[Caml-list] inference and phantom types

[Julien Cohen]

I read in the thread 
http://caml.inria.fr/archives/200109/msg00097.html
that phantom types could be used in ocaml but I have some 
troubles understanding the way they really work.

In the following session I use a phantom type ('a,'b)t to 
simulate a list with an additionnal type 'b. I create a special 
cons preserving the type. I create an (int,bool)t value and when 
I make a cons on it and the phantom type seems not to be well 
infered:



         Objective Caml version 3.04

# type ('a,'b) t = 'a list;;
type ('a, 'b) t = 'a list

# let f (x:'a) (y:('a,'b) t) = (x::y : ('a,'b) t);;
val f : 'a -> ('a, 'b) t -> ('a, 'b) t = <fun>

# let (v: (int,bool) t) = [1];;
val v : (int, bool) t = [1]

# f 1 v;;
- : (int, '_a) t = [1; 1]


Is there a fundamental reason for the bool type not to be inferred?
(no response in the ocaml-beginner list)

Thanks
Julien Cohen

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] inference and phantom types

[Jacques Garrigue]

From: Julien Cohen <jcohen@lami.univ-evry.fr>

> I read in the thread 
> http://caml.inria.fr/archives/200109/msg00097.html
> that phantom types could be used in ocaml but I have some 
> troubles understanding the way they really work.
> 
> In the following session I use a phantom type ('a,'b)t to 
> simulate a list with an additionnal type 'b. I create a special 
> cons preserving the type. I create an (int,bool)t value and when 
> I make a cons on it and the phantom type seems not to be well 
> infered:
> 
> 
> 
>          Objective Caml version 3.04
> 
> # type ('a,'b) t = 'a list;;
> type ('a, 'b) t = 'a list
> 
> # let f (x:'a) (y:('a,'b) t) = (x::y : ('a,'b) t);;
> val f : 'a -> ('a, 'b) t -> ('a, 'b) t = <fun>
> 
> # let (v: (int,bool) t) = [1];;
> val v : (int, bool) t = [1]
> 
> # f 1 v;;
> - : (int, '_a) t = [1; 1]
> 
> 
> Is there a fundamental reason for the bool type not to be inferred?
> (no response in the ocaml-beginner list)

Not surprising, this is not a beginner question :-)

What happens is just that abbreviation types are expanded before
unification, meaning that you are actually not unifying
('a,'b) t with ('c,'d) t, but only 'a list with 'c list, so that 'b
and 'd will not be unified.

Note that in recent versions of ocaml, defining a datatype (with
constructors) will not help: the typecker infers variance, and will
detect that 'b is unused in the definition, so that again it will just
be discarded during unification (or subtyping).

The real solution is to use an abstract type:
put your type definition in a module with necessary operations,
and provide an interface where the type is abstract.

For instance

module M : sig
  type (+'a,'b) t
  val inj : 'a list -> ('a,'b) t
  val proj : ('a,'b) t -> 'a list
end = struct
  type ('a,'b) t = 'a list
  let inj x = x
  let proj x = x
end

If you really don't want your type to be abstract, you will need to
make the type variable appear somewhere in it with the right variance,
which can be complicated...

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners