Browse thread
[Caml-list] Re: OCaml typechecking bug? (PR#3104) [about phantom types]
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Jacques GARRIGUE <garrigue@k...> |
| Subject: | [Caml-list] Re: OCaml typechecking bug? (PR#3104) [about phantom types] |
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