| author | Alan Dipert
<alan@tailrecursion.com> 2026-07-16 16:10:12 UTC |
| committer | Alan Dipert
<alan@tailrecursion.com> 2026-07-16 16:10:12 UTC |
| parent | 09fa575788ded96aa6186524df7efbcf70dec908 |
| drafts/FLForFiniteDomains.md | +394 | -0 |
diff --git a/drafts/FLForFiniteDomains.md b/drafts/FLForFiniteDomains.md new file mode 100644 index 0000000..f49c075 --- /dev/null +++ b/drafts/FLForFiniteDomains.md @@ -0,0 +1,394 @@ +# FLForFiniteDomains + +John Backus' [Turing Award lecture](https://cacm.acm.org/research/can-programming-be-liberated-from-the-von-neumann-style/) is often read as a broad attack on imperative programming, but the part I keep coming back to is narrower. He thought we were often speaking in the wrong units. We described programs as sequences of named updates when the real content of the problem lived elsewhere: in the structure of the data, and in the algebra of transformations over that structure. + +That does not mean every program wants the same notation. Sometimes the natural object really is a small control graph. Sometimes it is not. I have been thinking about the boundary between those two cases. + +A calculator with a formally specified interface is a useful example because it contains both kinds of thing side by side. + +## The direct case: a reference picker + +Suppose the calculator supports staged reference entry. The user is either not picking a reference, choosing a column, or choosing a row. In one project I have been working on, the canonical machine spec for that logic contains this fragment: + +```json +"refPicker": { + "kind": "fsm", + "states": ["off", "column", "row"], + "events": ["begin", "selectColumn", "rowBackspaceToColumn", "cancel", "commit", "hardReset"], + "transitions": [ + { "from": "*", "event": "hardReset", "to": "off" }, + { "from": "off", "event": "begin", "to": "column" }, + { "from": "column", "event": "begin", "to": "column" }, + { "from": "column", "event": "selectColumn", "to": "row" }, + { "from": "row", "event": "rowBackspaceToColumn", "to": "column" }, + { "from": "column", "event": "cancel", "to": "off" }, + { "from": "row", "event": "cancel", "to": "off" }, + { "from": "row", "event": "commit", "to": "off" } + ] +} +``` + +That JSON is already fairly close to the underlying mathematical object, which is just a sparse transition relation over a tiny product domain. The same machine can be written more readably as a table: + +```text +refPicker + +event off column row +------------------------------------------------ +begin column column - +selectColumn - row - +rowBackspaceToColumn - - column +cancel - off off +commit - - off +hardReset off off off +``` + +`-` means invalid. + +This table is already nearly ideal. You can read it across rows if you care about the meaning of an event everywhere. You can read it down columns if you care about what is legal in a given phase. The wildcard `hardReset` is obvious. The self-loop on `column` under `begin` is obvious. The fact that `commit` is only legal from `row` is obvious. + +If I want a more algebraic view, I can still have one. The table determines a partial transition function + +```text +delta : State x Event -> State + Invalid +``` + +or, if I insist on totality, a total function into an explicit result domain: + +```text +delta : State x Event -> Result + +Result = ok State | invalid +``` + +and now the same machine can be factored as a small program built from simpler handlers: + +```text +delta = + resetOverride o byState + +resetOverride (s, e) = + if e = hardReset then ok off else byState (s, e) + +byState = + case on first projection of + off -> offStep + column -> columnStep + row -> rowStep + +offStep (_, e) = + if e = begin then ok column else invalid + +columnStep (_, e) = + if e = begin then ok column + else if e = selectColumn then ok row + else if e = cancel then ok off + else invalid + +rowStep (_, e) = + if e = rowBackspaceToColumn then ok column + else if e = cancel then ok off + else if e = commit then ok off + else invalid +``` + +Now the machine has been expressed in a function-level way. There is an override combinator for the wildcard reset rule, a decomposition by state, and local handlers for each state. That is a perfectly respectable algebraic presentation. + +But it is also a useful demonstration of a limit. The FL treatment does not really compress this machine very much. The wildcard reset factors out nicely, and the partition by source state is clean, but after that the remaining information is still just the sparse relation itself. There is no larger family of similar transformations to absorb into a more interesting normal form. + +That is why I would say the table is the natural normal form for `refPicker`. The algebra can represent it, but the algebra does not reveal some deeper structure that the table was hiding. The thing is already as simple as it looks. + +That is not a disappointment. It tells us something important. + +## What the machine teaches + +The `refPicker` example draws a boundary. + +Some parts of a program are genuinely about phase and legality. They are about which events are admitted from which states, and what the control graph looks like. For those parts, [statecharts](https://weizmann.elsevierpure.com/en/publications/statecharts-a-visual-formalism-for-complex-systems/), hierarchical state machines, and plain old transition tables are exactly the right abstraction. + +Backus did not argue that every good program should look the same. He argued that the representation should reflect the real structure of the problem. In the `refPicker` case, the real structure is already a tiny relation over named phases. There is not much redundancy to remove. The machine is already near its own normal form. + +So the interesting question is not “how do I force this machine into FL?” The interesting question is “what happens when the thing being modeled is no longer mainly a phase graph?” + +## Where charts start to strain + +Take a different part of the same calculator: the grid point or cursor. Suppose the calculator has 6 columns, 64 rows, and one distinguished point marking the next write location. + +This domain is finite, but it does not feel like `refPicker`. The interesting object is no longer a handful of named phases. It is a structured finite space. + +That difference matters. A tiny control graph wants to be described extensionally: here are the states, here are the events, here are the legal pairs. A grid point wants to be described intensionally: here is the space, here are its axes, here are the transformations that act on those axes. + +If I insist on a chart-first view, several bad options appear. I can enumerate too many concrete states. I can leave the chart small but move the real semantics into side variables and guard logic. Or I can stop pretending and write ordinary integer code with boundary checks scattered through it. + +All three options lose something. + +The first loses compression. A 6 x 64 grid has 384 concrete positions. Once I start flattening the point into named machine states, the model size starts scaling with the size of the space rather than with the structure of the space. + +The second loses semantic center of gravity. The chart remains small, but the real meaning migrates into guards, helper functions, and arithmetic done elsewhere. The machine still exists, but it is no longer carrying the main burden. + +The third loses formal shape almost entirely. I still have the behavior, but now it is expressed as plain index arithmetic with edge checks. The program may work, but the structure of the domain is no longer obvious in the structure of the program. + +This is where finite-domain structure becomes the real issue. The problem is not simply that the space is large. A 384-element set is not large. The problem is that it is not an undifferentiated set. It is a product of two bounded axes, and the useful transformations respect that product structure. + +This is where I think the limits of HSMs show up. They compress repeated control structure very well. They do not, by themselves, give me much leverage over bounded coordinate spaces. They can mention those spaces, but they do not make them algebraically clean. + +That asymmetry explains something common in real systems. The mode logic is often deeply and cleanly formalized. The coordinate logic is often less fully encapsulated. This is not necessarily because the second part matters less. It is because the chart formalism has more leverage on the first part than on the second. + +## Backus' idea, applied narrowly + +This is where I think Backus becomes useful again. + +The point is not that I should reach first for theorem proving, or even first for a type discipline. The point is that I should look for the algebra of the domain and write the program in those terms. + +Backus' [lecture](https://cacm.acm.org/research/can-programming-be-liberated-from-the-von-neumann-style/) complains about the “word-at-a-time” style and the tight coupling of semantics to state transitions. His remedy is a style based on combining forms. [The FL project](https://theory.stanford.edu/~aiken/publications/trs/FLProject.pdf) and the [FL manual](https://theory.stanford.edu/~aiken/publications/trs/RJ7100.pdf) turn that into a more practical language story. The lasting idea is that a program should be assembled from transformations that match the structure of the domain, not from a pile of unrelated update steps. + +For the grid point, the first thing I want is not a movement routine. It is the shape of the space. + +```text +shape Grid = + { rows : Nat + , cols : Nat + } + +grid = + { rows = 64 + , cols = 6 + } +``` + +From that I derive the position space: + +```text +type Row = Fin grid.rows +type Col = Fin grid.cols + +type Point = + { row : Row + , col : Col + } +``` + +The crucial thing here is not the surface notation. It is that the domain is described structurally. A point is not an integer that happens to be interpreted as a coordinate. It is the product of a row domain and a column domain. + +This is the finite-domain move that actually matters. The constants are no longer floating around in the motion logic as stray arithmetic facts. They have been absorbed into the description of the space itself. `64` and `6` appear once, in the shape. Everything downstream is stated in terms of rows, columns, and their product. + +That description does some work before any movement function has been written. The point space is already closed. Illegal rows and columns are not something to rule out later. They are outside the described world from the beginning. + +It also changes what counts as a good program. In the chart view, a good program is one that lists the correct transitions. In the finite-domain view, a good program is one whose operations are natural endomorphisms of the space. That is a very Backus-like shift: away from enumerating cases and toward choosing the right family of transformations. + +A fuller FL-esque implementation of the grid-point behavior looks like this: + +```text +module GridPoint + +shape Grid = + { rows : Nat + , cols : Nat + } + +grid : Grid +grid = + { rows = 64 + , cols = 6 + } + +type Row = Fin grid.rows +type Col = Fin grid.cols + +type Point = + { row : Row + , col : Col + } + +type Move = + Up + | Down + | Left + | Right + | EnterAdvance + +succSat : Fin n -> Fin n +predSat : Fin n -> Fin n + +first : (a -> b) -> { fst : a, snd : c } -> { fst : b, snd : c } +second : (c -> d) -> { fst : a, snd : c } -> { fst : a, snd : d } + +compose : (b -> c) -> (a -> b) -> a -> c +id : a -> a + +pairToPoint : { fst : Row, snd : Col } -> Point +pairToPoint p = + { row = p.fst, col = p.snd } + +pointToPair : Point -> { fst : Row, snd : Col } +pointToPair p = + { fst = p.row, snd = p.col } + +mapPoint : (Row -> Row) -> (Col -> Col) -> Point -> Point +mapPoint f g = + compose + pairToPoint + (compose + (second g) + (compose + (first f) + pointToPair)) + +onRow : (Row -> Row) -> Point -> Point +onRow f = + mapPoint f id + +onCol : (Col -> Col) -> Point -> Point +onCol g = + mapPoint id g + +up : Point -> Point +up = + onRow predSat + +down : Point -> Point +down = + onRow succSat + +left : Point -> Point +left = + onCol predSat + +right : Point -> Point +right = + onCol succSat + +isLastCol : Col -> Bool +isLastCol + +isLastRow : Row -> Bool +isLastRow + +zeroCol : Col +zeroCol + +advance : Point -> Point +advance p = + if isLastCol p.col then + if isLastRow p.row then + p + else + { row = succSat p.row, col = zeroCol } + else + right p + +move : Move -> Point -> Point +move m = + case m of + Up -> up + Down -> down + Left -> left + Right -> right + EnterAdvance -> advance +``` + +The syntax is modernized, but the intended reading is Backus-like. The program is assembled from a small stock of structurally meaningful transformations and combining forms. `first`, `second`, and `compose` are doing the function-level work. `mapPoint`, `onRow`, and `onCol` are not conveniences pasted on top of an imperative core. They are the program. + +## A small algebra of motions + +Now I want transformations that respect this structure. + +Start with local endomorphisms on the axes: + +```text +succSat : Fin n -> Fin n +predSat : Fin n -> Fin n +``` + +These are saturated successor and predecessor. The important fact is not how they are implemented. The important fact is that they are endomorphisms of a bounded domain. + +Then add combining forms that lift local transformations to the point product: + +```text +mapPoint : (Row -> Row) -> (Col -> Col) -> Point -> Point +onRow : (Row -> Row) -> Point -> Point +onCol : (Col -> Col) -> Point -> Point +``` + +At this point the primitive motions become tiny expressions: + +```text +up = onRow predSat +down = onRow succSat +left = onCol predSat +right = onCol succSat +``` + +This is the place where the FL view earns its keep. The motions are not a family of separate ad hoc procedures anymore. They are instances of a small algebra: axis-local endomorphisms lifted over a product. + +That is more than a pleasing notation change. It changes what is explicit in the program. + +`up` is visibly a row-only transformation. `left` is visibly a column-only transformation. All four motions are visibly endomorphisms of the point space. The structure of the program says what sort of thing each motion is. + +It is worth dwelling on that, because this is where finite domain really bites. If I had modeled the point as a single flat index and then written four little arithmetic procedures, I would still have a correct program. But I would have lost the factorization. I would no longer be able to say, at the level of program form, that `up` and `down` are one family and `left` and `right` are another. I would have erased the product structure and then simulated it again with arithmetic. + +In Backus' terms, that would be a step backward. The interesting algebra is not “add one, subtract one, add six, subtract six.” The interesting algebra is “act on the row coordinate,” “act on the column coordinate,” and “lift those actions to the product.” The point of the finite-domain presentation is that it preserves exactly that distinction. + +## The right kind of normal form + +Here there is a normal form that did not exist for `refPicker`. + +For `refPicker`, the table was already the normal form because the remaining information was just the sparse relation itself. + +For the grid point, the normal form is not a big table of concrete positions. It is the algebraic factorization: + +- describe the domain as a product, +- choose local endomorphisms on the factors, +- lift them with combining forms, +- build larger motions from those lifted pieces. + +That is a real compression. The code does not scale with the number of positions. It scales with the structural vocabulary of the domain. + +This is what I mean by saying that finite domain demands expansion. Once the domain is a product space, the main intellectual work is no longer listing cases. It is finding the right factorization of the operators. The algebra needs more explanation because the payoff is there, not in the mere fact that the domain is finite. + +If the grid becomes larger, the program does not have to grow proportionally. If the row and column domains are still the same kind of thing, the same algebra still applies. That is precisely the sort of nonrepetitive construction Backus was asking for. + +## What becomes visible by construction + +The attraction of this style is often described in the language of proofs, but I think that can be misleading. + +Of course one can later prove things about these programs, and systems like [Coq](https://coq.inria.fr/documentation), [Lean](https://lean-lang.org/learn/), [Agda](https://agda.readthedocs.io/), or [Idris](https://www.idris-lang.org/pages/documentation.html) are useful when explicit proof is the point. But that is not the main thing I am after. + +The main thing is that the program already advertises some of its important properties. + +If `up = onRow predSat`, then `up` is visibly row-local. If `right = onCol succSat`, then `right` is visibly column-local. If all these motions are endomorphisms of `Point`, then staying in the point space is part of what they are, not a condition to be checked after the fact. + +Backus' emphasis on the algebra of programs matters here. A good algebra does not merely make proofs possible. It makes the semantic shape of the program easier to see. + +## Next to HSMs, not against them + +Nothing in this argument displaces machines where machines belong. + +I still want a chart for interaction modes, file workflow, staged reference entry, pane switching, and any other part of the system whose main content is control phase and admissible events. The machine representation is already doing its job there. + +What I want is a better division of labor. + +Let control graphs be described as control graphs. Let bounded structured spaces be described as bounded structured spaces. Let the program algebra match the kind of object being modeled. + +In that arrangement, HSMs and FL-style modeling are not rivals. They are solving different compression problems. + +## The narrow claim + +My claim is narrow. + +A small reference picker should remain a machine. Its best human form is a sparse transition table, and its best algebraic factoring is only a light restatement of that table. + +A grid point should not be flattened into the same kind of object. Once the real content of the feature is a bounded structured space rather than a tiny phase graph, function-level ideas start to help. The domain comes first. The transformations are chosen as endomorphisms of that domain. Combining forms lift and assemble them. The resulting program has a normal form that reflects the structure of the space rather than the enumeration of its cases. + +That seems to me like a real use of Backus' idea in ordinary software design: not as nostalgia, and not as a demand to rewrite everything in historical FL syntax, but as a way to notice when a problem has stopped wanting to be a chart and started wanting to be an algebra. + +## References + +- John Backus, [Can Programming Be Liberated from the von Neumann Style?](https://cacm.acm.org/research/can-programming-be-liberated-from-the-von-neumann-style/) +- Alexander Aiken, John H. Williams, Edward L. Wimmers, [The FL Project: Design of a Functional Language](https://theory.stanford.edu/~aiken/publications/trs/FLProject.pdf) +- Backus, Williams, Wimmers, Lucas, Aiken, [FL Language Manual, Parts 1 and 2](https://theory.stanford.edu/~aiken/publications/trs/RJ7100.pdf) +- David Harel, [Statecharts: A Visual Formalism for Complex Systems](https://weizmann.elsevierpure.com/en/publications/statecharts-a-visual-formalism-for-complex-systems/) +- [The Coq Proof Assistant documentation](https://coq.inria.fr/documentation) +- [Lean documentation](https://lean-lang.org/learn/) +- [Agda documentation](https://agda.readthedocs.io/) +- [Idris 2 documentation](https://www.idris-lang.org/pages/documentation.html)