What is hereditary substitutio,n and why should I use it?
I've been taking a look at hereditary substitution for my little programming language, because hereditary substitution is supposed to give a particularly clean categorical semantics for Cartesian categories, as you don't need to quotient by small step or big step relations.
I've run into a few issues that could use clarity, and need help with better examples and explanations.
I'm not sure how important this is, but for making substitution total, I've found multisubstitution of all the variables in the environment simpler.
In general, I've found making hereditary substitution total over undecorated terms that are not necessarily well-typed an annoying side issue. Using the option monad complicates stating and proving important properties like associativity.
I've also found hereditary substitution not so useful for logic programming fragment of my language which doesn't really admit straightforward big step semantics. Hereditary substitution seems to work best with values and particularly Cartesian closed categories. I am not really sure how hereditary substitution for substructural languages ought to work for example.
Eta expansion seems to rely on unique introductions for types. For example eta expansion for sum types isn't really clear to me.
In general, it's not clear to me why hereditary substitution is the way it is or how to extend it for very different languages.