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

• does not use subtyping anywhere
• and also, the end is strange,

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 === with type 'a ref -> 'b ref -> ('a, 'b) eq ?

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,
and you can recover the type of the reference using ===.

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

The point is that === allows to some of the thing do what you can do with a representation of type, without ...

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

• only used internaly
• === is enough
• and a parser in general may handle quite a few types
• and our earley parser is not a functor, and this would require to make it a functor to pass a type (or maybe use extensible variant ?)

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
1° you have a data structure typically a record of type td
2° you frequently map td to various types (not always the same)
3° you would like to store this binding in td directly.

(===) 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
use an option type which is in fact always None to keep the type constraint.
There probably is a better was. This code is easy to modify to use ===
only on ref.

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
all useless cost. This is not yet the case here ... as I can not find a way to eliminate the type ('a,'b) abstract ...

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.