Hydra's epsilon encoding (which maps types to terms, found in Hydra.CoreEncoding and Hydra.CoreDecoding, currently only in Haskell) is not a faithful implementation of the epsilon encoding described in the Lambda Graph spec. This is one of the few remaining points of misalignment between Hydra and the spec. The reasons are practical ones, e.g. encoding "forall" types as lambda terms (as opposed to records) causes certain problems. Determine whether these problems lie with the implementation, or with the specification. Some assumptions have been made about the epsilon encoding in the spec which have not yet been proven (e.g. that type reduction can be performed by first epsilon-encoding a type, applying term reduction, then decoding the type). Prove or disprove them.
Hydra's epsilon encoding (which maps types to terms, found in
Hydra.CoreEncodingandHydra.CoreDecoding, currently only in Haskell) is not a faithful implementation of the epsilon encoding described in the Lambda Graph spec. This is one of the few remaining points of misalignment between Hydra and the spec. The reasons are practical ones, e.g. encoding "forall" types as lambda terms (as opposed to records) causes certain problems. Determine whether these problems lie with the implementation, or with the specification. Some assumptions have been made about the epsilon encoding in the spec which have not yet been proven (e.g. that type reduction can be performed by first epsilon-encoding a type, applying term reduction, then decoding the type). Prove or disprove them.