Let me show you a 100x

So, let me show you a 100x for a change. Biological time is running out, so I have to rush out less polished results, but still they are way above average.

What is an intuitive understanding (which can be traced all the way back to the early Upanishads)? It is brain’s way to capture (and “understand”) an observed recurring commonality (a common pattern) without being able to know all the underlying details of how (and exactly why) the pattern emerge.

An intuitive understanding is “cheap” (but very valuable when is correct – precisely why it has been evolved), because reconciling all the relevant details, without introducing abstract bullshit and not missing anything relevant is a daunting task, way beyond human mind capacity.

So, the “modern science” is working by just allowing everyone to publish their mostly wrong abstract bullshit, and the other people would select and reconcile the occasional, rare grains of truths. Think of a large flock of chickens running on a bare ground searching for maize seeds which sometimes are hidden in lumps of cow’s poo (I am not even kidding).

I always wanted to reconcile (or at lest not lose by forgetting) the intuitions (or intuitive insights) I have got by reading a few rare good books on seemingly unrelated subjects. The task, however, was way larger to fit into my tiny, short “attention windows”. This is like running – you have to stop and restart, stop and restart.

The first insight was that thee is what is called duality (structural duality, to be precise) between a definition of a sum-type in say SML or Haskell and a function which consumes such type, defined by clauses, as in SML, Erlang or Haskell, and that this is the only right way to define a total functions out of a set of partial functions (which is what each individual clause is).

Another insight is that once we have GADTs (“indexed” or parameterised Sum-types) we define somethings that is called an Initial Algebra, and a function, defined by clauses, becomes a natural Interpreter.

This pattern is not arbitrary, of course. Natural (evolved or emerged) complexity tends to have a clear layered hierarchical structure (the fact observed by Simon back in the 70s), and each layer (of complexity) shall export its own pure-functional, declarative state-less abstract interface as an embedded DSL, where each layer strictly above it shall have an interpreter for the DLS form the layer strictly below it.

There can be different interpreters for the same “Initial Algebra”, and “composing interpreters” is the only way of proper composition (which is, of course, just nesting of function calls or transformations).

