# Is this DO LET sugar considered pure Lambda calculus and nullipotent / side-effect-free?

I'm thinking these familiar concepts of DO and LET/LET* in the context of Lambda Calculus (LC).

LET is an abbreviation for this LC expression:

(LET a 1 b 2 e) = (λ a . (λ b . e) 1 2)


and LET* is an abbreviation for this LC expression:

(LET* a 1 b 2 e) = (λ a . (λ b . e 2) 1)


where e is the body of the function. LET* just enables to use former variable inside latter variable in the following way:

(LET* a 1 b a e) = (λ a . (λ b . e a) 1)


DO is an abbreviation too and can be used in conjunction with LET's to achieve same than LET*:

(DO (LET a 1) (LET b 2) e) = (λ a . (λ b . e 2) 1)


So I have three different shorthands to construct LC expressions. Now, my questions is that is this syntactic sugar throwing me out from pure LC (or functional programming in general sense) and am I introducing side effects by this syntax?

In a way it looks like it, but on the other hand these three shorthands are only abbreviations and they translate to Lambda Calculus expressions that are well defined and reducible as any LC expressions.

Anything that can be encoded in the pure lambda calculus, as you realize in the last paragraph, can not have side effects. Otherwise, the lambda calculus itself would be able to express those side effects as well.

However, note that your encoding looks a bit weird. For instance,

(LET a 1 b 2 e) = (λ a . (λ b . e) 1 2)


does not bind 1 to a and 2 to b. You probably want instead

(LET a 1 b 2 e) = (((λ a . (λ b . e)) 1) 2)


which does the correct binding. The other encoding should be fixed similarly.

I would suggest you "test" these encoding by performing $\beta$ steps. If you don't reach $e\{1/a,2/b\}$ something looks wrong.

• You can encode effects such as exceptions with continuations. Commented Sep 25, 2017 at 17:33
• @chi Right, that is exactly how I interpret the notation in my original post. I think both notations should be fine, mainly because expression could be written even less verbose λa.λb.e 1 2 or λab.e 1 2 right? Anyway, we can safely say, that LET and DO as they are presented above, do not side effect? I wonder what would be the global scope then, that would make side effects possible, if not in LC, but some other similar system? Commented Sep 25, 2017 at 17:57
• I mean, what is the trick to jump from the nullipotent to the side-effected system? Commented Sep 25, 2017 at 18:02
• @xavierm02 I agree, but then, what is an "effect" and what is "pure computation", if you can encode the former in the latter?
– chi
Commented Sep 25, 2017 at 18:24
• @chi I have shown in LET and LET* that parentheses do matter in my notation too. Otherwise it is just a matter of decision on evaluation strategy in what order to apply functions, bind arguments and so forth. Evidently it all has an effect to the result. But in this case, because of selection of my strategy, we do talk about same results, with or without parentheses. Commented Sep 26, 2017 at 4:22