Equational

 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 beca...

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:  Focus on argument...

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 proper...