If you read some “obscure” Lecture notes on Cambridge Advanced Functional Programming course, you will find some such interpreters being actually implemented in Ocaml, but everything is still ugly, because Ocaml researches were not smart enough to keep the definition by clauses syntax, as in SML or Shen or Erlang (and use pattern-matching or the = function syntax instead.

But the syntax must be central to a good language,(hi, Dan Grossman) and [syntactic] elegance is not optional, because it gives or reinforces intuitive insights. Uniformity and resulting minimalism are also not optional.

I had the intuitive understanding that “all we need” [is Lambda] (Brian Harvey, the great) are just a few elements of the traditional (evolved) mathematical notation for years – the | , -> () =, were painted on the wall above my bed, but, of course, knowing something intuitively is not enough.

I have accumulated a lot more of intuitive insights. That for all a syntax of Haskell is just (an isomorphic to) a definition of an anonymous Trait, and that Trait Bounds are proper such that clauses, which in turn are boolean expressions (or predicates) at a type-level (and that fucking Java or C++ classes are bullshit cmpared to this generality).

The untyped lambda calculus at the type-level of simply-typed lambda calculus is another obvious intuition. The System F Omega (+ linear logic) is an intuitive foundation of all programming (due to Curry Howard isomorphism and the uniersal structural patters (of a universal DAG) that it captures). I have a lot,

So I’ve unified and reconciled some of my intuitions: https://github.com/lngnmn2/f-lang by creating a language in which the syntax is at the centre, and it captures the underlying semantics with the proper traditional mathematical notation.

What for? Well. there more intuitions, of course. Remember some funny guys who developed the ZIO library for Scala on Youtube (look, ma, I am so smart, I use the M-word!)? They definitely had some intuitive insights, based on frequently observed commonalities (or recurring patterns in the code and internet memes). Know what they were missed? The question: from where these reccurent patterns come from?

The Category Theory (and the wonderful Bartosz in his blog) had some answers for this question, but even he didn’t traced these patterns all the way back to the basic structural elements of a Universal DAG (which can structurally encode any computation). I did.

Every DAG is “just composition of forks, joins and steps”, so is every Algebraic Data Type (which is, of course, a direct consequence). The composition of morphsms in terms of a Category Theory is just composition of “steps”, and those compositions (of steps) sometimes form a commuting diagram, which tell one something about the properties these compositions have.

Again, none of these are arbitrary coincidences – they all capture the “parts of the very same Elephant” (poor, blind philosophers, and I am one of them, realizing that at least the Elephan is indeed one and the same, from which everything follows).

There is more. The basic structural elements are the only possible ones – they are the Universal building blocks of every form of complexity in the Universe, and the only universal way of capturing this is “arrows between dots”. Ok ok.

So, my F-lang is a language where the syntax (and the underlying semantics) directly capture the notion of “just dots between [directed] arrows” (to write composed “interpreters” over GADTs ,constrained by Traits and trait bounds).

As for languages, the theoretical block-chain clowns (hi, vitaliks), are still missing the fact that David Turner’s KRC language (and compilation to SKI combinators) is literally all they need. Just add gas to SKI. Okay, nevermind.

Let’s get serious for a while.

There is the way to program, and it is, indeed, declarative, pure-functional over persistent (structural-sharing) immutable data structures (made out of proper Algebraic Data Types).

The key is to stay as high-level and as close to declarative Gentzen’s Natural Deduction (and the Sequent Calculus) as possible.

One declares an “Initial Algebras” (which is just a particular abstract structure) and how to interpret them, layer by layer, building up a structurally verified DAG, which has to be eventually executed by the mundane “imperative” language runtime, while we stay pure (and simple, all dressed in a spotless while) behind the monadic abstraction barriers. This is not just a pretentious idealism (as on fucking social media) it is the way to have absolute security of a pen-and-paper calculation by substitution of equals for equals at the Model and Business-Logic layers of abstraction.

Here, probably, comes the Nested Interpreters and the miniKaren of Scheme (Racket) tradition, but I am not sure.

What I am sure of is that at any abstraction boundary there shall be a pure-functional abstract stateless DSL (as a public interface), just like that Turtle (drawing) language, and a corresponding interpreter (an evaluator for a DSL, which is, ideally, is just a pure function), outputs of which shall be composed.

To make composition mathematically sound (not arbitrary) one shall not introduce any abstractions beyond those which are structurally forced (by the structure of the underlying DAG), which means, again, just | , -> () =, (and juxtaposition!) where () stands for nesting, and thus the only way to define precedence (an order of evaluation), = stands for mathematical immutable bindings, and -> stands for a lot of things, but ultimately if R then Q, which is not just Modus Ponens, but a Universal single-clause [partial] function, the notion originally captured by the Lambda application.

There is more, of course. Which an expressive enough type-system (as in my F-lang) the ideal of types being theorems and functions on them being proofs (witnesses) becomes a reality, as long as one sticks to the | -> structural duality, which is, arguably, the most fundamental building block (corresponding, not coincidentally, to the Introduction and Eliminations rules).

Even in Rust, the type-state pattern on a parameterised enum is, surprise! an ad-hoc encoding of proper GADTs, and pattern-matching expressions of those (when such an expression is the whole body of a function) is an interpreted (by definition).

Now thinks of the individual enum-clauses being pure declarations of possible (and only) “actions”, and an interpreter that executes them, eventually, behind a monadic abstraction barrier, returning a “pure” result, and wallah, the IO Monad, the State Monad, the Reader Monad, and ultimately, Free Monads and Applicatives (one shouldn’t have their theoretical CS classes missed).

One more time – one not just build a nested expression, which can be “mechanically” evaluated by substitution, with a pen and a paper, instead one builds a universal DAG, which captures and represents this very process of evaluation (eventually, by someone else), while structurally proving (at the compile time) that this DAG is composed properly and will not fail to be evaluated in principle.

How? By composing larger structural elements into the very same “forks, joins and steps”, Introductions, Eliminations and Modus Ponens, by having an Interpreter for a pure DSL of the layer [of abstraction] strictly below.

Ok, let me show you something:

forAll a where
type Expr a =
    | Lit Int                      suchThat (a == Int)
    | Add (Expr Int, Expr Int)     suchThat (a == Int)
    | IsZero (Expr Int)            suchThat (a == Bool)
    | If (Expr Bool, Expr a, Expr a)

-- Clause 1: (Lit Int) -> Int
let eval_lit = (Lit n) -> n

-- Clause 2: (Add) -> Int
let eval_add = (Add (l, r)) -> (eval l) + (eval r)

-- Clause 3: (IsZero) -> Bool
let eval_iszero = (IsZero e) -> (eval e == 0)

-- Clause 4: (If) -> a
let eval_if = (If (cond, t, f)) ->
    | eval cond -> eval t
    | otherwise -> eval f

let eval = eval_lit | eval_add | eval_iszero | eval_if

-- or even better, as in SML, to capture that very structual duality

let eval =
  | (Lit n) -> n
  | (Add (l, r)) -> (eval l) + (eval r)
  | (IsZero e) -> (eval e == 0)
  | (If (cond, t, f)) ->
    | eval cond -> eval t
    | otherwise -> eval f

Notice how many (and which ones) structural elements are out there. There are the “emergent properties”:

• GADTs are indexed coproducts (disjoint unions indexed by a type parameter)
• a DSL is just a sum-type (GADT)m an interpreter is just a pure exhaustive pattern-matching expression
• Interpreters are the only lawful transformations (they are the unique homomorphisms out of the initial algebra / free structure)
• You can have many interpreters (pretty-printer, evaluator, optimizer, logger, HyperLiquid executor, simulator, type-checker, etc.)
• All interpreters automatically commute with each other because they are Natural Transformations
• Each layer exports a pure, stateless declarative DSL
• The layer above consumes that DSL exclusively via an interpreter
• The constructors of the GADT and the pattern-match arms of the interpreter are structural duals (introduction vs elimination)
• The entire stack forms a commuting diagram that never breaks — the universal DAG remains coherent at every level

Nothing of the above is arbitrary or coincidental, due to the fact that the Elephant is, indeed. the one and the same. The Curry-Howard isomorphism is only the beginning.