A variable is a triple of a unique identifier (varID), a hint for how to display things to humans (varHint), and a type (varType). Notably, the hint is only used for display purposes, and the type is only used for typing purposes; thus, the Eq and Ord instances only look at the unique identifier, completely ignoring the other two components. However, the varEq function does take the type into consideration (but still ignores the hint).

N.B., the unique identifier is lazy so that we can tie-the-knot in binder.

Compare to variables at possibly-different types. If the variables are "equal", then they must in fact have the same type. N.B., it is not entirely specified what this function means when two variables have the same varID but different varType. However, so long as we use this function everywhere, at least we'll be consistent.

Possible interpretations:

• We could assume that when the varTypes do not match the variables are not equal. Upside: we can statically guarantee that every variable is "well-typed" (by fiat). Downside: every type has its own variable namespace, which is very confusing. Also, the Ord SomeVariable instance will be really difficult to get right.
• We could require that whenever two varIDs match, their varTypes must also match. Upside: a single variable namespace. Downside: if the types do not in fact match (e.g., the preprocessing step for ensuring variable uniqueness is buggy), then we must throw (or return) an VarEqTypeError exception.
• We could assert that whenever two varIDs match, their varTypes must also match. Upsides: we get a single variable namespace, and we get O(1) equality checking. Downsides: if the types do not in fact match, we'll probably segfault.

Whichever interpretation we choose, we must make sure that typing contexts, binding environments, and so on all behave consistently.

An exception type for if we need to throw an error when two variables do not have an equal varType. This is mainly used when varEq chooses the second interpretation.

Convenient synonym to refer to the kind of a type variable: type KindOf (a :: k) = ('KProxy :: KProxy k)

Hide an existentially quantified parameter to Variable.

Because the Variable type is poly-kinded, we need to be careful not to erase too much type/kind information. Thus, we parameterize the SomeVariable type by the kind of the type we existentially quantify over. This is necessary for giving Eq and Ord instances since we can only compare variables whose types live in the same kind.

N.B., the Ord instance assumes that varEq uses either the second or third interpretation. If varEq uses the first interpretation then, the Eq instance (which uses varEq) will be inconsistent with the Ord instance!

A set of (typed) variables.

Convert a list of variables into a variable set.

In the event that multiple variables have conflicting varID, the latter variable will be kept. This generally won't matter because we're treating the list as a set. In the cases where it would matter, chances are you're going to encounter a VarEqTypeError sooner or later anyways.

Convert a list of variables into a variable set.

In the event that multiple variables have conflicting varID, the latter variable will be kept. This generally won't matter because we're treating the list as a set. In the cases where it would matter, chances are you're going to encounter a VarEqTypeError sooner or later anyways.

Return the successor of the largest varID of all the variables in the set. Thus, we return zero for the empty set and non-zero for non-empty sets.

A pair of variable and term, both of the same Hakaru type.

A set of variable/term associations.

N.B., the current implementation assumes varEq uses either the second or third interpretations; that is, it is impossible to have a single varID be shared by multiple variables (i.e., at different types). If you really want the first interpretation, then the implementation must be updated.

The empty set of associations.

A single association.

Convert an association list into a list of associations.

Convert a list of associations into an association list. In the event of conflict, later associations override earlier ones.

Convert an unzipped list of curried associations into an association list. In the event of conflict, later associations override earlier ones.

Add an association to the set of associations.

HACK: if the variable is already associated with some term then we throw an error! In the future it'd be better to take some sort of continuation to decide between (a) replacing the old binding, (b) throwing an exception, or (c) safely wrapping the result up with Maybe

Look up a variable and return the associated term.

N.B., this function is robust to all interpretations of varEq.

Adjust an association so existing variable refers to different value. Does nothing if variable not present.