Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

OCaml typechecking bug? #3104

Closed
vicuna opened this issue Aug 26, 2004 · 1 comment
Closed

OCaml typechecking bug? #3104

vicuna opened this issue Aug 26, 2004 · 1 comment
Labels

Comments

@vicuna
Copy link

vicuna commented Aug 26, 2004

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

@vicuna vicuna closed this as completed Aug 27, 2004
@vicuna
Copy link
Author

vicuna commented Aug 27, 2004

Comment author: administrator

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

@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant