Lambda the Ultimate

We're familiar with the notion of function composition which is essentially sticking functions end-to-end:

(a -> b) -> (b -> c) -> (a -> c)

However, is there any formal treatment of function "concatenation" for functions that operate on n-tuples that would be essentially sticking functions "side-by-side"? The type would be something like this (where a, b, c, and d are n-tuples and ++ is the concatenation operator):

(a -> b) -> (c -> d) -> (a ++ c) -> (b ++ d)

I think a visual example allows a good intuition for what I'm talking about. If F is a function from a 1-tuple to a 2-tuple, and G is a function from a 2-tuple to a 1-tuple, then their composition would be this:

     IN
      |
   .--o--------.
   |     F     |
   |--o-----o--|
      |     |
   .--o-----o--.
   |     G     |
   |--o--------|
      |
     OUT

and their concatenation would be this:

     IN          IN    IN
      |           |     |
   .--o--------.--o-----o--.
   |     F     |     G     |
   |--o-----o--|--o--------|
      |     |     |
     OUT   OUT   OUT

Composition indicates a dependence (e.g. G is dependent on the output of F) that requires sequential evaluation whereas concatenation indicates an independence (e.g. F and G do not share inputs) that allows for parallel evaluation. Both operations are associative.

There exist operations with a similar spirit to the concatenation expressed above: the functional form of construction in Backus's FP, the *** operator for the -> arrow in Haskell, and the family of spread combinators in Factor to name a few. However, none of these deal with concatenated inputs/outputs and none of these are associative, so they're not quite what I'm after.

Any pointers towards related mathematical notions or languages with a similar feature would be much appreciated.

As a mathematician who's quite new to type theory, I have only vaguely internalised the fact that forall a.a and Pi a.a (or whatever the appropriate ASCII-isations are) mean the same thing. Thus, although it seems obvious to me that forall a.a is empty (or does one say uninhabited?), I was nonetheless quite startled to read the following in Barendregt's "Introduction to generalised type systems", p. 132:

… write \bot \equiv (\Pi \alpha : *. \alpha), which is the second-order definition of falsum.

I tried to re-cast this in language more familiar to me, and wound up with the statement that the product of all sets is empty.

Now, I know that type theories tend (understandably) to be biased more towards constructivist than traditional ZFC-based axiomatisations; but it seems to me that, beyond just saying that we don't assume the Axiom of Choice, this statement is saying that we take that axiom as the definition of ‘false’! Is the rejection of choosiness really so definitive, or am I just skipping over some point (like, say, that some sets are empty, so that including them in the product will naturally make it, too, empty)?

Monads in Action, Andrzej Filinski, POPL 2010.

In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be evaluated according to an effect-free semantics. Any effect-specific operations expressible in the monad are also given purely functional definitions, but these definitions are only directly executable in the context of an already translated program. This approach thus takes an inherently Church-style view of effects: the nominal meaning of every effectful term in the program depends crucially on its type.

We present here a complementary, operational view of monadic effects, in which an effect definition directly induces an imperative behavior of the new operations expressible in the monad. This behavior is formalized as additional operational rules for only the new constructs; it does not require any structural changes to the evaluation judgment. Specifically, we give a small-step operational semantics of a prototypical functional language supporting programmer-definable, layered effects, and show how this semantics naturally supports reasoning by familiar syntactic techniques, such as showing soundness of a Curry-style effect-type system by the progress+preservation method.

The idea of monadic reflection was one I never felt I really understood properly until I read this paper, so now I'll have to go back and re-read some of his older papers on the subject.

Is anybody aware of university courses (or textbooks) with a focus on the design of just-in-time compilers (JITs)? (Basically, as alternative to a standard compiler construction course)

In the last few years there has been some interesting research on the topic of JITs, (many being mentioned here on LtU), e.g., the Javascript JITs (TraceMonkey, Google V8), the PyPy JIT, LuaJIT, the recent story about verified JITs, Factor's compilation strategy might also be of interest, etc..

So far, I have not found any course focusing on JITs. At most, some compiler construction courses mention JIT technology (usually Java's) in passing. The textbook situation seems to be equally bland.

As I started learning category methods, I noticed that my prior attitude dismissing it as "abstract nonsense" was based upon ignorance. As somebody with physics background I begin to appreciate shifting emphasis from objects onto symmetry, invariance (err morphisms). So in order to understand structure one has to master morphisms. Fine.

Let's compare this with algebraic perspective. There we study objects and operations between them. When we constrain those operations with some axioms we get an algebraic system. A significant part of studying a concrete algebra would be discovering its axiom system. For example, Relation Algebra has been discovered by Pierce, but hasn't been fully axiomatized until Tarski.

Now, how would I study Relation Algebra with methods of category theory? As discovery is significant element of algebraic method and category theory is in a sense dual perspective, I'd guess drawing arrows wouldn't advance me too much, and I would have to discover some important morphisms... Perhaps, a helpful analogy would be how is it done in other categories (preferably, from elementary mathematical fields:-)?