[Haskell-cafe] Is it safe to postulate () has one inhabitant?
winterkoninkje at gmail.com
Wed Apr 13 00:43:39 UTC 2016
On Tue, Apr 12, 2016 at 4:01 PM, David Feuer <david.feuer at gmail.com> wrote:
> 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.
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)).
More information about the Haskell-Cafe