## Eta-expansion of abstractions outside the lambda-calculus

I've been reading up on multi-stage programming recently and came accross Eta-expansion does The Trick which interests me because partial evaluation is something I think deserves higher visibility in programming in general.

I've seen η-expansion in the context of the various λ-calculi before but I can't seem to translate this to algol style languages. I must be missing something trivial or obvious. Could anyone please enlighten me?

## Comment viewing options

### Suppose we've got an

Suppose we've got an imperative language in named style (where every side-effecting expression gets its own name):

e ::= n | x | e = e | e + e | etc. (only pure expressions go here)

c ::= e | !e | ref(e) | e := e' | let x = c1 in c2


Here, !e dereferences a pointer, ref(e) allocates a new pointer pointing to e, and e := e' evaluates e to a pointer value, and then updates it with e'. let x = c1 in c2 evaluates c1, binds its result to the variable x, and then evaluates c2.

This language is extremely close to being in monadic style, and in fact that's the idea that gives the eta-expansion rule for it:

c == let x = c in x


We also have a beta-rule for this language:

let x = e in c ==  c[e/x]


and also a commuting conversion:

let x = (let y = c1 in c2) in
c3

==

let y = c1 in
let x = c2 in
c3


### Let me see if I have this right...

So you simply wrap a function around the statement/command?

If you were using a language without inferred types would the enclosing function have to bind the free variables of c?

I can see what you mean by the monadic comment from the code examples. Reminds me of Monad Laws in do notation.

Thanks for the information.

### There are no functions in

There are no functions in the little language I sketched out. The eta rule is exactly the observation that let x = c in x and c compute the same thing. So in C, this would be the equivalence of:

int x = expression;
return x;

compared to

return expression;


Thanks again.