A unifier maintains a graph whose vertices are equivalence classes of variables. With each equivalence class, a piece of information of type
data is attached.
type 'a structure = 'a S.structure
'a structure describes the information that is attached with each class. It is parameterized over a type
'a of children. In the definition of the type
'a is instantiated with
data is a synonym for
variable structure. So, the data attached with an equivalence class of variables is a structure whose children are variables.