You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 3104 Reporter: administrator Status: closed Resolution: not a bug Priority: normal Severity: minor Category: ~DO NOT USE (was: OCaml general)
Bug description
Full_Name: Brian Rogoff
Version: 3.08.1
OS: Linux
Submission from: 192-149-105-50.artisan.com (192.149.105.50)
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'
bpr@boreal[bpr]$ ocaml
Objective Caml version 3.08.1
module type PHANTOM_INT = sig
type 'p t = int
type even
type odd
val add : 'p t -> 'p t -> 'p t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end;;
module type PHANTOM_INT =
sig
type 'a t = int
type even
type odd
val add : 'a t -> 'a t -> 'a t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end
module PhantomInt : PHANTOM_INT = struct
type 'p t = int
type even = ()
type odd = ()
let add = ( + )
let add_even_even = add
let add_even_odd = add
let add_odd_even = add
let add_odd_odd = add
let make_even n = if n mod 2 = 0 then n else failwith "not even"
let make_odd n = if n mod 2 <> 0 then n else failwith "not odd"
end;;
module PhantomInt : PHANTOM_INT
let two = PhantomInt.make_even 2;;
val two : PhantomInt.even PhantomInt.t = 2
let three = PhantomInt.make_odd 3;;
PhantomInt.add_even_even two three;;
val three : PhantomInt.odd PhantomInt.t = 3
- : PhantomInt.even PhantomInt.t = 5
module type PHANTOM_INT' = sig
type 'p t = Int of int
type even
type odd
val add : 'p t -> 'p t -> 'p t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end;;
module type PHANTOM_INT' =
sig
type 'a t = Int of int
type even
type odd
val add : 'a t -> 'a t -> 'a t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end
module PhantomInt' : PHANTOM_INT' = struct
type 'p t = Int of int
type even = ()
type odd = ()
let add (Int x) (Int y) = Int(x + y)
let add_even_even = add
let add_even_odd = add
let add_odd_even = add
let add_odd_odd = add
let make_even n = if n mod 2 = 0 then Int n else failwith "not even"
let make_odd n = if n mod 2 <> 0 then Int n else failwith "not odd"
end;;
module PhantomInt' : PHANTOM_INT'
let two' = PhantomInt'.make_even 2;;
val two' : PhantomInt'.even PhantomInt'.t = PhantomInt'.Int 2
let three' = PhantomInt'.make_odd 3;;
val three' : PhantomInt'.odd PhantomInt'.t = PhantomInt'.Int 3
PhantomInt'.add_even_even two' three';;
This expression has type PhantomInt'.odd PhantomInt'.t
but is here used with type PhantomInt'.even PhantomInt'.t
-- Brian
The text was updated successfully, but these errors were encountered:
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
Original bug ID: 3104
Reporter: administrator
Status: closed
Resolution: not a bug
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)
Bug description
Full_Name: Brian Rogoff
Version: 3.08.1
OS: Linux
Submission from: 192-149-105-50.artisan.com (192.149.105.50)
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'
bpr@boreal[bpr]$ ocaml
Objective Caml version 3.08.1
module type PHANTOM_INT = sig
type 'p t = int
type even
type odd
val add : 'p t -> 'p t -> 'p t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end;;
sig
type 'a t = int
type even
type odd
val add : 'a t -> 'a t -> 'a t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end
module PhantomInt : PHANTOM_INT = struct
type 'p t = int
type even = ()
type odd = ()
let add = ( + )
let add_even_even = add
let add_even_odd = add
let add_odd_even = add
let add_odd_odd = add
let make_even n = if n mod 2 = 0 then n else failwith "not even"
let make_odd n = if n mod 2 <> 0 then n else failwith "not odd"
end;;
module PhantomInt : PHANTOM_INT
let two = PhantomInt.make_even 2;;
val two : PhantomInt.even PhantomInt.t = 2
let three = PhantomInt.make_odd 3;;
PhantomInt.add_even_even two three;;
val three : PhantomInt.odd PhantomInt.t = 3
- : PhantomInt.even PhantomInt.t = 5
module type PHANTOM_INT' = sig
type 'p t = Int of int
type even
type odd
val add : 'p t -> 'p t -> 'p t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end;;
module type PHANTOM_INT' =
sig
type 'a t = Int of int
type even
type odd
val add : 'a t -> 'a t -> 'a t
val add_even_even : even t -> even t -> even t
val add_even_odd : even t -> odd t -> odd t
val add_odd_even : odd t -> even t -> odd t
val add_odd_odd : odd t -> odd t -> even t
val make_even : int -> even t
val make_odd : int -> odd t
end
module PhantomInt' : PHANTOM_INT' = struct
type 'p t = Int of int
type even = ()
type odd = ()
let add (Int x) (Int y) = Int(x + y)
let add_even_even = add
let add_even_odd = add
let add_odd_even = add
let add_odd_odd = add
let make_even n = if n mod 2 = 0 then Int n else failwith "not even"
let make_odd n = if n mod 2 <> 0 then Int n else failwith "not odd"
end;;
module PhantomInt' : PHANTOM_INT'
let two' = PhantomInt'.make_even 2;;
val two' : PhantomInt'.even PhantomInt'.t = PhantomInt'.Int 2
let three' = PhantomInt'.make_odd 3;;
val three' : PhantomInt'.odd PhantomInt'.t = PhantomInt'.Int 3
PhantomInt'.add_even_even two' three';;
This expression has type PhantomInt'.odd PhantomInt'.t
but is here used with type PhantomInt'.even PhantomInt'.t
-- Brian
The text was updated successfully, but these errors were encountered: