Determine if enforcing unique names is required (and implement it) or not

[michel-steuwer]

After switching to the unified DSL with #76 we no longer enforce unique names in Rise.

Do we still need to do this? Currently, all tests pass without enforcement of this.

Can we find a counterexample that shows that this is still required?

If we need to enforce unique names for binders, we need to implement this at the value and type level.

[Bastacyclop]

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.

[Bastacyclop]

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.

[umazalakain]

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

[Bastacyclop]

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))