Allow name representations other than String

[ocecaco]

The current representation of names is based on a String and a disambiguating integer.

data Name a = Fn String !Integer    -- free names
            | Bn !Integer !Integer  -- bound names / binding level + pattern index

Perhaps it would make sense to make names generic, such that other representations of the name (using Text, for instance), can be used. This would also allow things like attaching additional information to names (e.g., free variables might be tagged with their type).

I would propose a datatype like the following:

data Name f a = Fn f !Integer
              | Bn !Integer !Integer

This is roughly the way I have (manually) implemented binding code in some of my own projects. I also tend to have a separate data type for free variables, which removes the need to check whether a name is a free variable in places where only free variables are expected (for example, a typing context typically does not hold any bound variables), like so:

data Name f a = Name f !Integer

data Var f a = Fn (Name f a)
             | Bn !Integer !Integer

I'm not actually that familiar with the design constraints of unbound-generics, and there might be considerations that make the use of this representation undesirable. I would be happy to hear any thoughts on this, and would also be willing to spend some time to implement this change.

[ocecaco]

I tried to make this change to get a rough initial idea of what the effect would be on the code base, and the main thing is that a lot of the type classes require an additional parameter (I'm not sure if it is possible to abstract this away somehow by using some kind of existential, similar to AnyName). Furthermore, I am not sure how to handle instances like instance Alpha Bool, since the type Bool does not uniquely identify the name representation that should be used.

[lambdageek]

I think this is a good idea, though I think we'll need to break the API to make it happen. Not saying that it's off the table, just that we'll need a major version bump and that I will need help to do it.

---

Details

I think it will require making Alpha a multi-parameter type class so that we can say something like

-- @Alpha n a@ means @a@ is a naming-aware datatype with names constructed using type constructor @n@.
class NameLike n => Alpha (n :: * -> *) a where
  ...

And then we'd have

data AnyName n where
 AnyName :: forall a . Typeable a => n a -> AnyName n

And we would have instances like

-- Bool works will any locally nameless representation `Name f :: * -> *` that represents free names by @f@
instance Alpha (Name f) Bool

[ocecaco]

I've looked at it a bit more, and I've now introduced a multi-parameter type class Alpha (n :: *) a where n indicates the type that should be used for names (e.g., might be Text or String). It's also possible, of course, to have n :: * -> * to make things even more generic, as you have written in your comment.

There do seem to be some tricky things like the type signature for unbind, which becomes:

unbind :: (Alpha n p, Alpha n t, Fresh m) => Bind p t -> m (p, t)

The issue here is that the type parameter n is ambiguous. In practice, there will usually only be one possible type for n, depending on the names that occur in the pattern/term. However, there are cases, like Bind (Embed Bool) Bool where the choice of n is not uniquely determined.

It seems to me that there are two possible solutions to this:

1. Use AllowAmbiguousTypes, which as I understand it ensures that there is only one possible choice for n at the use site.
2. Make sure that the n is uniquely determined by referencing it somewhere in the type signature of unbind. I'm not exactly sure what this would look like, but I think this might require adding an extra type parameter to Bind somewhere.

I've also looked at how Moniker handles this. It seems they effectively use option 1, since their unbind function also has a type parameter n which is not uniquely determined in all cases by p and t. In most cases the choice of n could be omitted, but it might be necessary to tell the Rust compiler which n is desired in ambiguous cases. I'm not sure this choice is equally idiomatic in Haskell however, since it requires a language extension.

EDIT: Actually, in Rust you would use "turbofish" syntax foo.unbind::<String>() to indicate which n you want, but I'm not sure something like that would work nicely in Haskell. It would require TypeApplications, which makes things convoluted and is yet another language extension.