I am writing a type checker for an ML dialect that involves generating "fresh" (new and unique) "type variables" (values representing unknowns). My strategy, and the strategy that seems to be used in tutorials, is to identify type variables with a unique integer and keep a counter that is incremented whenever a fresh type variable is generated.
Previously, I kept the counter as a mutable field of a record type representing the state of the type checker.
The program needs to compare type variables; it does this by comparing their integer IDs. Because different type checker states keep their own counters, one could potentially compare the type variables generated from two different type checker states and have them be equal. This is API misuse and should not ever happen.
type state =
{ mutable vargen : int
; (* Other fields... *) }
let fresh_tvar st =
st.vargen <- st.vargen + 1;
Type.Var.{ id = st.vargen - 1
; (* Other fields... *) }
let compare lhs rhs = compare lhs.id rhs.id
To better enforce correctness, I decided to move the counter from the type checker state to a global and private member of the type variable module. Now, distinct type variables can never be equal. Code outside the module cannot access the counter or the ID of a type variable; they can only compare two type variables.
module type Var = sig
type t
val fresh : some_type -> some_other_type -> t
val compare : t -> t -> bool
end
module Var : Var = struct
type t = { id : int; (* Other fields... *) }
let counter = ref 0 (* Global mutable state not exposed in signature *)
let fresh some_arg some_other_arg =
counter := !counter + 1;
{ id = counter - 1
; (* Other fields... *) }
let compare lhs rhs = compare lhs.id rhs.id
end
Because global mutable state is considered harmful (especially in functional programming!), I'm not sure if my new code is good.
- Is global mutable state justified in this context?
- If my first design is better, in general, how may I enforce the invariant that values generated by physically separate states not be used together? (Another example of such a violation, in C++, would be comparing iterators to different containers.)
- Is the type checker state itself actually a singleton that behaves like global state in all but name?
I am using OCaml, by the way, if the language's specific idioms affect the answer to my question.