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

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

[Jacques GARRIGUE]

From: bpr@artisan.com
> Version: 3.08.1
> 
> As mentioned on the mailing list, simple use of phantom types leads to a 
> situation where it appears that built in types and user defined types are
> handled 
> differently. Here's a simple example from the command line. The same behavior is
> 
> observed when I replace int in "type 'p t = int" with int64 and int array, or
> when 
> I change from sum type to record in PHANTOM_INT'  

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)

> bpr@boreal[bpr]$ ocaml
>         Objective Caml version 3.08.1
> 
> # module type PHANTOM_INT = sig
>   type 'p t =  int
[...]
>   val add_even_even : even t -> even t -> even t
> end;;
[...]
> # PhantomInt.add_even_even two three;;
> val three : PhantomInt.odd PhantomInt.t = 3

This behaviour is perfectly normal.
In the above signature, the type t is not phantom at all.
It will be expanded to int before checking equality, so the type
argument will be completely ignored altogether.

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

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

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

[brogoff]

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

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

[brogoff]

On Fri, 27 Aug 2004, Jacques GARRIGUE wrote:
[...snip...]
> 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)
[...snip...]
> This behaviour is perfectly normal.
> In the above signature, the type t is not phantom at all.
> It will be expanded to int before checking equality, so the type
> argument will be completely ignored altogether.

OK, ignore my request for further explanation, it all makes good sense now,
even though it was counterintuitive behavior at first. It does suggest that
making a syntactic distinction between type abbreviation and datatype
definition a la SML is a good idea.

I never ran across this behavior before since I assumed the phantom type had to
be abstract and always coded it that way.

All of this phantom type stuff makes me wish we had dependent types anyways...

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