Make Expr type explicit, add Literal constructor

[rvs314]

This adds Expr as a union of either Variables, Terms or Literals, the last of which being a new protocol with a default implementation. The new constructor makes sure we can distinguish terms-as-values vs terms-as-terms (Literal[Term[A]] != Term[A]).

[eb8680]

Can you rename Literal to e.g. Atom or Constant so that it doesn't collide with typing.Literal?

[rvs314]

Can you rename Literal to e.g. Atom or Constant so that it doesn't collide with typing.Literal?

That makes sense - I've renamed it to Constant

[eb8680]

Going to merge this for now because it's more correct than the current version, but I think to correctly support higher-order syntax we might actually want Expr = Term[T] | T where variable contexts are determined by typing rules associated with each Operation. (In that approach, Variable is an Operation with a typing rule that introduces a fresh variable in its result context).

That's how things work in Funsor, and I think that's standard in literature on generalized algebraic theories.