This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] inference and phantom types
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Jacques Garrigue Subject: Re: [Caml-list] inference and phantom types
```From: Julien Cohen <jcohen@lami.univ-evry.fr>

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

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

```