Respect the identity of variables

[ttuegel]

In Kore.Syntax.Variable, we have this definition of a variable:

data Variable = Variable
    { variableName :: !Id
    , variableCounter :: !(Maybe (Sup Natural))
    , variableSort :: !Sort
    }

Eq and Ord are defined as if this is a value type (in domain-driven design terminology). In fact, if the variableName and variableCounter of two variables are the same, they are regarded as the same variable; then if their variableSort differs, they are not different, but inconsistent. That is, Variable should be an entity type (domain-driven design terminology again) whose unique identifier is the combination of variableName and variableCounter.

If we move variableSort out of Variable, then FreshPartialOrd (introduced in #1539) becomes a simple upper semilattice. Alternatively, we might combine variableName and variableCounter into a VariableName type, and define an upper semilattice on this type only (instead of a class) and provide optics for renaming other variable types.

[ttuegel]

@traiansf After our conversation, I reflected on this more, and I would like to offer an alternative proposal. First, let me make some remarks, and let us ensure we are in agreement.

For any occurrence of a variable x:A, we might reasonably say that x is the "name" of the variable. Set variables and element variables have different names: a variable named x is certainly an element variable, and a variable named @x is certainly a set variable.

It is inconsistent for the same variable name to occur with two different sorts, but only in the same scope. For example,

σ(x:A, x:B)  // inconsistent
σ(x:A, \exists(x:B, f(x:B)))  // consistent

The "identity" of a variable is also a little tricky to pin down. In the inconsistent example above, it doesn't even make sense to ask if x:A and x:B are the same variable. In the consistent example, they are different variables: they have different scope. So, having the same name is not sufficient to call two variables the same. Is it even necessary? Arguably, no; consider these patterns:

\exists(x:A, φ(x:A))
\exists(y:A, φ(y:A))

One could reasonably argue that x:A and y:A are the "same" variable in these patterns because the patterns are equivalent up to renaming.

The last example convinced me that when we rename variables, we are not creating fresh variables, but fresh names. Therefore, I think we should use separate types for variable names and variable occurrences. At present, we have

data Variable =
    Variable
        { variableName :: Id
        , variableCounter :: Counter
        , variableSort :: Sort
        }

(In the actual implementation, variableCounter is not a opaque type, but it's not important for this discussion what exactly it is.)

I propose we should factor out the variableName and variableCounter, which together form a refresh-able name:

-- | A refresh-able variable name.
data FreshName =
    FreshName
        { freshName :: Id
        , freshCounter :: Counter
        }

-- | An occurrence of a variable.
data Variable name =
    Variable
        { variableName :: name
        , variableSort :: Sort
        }

-- These types also change because they represent occurrences, not merely names.
-- They are type-safe wrappers reflecting that element and set variables have distinct names.
newtype ElementVariable name = ElementVariable { getElementVariable :: Variable name }
newtype SetVariable name = SetVariable { getSetVariable :: Variable name }

The rationale for this is that, at present, refreshVariable must consider the Sort of the variables involved. This includes attaching the correct sort to the fresh name, but it's also important for sorting the Set of variables given to refreshVariable. We have had bugs in this code before. It's extremely subtle; almost too subtle for me. I think that subtlety is a reflection of the fact that the code blurs the domain model's distinction between "variables" and "variable names".

[traiansf]

@ttuegel I believe you are right. One way to make the domain distinction between the two concepts clearer (at least, in my view), is to imagine that we might at some point in the future switch to using DeBruijn indices; then, variableName would perhaps be a variableId, and be a number, but the sort would still be required.

Now, about the naming, I would still use Variable (or, if you want, VariableName) instead of FreshName and (SortedVariable instead of Variable). I'm thinking that being sorted is a constraint on a variable, similar to that of being Element or Set; and, indeed, if we switch to Applicative ML, that constraint might become a semantical one, instead of syntactic, as it is now.

[ttuegel]

Now, about the naming, I would still use Variable (or, if you want, VariableName) instead of FreshName and (SortedVariable instead of Variable). I'm thinking that being sorted is a constraint on a variable, similar to that of being Element or Set; and, indeed, if we switch to Applicative ML, that constraint might become a semantical one, instead of syntactic, as it is now.

Perhaps VariableName for variable names without counters (in the parser) and FreshVariableName (or InternalVariableName) for variable names with counters (during execution)? It would be nice to distinguish them at the type level when we are unparsing: we have to do this funny little "dance" about updating all the counters so that the unparsed names are unique, and that is easier to understand if everything is typed that way.

👍 on SortedVariable instead of Variable; also because the class with that name would go away.