Return to Answer

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on the lexicographic product of terms and types.
• Predicative System F can be normalized by induction on the lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with: if we use stronger metatheoretic features, we can implement normalization in more convenient ways. For example, logical relations use large elimination on syntactic types, and so does normalization-by-evaluation. Comparing hereditary substitution to NbE:

• It scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things, or if we want to show that our syntax of normal forms yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I note again that you are free to use any normalization algorithm for defining substitution on normal terms.

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on a lexicographic product of terms and types.
• Predicative System F can be normalized by induction on a lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with: if we use stronger metatheoretic features, we can implement normalization in more convenient ways. For example, logical relations use large elimination on syntactic types, and so does normalization-by-evaluation. Comparing hereditary substitution to NbE:

• It scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things, or if we want to show that our syntax of normal forms yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I note again that you are free to use any normalization algorithm for defining substitution on normal terms.

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on the lexicographic product of terms and types.
• Predicative System F can be normalized by induction on the lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with: if we use stronger metatheoretic features, we can implement normalization in more convenient ways. For example, logical relations use large elimination on syntactic types, and so does normalization-by-evaluation. Comparing hereditary substitution to NbE:

• It scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things with our syntax, or if we want to show that our syntax yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I would again note that you are free to use any normalization algorithm for defining substitution on normal terms.

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on the lexicographic product of terms and types.
• Predicative System F can be normalized by induction on the lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with: if we use stronger metatheoretic features, we can implement normalization in more convenient ways. For example, logical relations use large elimination on syntactic types, and so does normalization-by-evaluation. Comparing hereditary substitution to NbE:

• It scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things, or if we want to show that our syntax of normal forms yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I note again that you are free to use any normalization algorithm for defining substitution on normal terms.

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on the lexicographic product of terms and types.
• Predicative System F can be normalized by induction on the lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with; if we use more liberal metatheoretic features, we can implement normalization in more convenient ways. For example, compared to normalization-by-evaluation:

• Hereditary substitution scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things with our syntax, or if we want to show that our syntax yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I would again note that you are free to use any normalization algorithm for defining substitution on normal terms.

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are "quasi-normal-forms" by Scherer. These support easy conversion checking, but still require an actual conversion relation. In any case, deciding eta for sum types is a large increase in formal complexity and it's probably not worth it for you. If you must have eta for sums, then the straightforward solution is to use non-normal syntax (with quotients or conversion relations), and perhaps postulate decidability of conversion.

The main point of hereditary substitution is essentially reverse mathematics: we're interested in simple "syntactic" termination measures for normalization.

• STLC can be normalized by induction on the lexicographic product of terms and types.
• Predicative System F can be normalized by induction on the lexicographic product of terms, types and multisets of universe levels.

However, if we don't care about reverse mathematics then there isn't really any reason to use hereditary substitution. Its suitability for reverse mathematics is what makes it more difficult to work with: if we use stronger metatheoretic features, we can implement normalization in more convenient ways. For example, logical relations use large elimination on syntactic types, and so does normalization-by-evaluation. Comparing hereditary substitution to NbE:

• It scales worse: it can't handle impredicativity, and it's not known if it works for dependent types.
• It's operationally less efficient.
• It's formally more difficult to handle, especially in proving correctness of normalization, which is required if we want to do slightly more interesting things with our syntax, or if we want to show that our syntax yields an initial model of some algebraic theory (e.g. cartesian closed categories, or simply typed categories-with-families).

If you want to skip quotients and conversion by only working with normal forms, it is not required to implement substitution as hereditary substitution; you can use pretty much any normalization algorithm. With NbE, substitution for normal terms is recovered by evaluating normal terms in the appropriate value environments, then quoting the result.

I'm not familiar with normalization for substructural theories; for these I would again note that you are free to use any normalization algorithm for defining substitution on normal terms.