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
Heterogeneous physical equality for references (was: Type soundness with GADT and heterogeneous physical equality) #7425
Comments
Comment author: @yallop The === function is not at all type safe. There are lots of ways that the same object can have different types, so deducing type equality from physical equality is not sound. Here's a shorter example: let x = object method m = 0 end
let (wrong : (< >, < m: int >) eq) = (x :> < >) === x
let coerce : type a b. (a, b) eq -> a -> b = fun Eq x -> x
let _ = (coerce wrong (object end))#m |
Comment author: Christophe Raffalli The given exemple
add : 'a table -> 'container -> 'a -> unit and two calls to add are accepted with disting 'a on the same table. |
Comment author: @yallop Subtyping's just one way that things can go wrong. Here's another: let id x = x
let (wrong : (int -> int, string -> string) eq) = id === id
let coerce : type a b. (a -> a, b -> b) eq -> a -> b = fun Eq x -> x
let _ = "abc" ^ coerce wrong 1 |
Comment author: @gasche Ah, my own example was a tad longer: let cast : type a b . (a, b) eq -> a -> b option =
function
| Eq -> (fun x -> Some x)
| Neq -> (fun _ -> None)
type 'a box = 'a option * unit
let any : type a . a box = (None, ())
let magic_cast (type a b) : a -> b = fun x ->
let wrong = (any : a box) === (any : b box) in
match cast wrong (Some x, ()) with
| None | Some (None, ()) -> assert false
| Some (Some v, ()) -> v |
Comment author: @yallop Here's a shorter one: let coerce (type a b c d) (Eq : (a -> c, b -> d) eq) (x: a) = (x : b)
let f = coerce ((===) (===) (===)) (===) (===) (===) (===) (===) |
Comment author: Christophe Raffalli Ok ... But still, the last two lines on my examples feel problematic to me: let _ = add t2 c1 (fun x -> x)
let _ = add t2 c2 2 with let add : type a. a table -> container -> a -> unit = ... |
Comment author: Christophe Raffalli and t2 is not a value hence monomorphic |
Comment author: @gasche In your example both t1 and t2 are polymorphic because of the relaxed value restriction: the type variable of ('a table) is in covariant position. |
Comment author: Christophe Raffalli It might be safe to use |
Comment author: @gasche I cannot see a problem with that definition. I am not sure what your use-case is, have you considered writing safe code (without externals) to achieve the same results? For example, if you had a runtime representation of types ('a ty) as a GADT, you could safely write type (_, _) eq = Refl : ('a, 'a) eq
val try_eq : 'a ty -> 'b ty -> ('a, 'b) eq option (but that require passing type witnesses along with your values) |
Comment author: Christophe Raffalli The point is that === allows to some of the thing do what you can do with a representation of type, without ... For instance, you can have a record holding a reference on an existential type, Do you have a formal argument proving such an === to be safe ? If yes, would it be a reasonable thing to add to the standard library ? |
Comment author: Christophe Raffalli For a nice use case, look at the attached code ... |
Comment author: @gasche
Some type representations are very light. In particular you can use open/extensible variants to create "universal type" of tags using generativity. (I was unable to find a good reference to that right now, though). Then the type ('a tag * 'a) is not substantially heavier than your ('a ref) proposal. |
Comment author: Christophe Raffalli The point is that in our case, the type 'a is unknown from the library we are defining (we are writing an earley parser and 'a is the type returned by the action of a grammar rule). I do not want my earley parser to ask for a description of the type being parsed, especially because this description is
|
Comment author: @yallop As gasche suggests, it's possible to define exactly your === operator for references in pure OCaml without unsafe extensions. Here's an implementation of the ref interface extended with such an operation: type (_,_) eql = Refl : ('a, 'a) eql
module Ref : sig
type _ t
val ref : 'a -> 'a t
val (:=) : 'a t -> 'a -> unit
val (!) : 'a t -> 'a
val (===) : 'a t -> 'b t -> ('a, 'b) eql option
end =
struct
type _ tag = ..
type 'a t = {
id: 'a tag;
eq: 'b. 'b t -> ('a, 'b) eql option;
mutable contents: 'a;
}
let (===) {eq} = eq
let (!) {contents} = contents
let (:=) r v = r.contents <- v
let ref (type a) contents =
let module M = struct type _ tag += T : a tag end in
let eq : type b. b t -> (a, b) eql option =
function {id=M.T} -> Some Refl | _ -> None in
{ id = M.T; eq; contents }
end |
Comment author: Christophe Raffalli Nice piece of code ... This proves (===) sound, isn't it ? Then, I had rather have (===) predefined and referring to the standard references. Indeed, the use case I have is (===) makes it possible with an access time in O(N) where N is the number of tables simultaneously in use (and not the size of the tables) See my attached code ... which is not as clean as possible, we add to |
Comment author: Christophe Raffalli Yes (answer to gashe) you may rename this thread and classify it as a feature wish. |
Comment author: @gasche I used imperative update to clarify what this ticket had "become" -- smalltalk pun intended. |
Comment author: Christophe Raffalli I uploaded a cleaner use case ... But the basic Idea is to avoid Any idea ? |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 7425
Reporter: Christophe Raffalli
Assigned to: @gasche
Status: acknowledged (set by @gasche on 2016-12-06T22:31:38Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.04.0
Category: typing
Has duplicate: #7428
Bug description
I would like the following (or equivalent) to be added somewhere
in the stdlib. This sound type safe and sometimes very useful,
by avoiding a runtime representation of the type.
Additional information
In its initial version, the present issue proposed a more permissive interface for (===), namely ('a -> 'b -> ('a, 'b) eq) instead of ('a ref -> 'b ref -> ('a, 'b) eq), which was shown unsound in the first few messages below. The initial discussion was as follows:
Consider the following heterogeneous physical equality,
limited to blocks, which should be type safe:
Then, the attached code breaks the type soundness of OCaml.
Remark, the given module seems sound if used in a separate module
with abstract type in its signature.
File attachments
The text was updated successfully, but these errors were encountered: