[Haskell-cafe] What's the motivation for η rules?
Dan Doel
dan.doel at gmail.com
Tue Jan 4 04:43:03 CET 2011
On Monday 03 January 2011 9:23:17 pm David Sankel wrote:
> The following is a dependent type example where equality of open terms
> comes up.
>
> z : (x : A) → B
> z = ...
>
> w : (y : A) → C
> w = z
>
> Here the compiler needs to show that the type B, with x free,
> is equivalent to C, with y free. This isn't always decidable, but eta
> rules, as an addition to beta and delta rules, make more of
> these equivalence checks possible (I'm assuming this is
> what extensionality means here).
Extensionality of functions (in full generality) lets you prove the following:
ext f g : (forall x. f x = g x) -> f = g
This subsumes eta for every situation it applies in, because:
ext f (\x -> f x) (\x -> refl (f x)) : f = (\x -> f x)
although making the equality that type checking uses extensional in this
fashion leads to undecidability (because determining whether two types are
equal may require deciding if two arbitrary functions are equal at all points,
which is impossible in general).
The reverse is not usually the case, though, because even if we have eta:
eta f : f = (\x -> f x)
and the premise:
pointwise : forall x. f x = g x
we cannot use pointwise to substitute under the lambda and get
necessary : (\x -> f x) = (\x -> g x)
Proving necessary would require use of ext to peel away the binder
temporarily, but ext is what we're trying to prove.
So, although eta is often referred to as extensional equality (confusingly, if
you ask me), because it is not part of the computational behavior of the terms
(reduction of lambda terms doesn't usually involve producing eta-long normal
forms, and it certainly doesn't involve rewriting terms to arbitrary other
extensionally equal terms), it is usually weaker than full extensionality in
type theories.
> What would be example terms for B and C that would require invoking the eta
> rule for functions, for example?
It could be as simple as:
z : T f
z = ...
w : T (\y -> f y)
w = z
On the supposition that those types aren't reducible. For instance, maybe we
have:
data T (f : Nat -> Nat) : Set where
whatever : T f
Without eta, the types aren't equal, so this results in a type error.
-- Dan
More information about the Haskell-Cafe
mailing list