Talk:Constant applicative form

Q&A discussion from HaWiki

What is the difference between ((+) 4) and \x -> (+) 4 x, apart from the obvious difference in notation? (I have braced the + to make the expressions compliant with Haskell syntax.)

One is an application that returns a function and may imply some work in general, the other is a syntactic value (a lambda abstraction).

If notation really happens to matter so much, then what about (4 +) and (+ 4)? Are both of these CAFs? If we take away the nifty syntax, how do we express (+ 4) then? Or is it no longer a CAF? ;)

It depends on how they desugar. `(4 +)` presumably desugars to `((+) 4)` and so is a CAF. If (+ 4) desugars to `\x -> x + 4` it isn't, if it desugars to `flip (+) 4` it is. -- DerekElkins

--- Rambler I'm afraid I still don't get it (or maybe I do, but I secretly wish it didn't mean that...) To the best of my understanding of the matter, `flip (+) 4` should return something that should behave exactly as `\x -> x + 4` would. Moreover, even if I take it for granted that `flip (+) 4` differs dramatically from `\x -> x + 4`, what happens when we expand the former?

There is no difference in behavior as far as meaning is concerned. They are just treated differently. -- DerekElkins

Suppose `flip` is defined as `\f x y -> f y x` (which it probably is, anyway,) then `flip (+) 4 where flip = \f x y -> f y x` is obviously not a CAF, according to the definition.

What about `flip (+) 4 where flip f x y = f y x`???

I believe that FOLDOC is incorrect here. A better way of thinking about CAFs is that a CAF is anything that can be let floated (see lifting pattern) to the top level. So a CAF can not only call other CAFs, but also other super combinators.

I believe that's already granted, according to the definition of a super combinator. A CAF may reference any super combinator simply by virtue of being one.

The difference between flip (+) 4 and \x -> x + 4 is that in a pure lambda calculus implementation, the former can be reduced but the latter cannot. Remember that \f x y -> f y x is a shorthand for \f -> (\x -> (\y -> f y x))), which means if given two arguments, it can be reduced. --AndrewBromage

Fine, is it then irreducibility that makes CAFs special? If so, then the current formulation of the definition clearly misses the point. If not, then why is this distinction relevant in the context of the definition?

In any case, I am left wondering 1) why irreducible expressions might be of such interest (apart from the trivially imaginable,) and 2) whatever happened to the proverbial referential transparency. It just struck me lately that my difficulty may be due to the fact that I am trying to make sense of CAFs in a broad theoretical context, whereas they may be simply an implementation instrument -- is this the case? --Rambler

You've inverted it slightly (or it reads that way): it's reducibility that makes CAFs special. Since they are reducible they may imply work; work that could be saved. Nevertheless, yes, one typically doesn't care whether something's a CAF or not as far as meaning goes. Read the relevant parts of the book I linked to below, if you haven't already. As for ReferentialTransparency, whether or not something is viewed as a CAF doesn't change it's meaning, i.e. it is just a different implementation of the same function. -- DerekElkins

OK, it definitely makes sense now, thanks to everyone for the explanations and references. --Rambler