Dynamic binding using a ref cell

Nick Zalutskiy

I understand that you can't do this, but want to understand precisely why.

module M : sig 
  type 'a t
  val call : 'a t -> 'a option
end = struct 
  type 'a t
  let state : ('a t -> 'a option) ref = ref (fun _ -> None)
  let call : ('a t -> 'a option) = fun x -> !state x
end

Results in:

Error: Signature mismatch:
Modules do not match:
    sig 
        type 'a t
        val state : ('_a t -> '_a option) ref
        val call : '_a t -> '_a option
    end
is not included in
    sig 
        type 'a t 
        val call : 'a t -> 'a option 
    end

    Values do not match:
        val call : '_a t -> '_a option
    is not included in
        val call : 'a t -> 'a option

Why are the abstract types not compatible here?

My gut tells me it has everything to do with early vs late binding, but I'm looking for an exact description of what the type system is doing here.

Jeffrey Scofield

One way to look at it is that your field state can't have the polymorphic value you ascribe to it, because mutable values can't be polymorphic. References are at most monomorphic (as indicated by the '_a notation for the type variable).

If you just try to declare a similar reference in the toplevel, you'll see the same effect:

# let lfr: ('a list -> 'a option) ref = ref (fun x -> None);;
val lfr : ('_a list -> '_a option) ref = {contents = <fun>}

The type variable '_a indicates some single type that hasn't yet been determined.

The reason that references can't be polymorphic is that it's unsound. If you allow references to be generalized (polymorphic) it's easy to produce programs that go horribly wrong. (In practice this usually means a crash and core dump.)

The issue of soundness is discussed near the beginning of this paper: Jacques Garrigue, Relaxing the Value Restriction (which I refer to periodically when I forget how things work).

Update

What I think you want is "rank 2 polymorphism". I.e., you want a field whose type is polymorphic. You can actually get this in OCaml as long as you declare the type. The usual method is to use a record type:

# type lfrec = { mutable f: 'a. 'a list -> 'a option };;
type lfrec = { mutable f : 'a. 'a list -> 'a option; }
# let x = { f = fun x -> None };;
val x : lfrec = {f = <fun>}
# x.f ;;
- : 'a list -> 'a option = <fun>

The following code compiles for me using lfrec instead of a reference:

module M : sig
  type 'a t
  val call : 'a t -> 'a option
end = struct
  type 'a t
  type lfrec = { mutable f: 'a. 'a t -> 'a option }
  let state: lfrec = { f = fun _ -> None }
  let call : ('a t -> 'a option) = fun x -> state.f x
end

Collected from the Internet

Please contact [email protected] to delete if infringement.

edited at
0

Comments

0 comments
Login to comment

Related