5

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.

1 Answer 1

6

Global state is not necessarily evil, even in functional languages. However:

  • all this does is enforce a consistent ID generation per process. Multiple processes could still clash. You have to decide at which point the uniqueness is good enough.

  • global ID generation can make testing more difficult. In contrast, if you can use a fresh ID generation state for each test, the exact IDs might be reproducible.

In nearly all programs there will be a dynamic element that you cannot represent in the type system, here: only IDs generated by the same type checker instance may be compared. It is reasonable to make checks to detect accidental errors, it is not always reasonable to aim for a design where misuse is not possible. I.e.: to err is human, but we can still treat API consumers as adults.

In this case, it might be sensible to combine your two approaches. Do provide encapsulation by using a module, but also support external state to simplify testing. E.g.:

module type Var = sig
  type typevar
  type state
  val newstate : () -> state
  val gensym : state -> some_type -> typevar
  val compare : typevar -> typevar -> bool
end

If reproducible type variable IDs are not necessary, then keeping your solution with encapsulated global state is fine.

Why is encapsulated global state arguably fine? Your ID generation function is clearly not a pure function, since it should return a different result each time. Non-pure function are common, especially in imperative languages like OCaml. This is similar to any function that does I/O, or a function that is a random number generator. But crucially, your ID generation function has a very simple data flow. Its output does not depend on previous function inputs, merely on the number of previous invocations.

Here is a diagram illustrating the data flow. Information flows out of the encapsulated system (shaded background), and states only depend on previous states. This mutable state is easy to reason about.

hidden counter

In contrast, “evil” global variables let data flow in multiple directions through the boundary of the encapsulated system. The state of the “encapsulated” system is shared among any consumers of that system, and the ID Ik depends on unknown inputs: we can get “action at a distance”, and multiple consumers (or simply, different parts of the code base) become more coupled. This data flow is much more difficult to reason about.

global variable

Not all mutable state is equally bad – we should sometimes take a step back and consider whether it really is a problem for our application.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.