On Tue, Apr 12, 2016 at 4:01 PM, David Feuer
I have heard of this "eta rule" before, but I know nothing about type theory. What does the rule say?
In the general use case, "eta rules" are rules that state that any term of a given type must have a specific form defined by the introduction and elimination rules for the type. The standard/original version of eta is for function types: forall (e :: a -> b). e = (\x -> e x) But we can generalize this to other types with a single constructor. For example: forall (e :: ()). e = () forall (e :: (a,b)). e = (fst e, snd e) For any given language/theory, these various eta rules may or may not be true. In Haskell because of decisions about un/liftedness, they prettymuch never hold at the term level. The major counterexamples being _|_ /= (\x -> _|_ x) and _|_ /= (fst _|_, snd _|_). Of course, one could have eta for functions without having it for tuples, and vice versa; there's nothing tying them together. Getting back to the original query, the question is whether these eta rules hold "one level up" where types must be expandable/contractible in particular ways based on the intro/elim rules for their kind. Since we don't have any notion of undefined at the type level, the obvious counterexamples go away; but that still doesn't guarantee they hold. (For example, if we do not allow reduction under binders, then the eta rule for functions won't hold (except perhaps in an up-to-observability sort of way)). -- Live well, ~wren