Re: [Caml-list] Re: OCaml typechecking bug? (PR#3104) [about phantom types]

[brogoff <brogoff@speakeasy.net>]

On Fri, 27 Aug 2004, Jacques GARRIGUE wrote:
> From: bpr@artisan.com
> Not surprising: the distinction is not between built-in and
> user-defined, but between abbreviation types and datatypes (which
> share the same syntax in ocaml, but have different syntax in most
> other dialects)

OK, I almost understand. I thought that you absolutely needed type abstraction
for phantom types to work, and I was surprised that the examples with data
types "worked" in the sense that illegal use was detected.

> > #   module type PHANTOM_INT' = sig
> >   type 'p t =  Int of int
> [...]
> >   val add_even_even : even t -> even t -> even t
> > end;;
> > # PhantomInt'.add_even_even two' three';;
> > This expression has type PhantomInt'.odd PhantomInt'.t
> > but is here used with type PhantomInt'.even PhantomInt'.t
>
> Actually this one is not much better.
> You indeed get an error if you try to unify [even t] with [odd t],
> but you still can cheat by building a value by hand (eg (Int 1 : even
> t) is perfectly legal), or by using subtyping ((two' :> odd t) shall
> work).

What I still don't understand is why we get the type "error" in this case,
where I used a datatype. What am I missing?

> A real phantom type must be abstract, and nothing else will.
> That is, in your signature, you must have:
>   module type PHANTOM_INT = sig
>     type 'p t
>     ...
>   end

That's what I originally thought, but the behavior in the case above threw me.

-- Brian

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