typed eta reduction, subtypes, etc.

• To: types@theory.lcs.mit.edu
• Subject: typed eta reduction, subtypes, etc.
• From: jcm@ra.stanford.edu (John Mitchell)
• Date: Thu, 9 Jun 88 21:13:55 PDT

What started out as a petty technical bicker has certainly
taken an interesting turn. As far as "typed lambda calculus"
in which every term has a unique type, I hope everyone agrees
that eta makes some sense. If A->B is the type of functions from
A to B, and both M:A->B and \x:A.Mx:A->B, then these two terms
define the same function, and can considered equal.

For systems with subtypes, or other ways of varying the domains
of functions, the situation is more complicated. As Vaughan points
out, \x:A.fx = f doesn't make that much sense if dom(f) is bigger
than A (or less than A?). For example, if we use retracts as
types (a la Scott's Pw paper), then

	\x:A.fx = \x.f(Ax)  =\= f

so this funny kind of eta fails.
I suppose this must be more or less what is going on in the
"interpretations" of subtyping various people have mentioned.
If we think of \x:A.fx as restricting the domain of f, then
removing \x:A..x obviously changes the meaning of a term.

 

• Prev: Seminar announcement
• Next: Type inference and implicit conversions
• Index(es):
  • Main
  • Thread