[Haskell-cafe] What's the motivation for η rules?

[Dan Doel]

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