Lambda the Ultimate

Multi Level Languages are Generalized Arrows - Adam Megacz, 12 pages

Multi-level languages and Arrows both facilitate metaprogramming,the act of writing a program which generates a program. The arr function required of all Arrows turns arbitrary host language expressions into guest language expressions; because of this, Arrows may be used for metaprogramming only when the guest language is a superset of the host language. This restriction is also present in multi-level languages which offer unlimited cross-level persistence. The converse restriction, that the host language is a subset of the guest language, is imposed for multi-stage languages – those multi-level languages with a run construct.

This paper introduces generalized arrows and proves that they generalize Arrows in the following sense: every Arrow in a programming language arises from a generalized arrow with that language’s term category as its codomain (Theorem 4.5.4). Generalized arrows impose no containment relationship between the guest language and host language; they facilitate heterogeneous metaprogramming. The category having all generalized arrows as its morphisms and the category having all multi-level languages as its morphisms are isomorphic categories (Theorem 4.7.8). This is proven formally in Coq, and the proof is offered as justification for the assertion that multi-level languages are generalized arrows.

[...]

Why heterogeneous metaprogramming? The effort expended in this paper is largely unnecessary if we are content with guest languages which are the same as – or even supersets of – the host language. The simplest “naturally occurring” example is that of invertible programming, as shown in the running BiArrow example of Section 3.2. An invertible programming language cannot include all of Haskell, since Haskell has functions which are quite obviously not invertible (e.g. fst).

Beyond applications like BiArrow which fit in a paragraph or two lie more appealing examples, including the design of digital circuits (much like Lava [BCSS98, SJRI01, GBK09]), stream processing of trees [KSK08] based on ordered linear types, and NESL-like data parallelism on platforms without global shared memory where (unlike [CLJ07]) parallelized functionals do not have access to the heap (i.e., they are access-restricted [Ble95, 10.3]).

Much of Adam's work is allowing programs to be embedded in a more natural syntax (i.e. rather than using 'ga_first' and 'ga_second' explicitly). To this end, he provides an extension to GHC and a wrapper syntax for the embedded languages.

Related nodes of interest:

• Arrows generalise monads and idioms
• Causal Commutative Arrows and Their Optimization

I was directed to Adam Megacz's Generalized Arrows while struggling to accurately model asynchronous composition of parallel dataflows for my eventless reactive paradigm. Haskell's Control.Arrow uses the pair type (,) to represent parallel computations. Unfortunately, that fails to capture the notion that different elements of the pair may require a different amount of time (both physically and logically) to compute or (for resources) otherwise acquire. Generalized arrows are at least a partial solution to this issue, e.g. allowing me to develop asynchronous product types and make synchronization a more explicit operation.

I've long been interested in multi-layer languages as a syntactic technique to tame behavior (an alternative to types). Generalized Arrows allow me to do this in the Haskell context. They'll certainly be something I explore further, especially if ever they enter the GHC main branch.