Usual NbE algorithms, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms.
Is there algorithms to (efficiently) exploit host language constructs to normalize terms to beta-eta normal form?
Usual NbE algorithms, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms.
Is there algorithms to (efficiently) exploit host language constructs to normalize terms to beta-eta normal form?