Thanks for the detailed response...<br><br><div class="gmail_quote">On Thu, Dec 30, 2010 at 9:54 AM, Conor McBride <span dir="ltr"><<a href="mailto:conor@strictlypositive.org">conor@strictlypositive.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">On 28 Dec 2010, at 23:29, Luke Palmer wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Eta conversion corresponds to extensionality; i.e. there is nothing<br>
more to a function than what it does to its argument.<br>I think<br>
Conor McBride is the local expert on that subject.<br>
</blockquote>
<br></div>
...I suppose I might say something.<br>
<br>Dependent type theories have programs in types, and<br>
so require some notion of when it is safe to consider open terms equal<br>
in order to say when types match:</blockquote><div><br></div><div>An attempt to recapitulate:</div><div><br></div><div>The following is a dependent type example where equality of open terms comes up.</div><div><br></div>
<div><div>z : (x : A) → B</div><div>z = ...</div><div><br></div><div>w : (y : A) → C</div><div>w = z</div></div><div><br></div><div>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).</div>
<div><br></div><div>What would be example terms for B and C that would require invoking the eta rule for functions, for example?</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
it's interesting to see how far one<br>
can chuck eta into equality without losing decidability of conversion,<br>
messing up the "Geuvers property", or breaking type-preservation.<br>
<br>
It's a minefield, so tread carefully. There are all sorts of bad<br>
interactions, e.g. with subtyping (if -> subtyping is too weak,<br>
(\x -> f x) can have more types than f), with strictness (if<br>
p = (fst p, snd p), then (case p of (x, y) -> True) = True, which<br>
breaks the Geuvers property on open terms), with reduction (there<br>
is no good way to orientate the unit type eta-rule, u = (), in a<br>
system of untyped reduction rules).<br>
<br>
But the news is not all bad. It is possible to add some eta-rules<br>
without breaking the Geuvers property (for functions it's ok; for<br>
pairs and unit it's ok if you make their patterns irrefutable). You<br>
can then decide the beta-eta theory by postprocessing beta-normal<br>
forms with type-directed eta-expansion (or some equivalent<br>
type-directed trick). Epigram 2 has eta for functions, pairs,<br>
and logical propositions (seen as types with proofs as their<br>
indistinguishable inhabitants). I've spent a lot of time banging my<br>
head off these issues: my head has a lot of dents, but so have the<br>
issues.<br>
<br>
So, indeed, eta-rules make conversion more extensional, which is<br>
unimportant for closed computation, but useful for reasoning and for<br>
comparing open terms. It's a fascinating, maddening game trying to<br>
add extensionality to conversion while keeping it decidable and<br>
ensuring that open computation is not too strict to deliver values.<br>
<br>
Hoping this is useful, suspecting that it's TMI<br></blockquote><div><br></div><div>Very useful. Not TMI at all. I find this fascinating.</div><div><br></div><div>David</div></div><br clear="all"><br>-- <br>David Sankel<br>
Sankel Software<br><a href="http://www.sankelsoftware.com">www.sankelsoftware.com</a><br>