Creating a map ref

Learning
1

For a while, a project of mine included this code:

type typ_ctx = string -> coq_type

let gamma = ref (fun _ -> Error)

let update_typctx id value =
  gamma := fun x -> if x = id then value else !gamma id

I failed to realize for a very long time that the latest value passed into update_typctx would “overwrite” anything else inside of gamma, I’m assuming because the reference to !gamma is only computed when the function is called, so it would just call back to the “top-level” map instead of recursively looking deeper into the map until it hits the original fun _ -> Error. For example:

# type coq_type = Error | Z | String | Unit | Record | Bool | Vector of coq_type
  ;;
type coq_type =
    Error
  | Z
  | String
  | Unit
  | Record
  | Bool
  | Vector of coq_type
# let gamma = ref (fun _ -> Error)
  ;; 
val gamma : ('_weak1 -> coq_type) ref = {contents = <fun>}
# !gamma "id";;
- : coq_type = Error
# let update id value = gamma := fun x -> if x = id then value else !gamma id;;
val update : string -> coq_type -> unit = <fun>
# update "array" (Vector Bool);;
- : unit = ()
# !gamma "array";;
- : coq_type = Vector Bool
# !gamma "id";;
- : coq_type = Vector Bool (* This should still be Error! *)

Is it at all possible to create a reference to a map like this? I’ve made the mistake of building much of my project’s structure around not needing to pass around a gamma and it would be a big hassle to reconfigure everything.

2

There are two issues with your code:

  1. A first issue that you noticed: the !gamma under the fun refers to the “updated” gamma instead of the “previous” gamma. However, this bug alone would mean that the call !gamma "id" after !gamma "array" would loop infinitely.

  2. A second issue, in the definition of update: it should be !gamma x instead of !gamma id.

Anyway, both issues can be solved easily by evaluating !gamma earlier, and changing id to x:

let update id value =
  let prev = !gamma in
  gamma := fun x -> if x = id then value else prev x

But it would be clearer to simply use a different data structure instead of a closure, eg a list:

let gamma = ref []
let update x v = gamma := (x, v) :: !gamma
let lookup x = match List.assoc_opt x !gamma with None -> Error | Some v -> v

In any case, it is always better to hide implementation details: concretely, it would be better to hide the fact that !gamma is a reference and instead define a lookup : string -> coq_type function and use that. That will simplify refactorinig your code if you decide to change the implementation of your maps.

Cheers,
Nicolas

3

A point that should be mentioned is that creating a map ref can be done with

module String_map = Map.Make(String)
let gamma = ref String_map.empty

which will be simpler and more efficient.