Determine if enforcing unique names is required (and implement it) or not about shine HOT 4 OPEN

I think that whichever way we go (names, indices, or pointers), we should go towards only using strings for debugging purposes and using integers for identification purposes, since that would speep up the compiler (a bit like string interning but without using strings in the first place). So comparing two variables should only cost a quick integer comparison instead of the current string comparison which is costly. For example if we keep a "name-based" representation an identifier could be:

case class Identifier(tag: String, id: Int) {
  def toString = s"$tag$id"
  def equals(other) = this.id == other.id
  def hashCode() = id.hashCode()
}

So when you look at a program as a human you might see variables tile0, tile1 and x2, but our compiler would only really care about variables 0, 1 and 2 for processing.

from shine.

We could also add to this issue the question of whether we want to use nameless representations such as DeBruijn indices or Abstract Syntax Graphs.

from shine.

@Bastacyclop I find this a good idea, and it looks like it should be relatively easy to implement. I will open an issue.

from shine.

note: after #214 and related equality saturation PRs, it should be possible to implement enforcing unique names as going through the DeBruijn representation:
def rename(e: core.Expr): core.Expr = eqsat.Expr.toNamedUnique(eqsat.Expr.fromNamed(e))

from shine.