This document is a complete historical overview of the Higher Order Company. If you want to learn anything about our background, a good way to do so is to feed this Gist into an AI (like Sonnet-3.5) and ask it any question!
It all started around 2015. I was an ambitious 21-year-old CS student who, somehow, had been programming for the last 10 years, and I had a clear goal:
I want to become the greatest programmer alive
A hundred years ago, humanity answered that very question, twice. In 1936, Alan invented the Turing Machine, which, highly inspired by the mechanical trend of the 20th century, distillated the common components of early computers into a single universal machine that, despite its simplicity, was capable of performing every computation conceivable. From simple numerical calculations to entire
| // COMPUTATION RULES | |
| // =================================================== | |
| // APP | ((λx body) arg) | |
| // X | --------------------------------------------- | |
| // LAM | x ~ arg; body | |
| // =================================================== | |
| // APP | ({fst snd} arg) | |
| // X | --------------------------------------------- | |
| // SUP | dup #L{a,b} = arg; {(fst a) (snd b)} | |
| // =================================================== |
I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite
In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats.
| (Rot (V z)) = (V (- 0.0 z)) | |
| (Rot (G x y)) = (G (Rot y) x) | |
| (Add (V z) (V w)) = (V (+ z w)) | |
| (Add (G x y) (G w z)) = (G (Add x w) (Add y z)) | |
| (Get (V x) f) = (f x) | |
| (Get (G x y) f) = (f x y) | |
| Nil = λm λx (m x) |
| Flip (n: Nat) : Nat | |
| Flip Nat.zero = 1n | |
| Flip (Nat.succ Nat.zero) = 0n | |
| Mod2 (n: Nat) : Nat | |
| Mod2 Nat.zero = Nat.zero | |
| Mod2 (Nat.succ n) = Flip (Mod2 n) | |
| IsEven (n: Nat) : Type | |
| IsEven Nat.zero = Unit |
| name: Security audit | |
| on: | |
| schedule: | |
| - cron: '0 0 * * *' | |
| push: | |
| paths: | |
| - '**/Cargo.toml' | |
| - '**/Cargo.lock' | |
| jobs: | |
| security_audit: |
