Lowering your continuations while lifting your functions (in Python)

 A Previous post describes Python code that does functional composition on reversible code. A question that one asks when starting to write compositional code is: how does one compose functions 'at different levels'? And I purposely express this a bit ambiguously as 'different levels' can mean different things. Today we will care about levels within a hierarchy of data containers and simple objects, and note a thing or two on the way.

The map function is Python's builtin tool to apply a function over each data of a container. Combined with a lambda or a function definition we can convert fonctions on container elements to functions on containers. Jargon for this type of code is that we are lifting a function to the container. The idea being that a function on a container is higher than function on container elements.

An important detail to note, is that while the mapped function is being lifted, the continuation context needs to be 'lowered'. This is because the lifted function will later be called with a continuation context for the container, yet internally the original mapped function is called, and it will need 'additional' continuation context. Therefore an extra level of continuation is added in to 'lower it' down to the level of the mapped function. Two examples are given, the first  

• "Lowers down" a detached generic continuation context. 

python

The second

• "Lowers down" a location carrying continuation. 

python (container), python (object)

Another particularity of this mapping code is that these extended / lowered continuation are data constructors. Which makes sense because for each element we need its return value to be become data to be put into the resulting mapped container.  This data constructor nature of the continuation extension also reflects the nature of the continuation changing as it enters the data container that is being mapped.

And this brings up an anecdote:

As I wrote these mapping functions, I was immediately reminded of the Newton programming language by Prof. Rapin EPFL. Sadly, I could not find a freely available document on Newton, yet if my memory serves me well, Newton had a higher order container location abstraction that provided a service not very different to our subject here. (One of my CS MS semester projects had me extending the Newton compiler,  in ~1985).

This continuation 'extension' technic has strong ties to the zipper structures for container traversals.

Yet more importantly it reminds us that within a more formal approach to code function arguments may be expressing:

1. What is coming in to the function.
2. The call contexts to the function.
3. Contexts of immediate use of the function's results.

Within a continuation passing style, it is therefore perfectly ok to decorate your continuations to communicate more context to your functions. In the example code referred to here, the 'lowered' continuation carries index positions, dictionary keys, and dataclass field names. 

All original content copyright James Litsios, 2021.

Data composition from functional composition in Python

Previous post describes code that does functional composition. Let's now add operators that convert this functional composition to become data composition, and allow what is produced to be 'executed later'. Github drop for these code snippet here.

Key insights in writing code this way are:

• Data objects are derived from the functions which define their semantics.
• This is meta-programming 'done backwards'. Like with meta-programming we capture 'what could be interpreted', but we do so through the execution semantics, not by adding an additional meta-language.
• Data objects execution semantics can be ambiguous until ambiguities are removed. Not far from a "quantum-like" execution model!
• There are strong ties here to laziness and trampolining.
• Blockchains are as much about composition of data, as about composition of functions.

These example code snippets are very short (<100 active lines). Two design choices make this possible: 

1. Focus on arguments, not return value, nor object state
2. Make everything composable 

What these examples hint at is:

• Return values are really just arguments to further calls. 
• Object states are really just arguments, references (e.g. function reference), and contexts of possible further calls.

This is in fact true at the most simple level, such as in the code tied to this posting. 

All original content copyright James Litsios, 2021.

Point-free reversible Python

Have you ever wanted to to write 'formal style' in Python?

If so, these snippets of code which I shared on gitbub might please you.

What is a formal style of programming

Formal "code", like formalism in mathematics, is to solidly tie what you write to what you mathematically mean. And that connection goes both ways: from math to expression, from expression to math. 

The traditional way to write formal code is to prove as much as you can 'along the way' of writing code. The difficulty of this approach is that proofs are hard, which either limits the complexity of your code, or limits your ability to be productive.

Another way to write code with mathematical properties is to assemble pieces of code that already have mathematical properties. When this assembly preserves these mathematical properties, and even better when it scales them, the resulting code has mathematical properties.  A key concept here is that these "pieces of code with mathematical property" are "at different levels", as it is the interplay between these levels that give the code its semantic depth.  (This last point explains why languages like Prolog are hard to scale).

Dualities are good place to find mathematical properties.  An example of duality is symmetry: something can be 'one way' and 'the other', and we know "mathematically" what that means. This is why reversible code,  reversible types, adjoint structures, and pretty much anything that goes 'one way' and 'the other' (e.g. like rows and columns) are a good basis on which to build systems with formal properties.

What is reversible programming?

Reversible expressions can be evaluated 'one way' and 'another'. This might be execution evaluation that might be reversed, yet might also mean that the interpretation of the expression can be seen from a reversed perspective at different semantic level (e.g. types, external view).

Reversibility is also a way to approach multi-party programming: Say I am party Alice having received B from Bob, after having previously shared A with Bob. Alice can reverse compute B to A to validate that Bob computed B from A. That is a simplified view of things, but it captures the idea that reversibility enables trust.

Reversibility is much like immutability that has been weakened, but which has not lost its magical properties.

What is point-free style?

A point-free (or tacit) style of programming traditionally means coding by composition without naming arguments (and without assignments). In a Python centric view that could mean to only use 'positional arguments', and to use only Callable objects (so as not to have method names), but you need to ask yourself: "Is that important"? In fact within the scope of reversible programming, point-free is best approached as composable and reversible. That you name things or not is of lesser importance. In fact, it is of lesser importance also because the traditional point-free is to focus on 'expression space'. Yet modern programming happens much at the type level, or the meta-type level, and a strict point-free approach would lead us to writing code where types are nameless, as well as meta-types. That would be tricky!

Note here: Point-free much leads to array, stream and structural oriented programming. This is not lost here. In fact a main reason to write code like this in Python is to write structural oriented ML. Reversibility is also a vital piece of blockchain and smart contracts theory too.

Why should you care?

Wikipedia's programming paradigm page enumerates many ways to code. Reversibility is one of the concepts that brings together all of these different ways of expressing software. Putting reversibility 'underneath' a paradigm gives it bridges to other paradigms that have also been given reversibility properties. 

All original content copyright James Litsios, 2021.