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

[David Sankel]

Thanks for the detailed response...

On Thu, Dec 30, 2010 at 9:54 AM, Conor McBride
<conor at strictlypositive.org>wrote:

> On 28 Dec 2010, at 23:29, Luke Palmer wrote:
>
>  Eta conversion corresponds to extensionality; i.e. there is nothing
>> more to a function than what it does to its argument.
>> I think
>> Conor McBride is the local expert on that subject.
>>
>
> ...I suppose I might say something.
>
> Dependent type theories have programs in types, and
> so require some notion of when it is safe to consider open terms equal
> in order to say when types match:


An attempt to recapitulate:

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).

What would be example terms for B and C that would require invoking the eta
rule for functions, for example?

it's interesting to see how far one
> can chuck eta into equality without losing decidability of conversion,
> messing up the "Geuvers property", or breaking type-preservation.
>
> It's a minefield, so tread carefully. There are all sorts of bad
> interactions, e.g. with subtyping (if -> subtyping is too weak,
> (\x -> f x) can have more types than f), with strictness (if
> p = (fst p, snd p), then (case p of (x, y) -> True) = True, which
> breaks the Geuvers property on open terms), with reduction (there
> is no good way to orientate the unit type eta-rule, u = (), in a
> system of untyped reduction rules).
>
> But the news is not all bad. It is possible to add some eta-rules
> without breaking the Geuvers property (for functions it's ok; for
> pairs and unit it's ok if you make their patterns irrefutable). You
> can then decide the beta-eta theory by postprocessing beta-normal
> forms with type-directed eta-expansion (or some equivalent
> type-directed trick). Epigram 2 has eta for functions, pairs,
> and logical propositions (seen as types with proofs as their
> indistinguishable inhabitants). I've spent a lot of time banging my
> head off these issues: my head has a lot of dents, but so have the
> issues.
>
> So, indeed, eta-rules make conversion more extensional, which is
> unimportant for closed computation, but useful for reasoning and for
> comparing open terms. It's a fascinating, maddening game trying to
> add extensionality to conversion while keeping it decidable and
> ensuring that open computation is not too strict to deliver values.
>
> Hoping this is useful, suspecting that it's TMI
>

Very useful. Not TMI at all. I find this fascinating.

David


-- 
David Sankel
Sankel Software
www.sankelsoftware.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110103/ab416ac0/attachment.htm>