Lambda the Ultimate

In λ-calculus, all functions are unary, and n-ary functions are encoded through currying. But knowing the arity of a function can be useful for optimization — a curried function starts computing only after applying it to at least N arguments, and this N can be useful to know.
It seems that call-by-push-value(CBPV) allows dealing with arities in a convenient way, as discussed below, though that was not the main design goal. My questions are:

1. Is this true?
2. Is this already known?
3. Would you recommend call-by-push-value, or are there downsides which make it unsuitable?

Below I explain the details.

Applications of arity:
(1) In GHC, that's useful to deal differently with partial applications — because e.g. a function body only computes after specifying enough arguments (in simple cases, that is barring some optimizations, as many arguments as specified in the left-hand side of the equations defining the function).
(2) In my case, I'm working on a program transformation: transforming a function f gives a function f* that returns f's final result and all its intermediate results. This can be useful for incremental computation (along ideas by Liu and Teitelbaum (1995)). Here, too, it seems silly to return intermediate results of a partial application.

But function arity is a tricky concept in λ-calculus. For instance, id should be unary, Haskell's ($) is binary, but ($) is defined as equal to id:

($) :: (a -> b) -> a -> b
($) = id

So, a notion of arity seems tricky, and one of my colleague keeps repeating it's a bad idea.

Today, while reading a paper using CBPV (Hammer et al. 2014), I got a hunch that the call-by-push-value (CBPV) λ-calculus seems to allow for a natural notion of arity. But Googling does not find this spelled out anywhere, maybe because CBPV seems typically used in theoretical contexts. I'm

So, why should CBPV help?

(1) It distinguishes values (A) and computations (C): Computations are either functions (A -> C) which take values and return computations, or base computations F A which wrap values in a "return" expression:

C ::= A -> C | F A

So, the return type of a function is wrapped by the F constructor. In particular, this distinguishes A1 -> A2 -> F A3 (a binary function) from A1 -> F (U (A2 -> F A3)), a unary function returning another unary function.
U is a type constructor for values representing thunks.

(2) Moreover, we also distinguish partial and full applications: since a full application produces a result of type F A, we need to use the elimination form for F.

Thus, after conversion to CBPV, we can distinguish syntactically between partial and full applications.

Questions:
- is this a good way to define a notion of arity?
- would it be better to just introduce multi-argument functions? I suspect not, because those prevent abstracting over arity, while CBPV you can still write forall A B. (A -> B).
- does the translation have downsides? I imagine that ($) = id transforms to something more complicated in CBPV, which would involve (the equivalent of) a full eta-expansion first.
- The GHC core language does have a notion of arity, but it does not seem as elegant as far as I can tell.
- is there an extension of CBPV to calculi richer than STLC, say to System F? I've heard people saying that focusing and polarity runs into some form of trouble with System F, but I haven't heard why. Interestingly, Levy's own paper dealing with System F (http://www.cs.bham.ac.uk/~pbl/papers/polynorm.pdf) does not use CBPV, but Jump-With-Argument.

Bibliography:

Liu, Y. A., and Teitelbaum, T. Caching intermediate results for program improvement. In Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation (New York, NY, USA, 1995), PEPM '95, ACM, pp. 190—201.
Hammer, M. A., Phang, K. Y., Hicks, M., and Foster, J. S. Adapton: Composable, Demand-driven Incremental Computation. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (New York, NY, USA, 2014), PLDI '14, ACM, pp. 156—166.

Hi all :)

I'm thinking about extending Wikipedia with a new page: Structured BNF. Is anyone interested in helping in changing content or lecturing it before I publish it? I would appreciate any comment, even if you think that this is not a thing to place in Wiki.

here is the content

While waiting for my plane and thinking about a what a VHDL/Verilog killer would look like, I had a very (un!)original idea: describe what is to be done in English, and let the killer do the code derivation.

Here is an example of a description of how I want my blob detection (a computer vision application) be done on incoming images:

blob detection, image processing
- connect neighboring high-intensity pixels
- high-intensity - values exceeding a threshold
- neighboring pixels of an image
- 8 pixels surrounding the pixel in question
- image is a 2d array of pixels, variable width and height
- pixels come one by one
- pixels are 8 bits, but can be larger
- threshold is variable at run time
- use png files as test images

This description is enough for a human to write the code, but not so for a computer, that has no understanding of any of these words.

Now my question is, is there anyone working on this?
If not---why not?

To start working on this, here is what I want to do (in my spare time):
- P. Norvig's PAIP has a chapter about solving simple math questions written in English. That's my starting point to derive some sort of meaning from English language description.
- Get from meaning to code. Probably, I will have to search through a code space to satisfy the meaning derived.

I like to hear your reasons on why it is or is not possible!