1  <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 1920 1400">
  2    <defs>
  3      <pattern id="grid" width="64" height="64" patternUnits="userSpaceOnUse">
  4        <path d="M 64 0 L 0 0 0 64" fill="none" stroke="#596775" stroke-width="0.5" opacity="0.15"/>
  5      </pattern>
  6      <marker id="arrow" markerWidth="10" markerHeight="10" refX="9" refY="3" orient="auto">
  7        <path d="M0,0 L0,6 L9,3 z" fill="#54aeff"/>
  8      </marker>
  9      <marker id="arrowGray" markerWidth="10" markerHeight="10" refX="9" refY="3" orient="auto">
 10        <path d="M0,0 L0,6 L9,3 z" fill="#596775"/>
 11      </marker>
 12      <linearGradient id="cubeGrad" x1="0%" y1="0%" x2="100%" y2="100%">
 13        <stop offset="0%" stop-color="#54aeff" stop-opacity="0.3"/>
 14        <stop offset="100%" stop-color="#111417" stop-opacity="0"/>
 15      </linearGradient>
 16    </defs>
 17    
 18    <rect width="1920" height="1400" fill="#111417"/>
 19    <rect width="1920" height="1400" fill="url(#grid)"/>
 20    
 21    <!-- Title -->
 22    <text x="960" y="60" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="48" font-weight="600" fill="#80ccff">The Lambda Hierarchy</text>
 23    <text x="960" y="100" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="20" fill="#596775">From Untyped to CIC · A Map of Type-Theoretic Foundations</text>
 24    
 25    <!-- Lambda Cube Legend -->
 26    <g transform="translate(1500, 130)">
 27      <rect x="0" y="0" width="380" height="130" rx="6" fill="#111417" stroke="#596775" stroke-width="1"/>
 28      <text x="190" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#80ccff">Barendregt's Lambda Cube</text>
 29      <text x="15" y="50" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#54aeff">λ2</text>
 30      <text x="45" y="50" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Terms → Types (polymorphism)</text>
 31      <text x="15" y="70" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#80ccff">λω</text>
 32      <text x="45" y="70" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Types → Types (type operators)</text>
 33      <text x="15" y="90" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#b6e3ff">λΠ</text>
 34      <text x="45" y="90" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Terms → Types (dependent types)</text>
 35      <text x="15" y="115" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">CoC = λ2 + λω + λΠ (all three)</text>
 36    </g>
 37  
 38    <!-- TIER 0: Untyped -->
 39    <g transform="translate(100, 160)">
 40      <rect x="0" y="0" width="1300" height="120" rx="8" fill="#111417" stroke="#596775" stroke-width="2"/>
 41      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="24" fill="#596775">Untyped Lambda Calculus</text>
 42      <text x="30" y="60" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#596775">λx.M | M N | x — No static type checking, everything is a function</text>
 43      
 44      <g transform="translate(30, 75)">
 45        <rect x="0" y="0" width="90" height="30" rx="4" fill="#111417" stroke="#596775"/>
 46        <text x="45" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Scheme</text>
 47      </g>
 48      <g transform="translate(130, 75)">
 49        <rect x="0" y="0" width="70" height="30" rx="4" fill="#111417" stroke="#596775"/>
 50        <text x="35" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Lisp</text>
 51      </g>
 52      <g transform="translate(210, 75)">
 53        <rect x="0" y="0" width="80" height="30" rx="4" fill="#111417" stroke="#596775"/>
 54        <text x="40" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Erlang</text>
 55      </g>
 56      <g transform="translate(300, 75)">
 57        <rect x="0" y="0" width="80" height="30" rx="4" fill="#111417" stroke="#596775"/>
 58        <text x="40" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Python</text>
 59      </g>
 60      <g transform="translate(390, 75)">
 61        <rect x="0" y="0" width="60" height="30" rx="4" fill="#111417" stroke="#596775"/>
 62        <text x="30" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Ruby</text>
 63      </g>
 64      <g transform="translate(460, 75)">
 65        <rect x="0" y="0" width="40" height="30" rx="4" fill="#111417" stroke="#596775"/>
 66        <text x="20" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">JS</text>
 67      </g>
 68      <g transform="translate(510, 75)">
 69        <rect x="0" y="0" width="60" height="30" rx="4" fill="#111417" stroke="#596775"/>
 70        <text x="30" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Bash</text>
 71      </g>
 72      
 73      <text x="650" y="100" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775" font-style="italic">Runtime dynamism. Types are lies we tell at 3am.</text>
 74    </g>
 75    
 76    <!-- Arrow up -->
 77    <line x1="750" y1="280" x2="750" y2="310" stroke="#596775" stroke-width="2" marker-end="url(#arrowGray)"/>
 78    
 79    <!-- TIER 1: STLC -->
 80    <g transform="translate(100, 320)">
 81      <rect x="0" y="0" width="1300" height="120" rx="8" fill="#111417" stroke="#54aeff" stroke-width="2"/>
 82      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="24" fill="#54aeff">Simply Typed Lambda Calculus (STLC)</text>
 83      <text x="30" y="60" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#596775">τ ::= α | τ → τ — Base types and function types. No polymorphism.</text>
 84      
 85      <g transform="translate(30, 75)">
 86        <rect x="0" y="0" width="120" height="30" rx="4" fill="#111417" stroke="#54aeff"/>
 87        <text x="60" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#54aeff">Go (pre-1.18)</text>
 88      </g>
 89      <g transform="translate(160, 75)">
 90        <rect x="0" y="0" width="50" height="30" rx="4" fill="#111417" stroke="#54aeff"/>
 91        <text x="25" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#54aeff">C</text>
 92      </g>
 93      <g transform="translate(220, 75)">
 94        <rect x="0" y="0" width="60" height="30" rx="4" fill="#111417" stroke="#54aeff"/>
 95        <text x="30" y="20" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#54aeff">Pascal</text>
 96      </g>
 97      
 98      <text x="350" y="100" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775" font-style="italic">Types exist. Copy-paste reigns supreme.</text>
 99    </g>
100    
101    <!-- Arrow up -->
102    <line x1="750" y1="440" x2="750" y2="470" stroke="#54aeff" stroke-width="2" marker-end="url(#arrow)"/>
103    
104    <!-- TIER 2: System F -->
105    <g transform="translate(100, 480)">
106      <rect x="0" y="0" width="1300" height="160" rx="8" fill="#111417" stroke="#54aeff" stroke-width="3"/>
107      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="24" fill="#54aeff">System F (λ2) — Polymorphic Lambda Calculus</text>
108      <text x="30" y="60" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#b6e3ff">∀α. α → α — Universal quantification over types. Parametric polymorphism.</text>
109      
110      <!-- Straylight languages -->
111      <g transform="translate(30, 80)">
112        <rect x="0" y="0" width="80" height="35" rx="4" fill="#0d1012" stroke="#54aeff" stroke-width="2"/>
113        <text x="40" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#54aeff">Rust</text>
114      </g>
115      <g transform="translate(120, 80)">
116        <rect x="0" y="0" width="120" height="35" rx="4" fill="#0d1012" stroke="#54aeff" stroke-width="2"/>
117        <text x="60" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#54aeff">TypeScript</text>
118      </g>
119      <g transform="translate(250, 80)">
120        <rect x="0" y="0" width="80" height="35" rx="4" fill="#0d1012" stroke="#54aeff" stroke-width="2"/>
121        <text x="40" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#54aeff">C++</text>
122      </g>
123      
124      <!-- Other System F languages -->
125      <g transform="translate(360, 80)">
126        <rect x="0" y="0" width="60" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
127        <text x="30" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Go</text>
128      </g>
129      <g transform="translate(430, 80)">
130        <rect x="0" y="0" width="70" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
131        <text x="35" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Java</text>
132      </g>
133      <g transform="translate(510, 80)">
134        <rect x="0" y="0" width="80" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
135        <text x="40" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Kotlin</text>
136      </g>
137      <g transform="translate(600, 80)">
138        <rect x="0" y="0" width="70" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
139        <text x="35" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Swift</text>
140      </g>
141      <g transform="translate(680, 80)">
142        <rect x="0" y="0" width="55" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
143        <text x="27" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">C#</text>
144      </g>
145      <g transform="translate(745, 80)">
146        <rect x="0" y="0" width="55" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
147        <text x="27" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">F#</text>
148      </g>
149      <g transform="translate(810, 80)">
150        <rect x="0" y="0" width="55" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
151        <text x="27" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Zig</text>
152      </g>
153      
154      <!-- Special: Elm -->
155      <g transform="translate(900, 80)">
156        <rect x="0" y="0" width="55" height="35" rx="4" fill="#111417" stroke="#7ec699"/>
157        <text x="27" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#7ec699">Elm</text>
158      </g>
159      
160      <text x="30" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775" font-style="italic">Generics. The industrial workhorse tier. Most production code lives here.</text>
161      <text x="730" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#7ec699">Elm: System F with no escape hatches. "If it compiles, it works."</text>
162    </g>
163    
164    <!-- Branch into two paths -->
165    <line x1="500" y1="640" x2="500" y2="680" stroke="#54aeff" stroke-width="2"/>
166    <line x1="1000" y1="640" x2="1000" y2="680" stroke="#80ccff" stroke-width="2"/>
167    
168    <!-- TIER 3a: System Fω (left branch) -->
169    <g transform="translate(100, 690)">
170      <rect x="0" y="0" width="600" height="160" rx="8" fill="#111417" stroke="#80ccff" stroke-width="2"/>
171      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="22" fill="#80ccff">System Fω — Type Operators</text>
172      <text x="30" y="58" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#b6e3ff">List : Type → Type — Higher-kinded types</text>
173      
174      <!-- Straylight -->
175      <g transform="translate(30, 75)">
176        <rect x="0" y="0" width="100" height="35" rx="4" fill="#0d1012" stroke="#80ccff" stroke-width="2"/>
177        <text x="50" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Haskell</text>
178      </g>
179      
180      <!-- Others -->
181      <g transform="translate(140, 75)">
182        <rect x="0" y="0" width="80" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
183        <text x="40" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">OCaml</text>
184      </g>
185      <g transform="translate(230, 75)">
186        <rect x="0" y="0" width="80" height="35" rx="4" fill="#111417" stroke="#80ccff"/>
187        <text x="40" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#80ccff">Scala 3</text>
188      </g>
189      <g transform="translate(320, 75)">
190        <rect x="0" y="0" width="110" height="35" rx="4" fill="#111417" stroke="#d19a66"/>
191        <text x="55" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#d19a66">PureScript</text>
192      </g>
193      
194      <text x="30" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775" font-style="italic">Functor, Monad, Applicative. The type-level DSL tier.</text>
195    </g>
196    
197    <!-- TIER 3b: LF/λΠ (right branch) -->
198    <g transform="translate(800, 690)">
199      <rect x="0" y="0" width="600" height="160" rx="8" fill="#111417" stroke="#b6e3ff" stroke-width="2"/>
200      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="22" fill="#b6e3ff">LF (λΠ) — Dependent Functions</text>
201      <text x="30" y="58" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#b6e3ff">Πn:Nat. Vec n — Types indexed by terms</text>
202      
203      <g transform="translate(30, 75)">
204        <rect x="0" y="0" width="70" height="35" rx="4" fill="#111417" stroke="#b6e3ff"/>
205        <text x="35" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#b6e3ff">Twelf</text>
206      </g>
207      <g transform="translate(110, 75)">
208        <rect x="0" y="0" width="80" height="35" rx="4" fill="#111417" stroke="#b6e3ff"/>
209        <text x="40" y="22" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#b6e3ff">Beluga</text>
210      </g>
211      
212      <text x="30" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775" font-style="italic">Metatheory. Proofs about proofs. The logical framework.</text>
213    </g>
214    
215    <!-- Converge arrows -->
216    <line x1="400" y1="850" x2="400" y2="890" stroke="#80ccff" stroke-width="2"/>
217    <line x1="1100" y1="850" x2="1100" y2="890" stroke="#b6e3ff" stroke-width="2"/>
218    <line x1="400" y1="890" x2="750" y2="890" stroke="#80ccff" stroke-width="2"/>
219    <line x1="1100" y1="890" x2="750" y2="890" stroke="#b6e3ff" stroke-width="2"/>
220    <line x1="750" y1="890" x2="750" y2="920" stroke="#54aeff" stroke-width="2" marker-end="url(#arrow)"/>
221    
222    <!-- TIER 4: CoC -->
223    <g transform="translate(100, 930)">
224      <rect x="0" y="0" width="1300" height="100" rx="8" fill="#111417" stroke="url(#cubeGrad)" stroke-width="3"/>
225      <rect x="0" y="0" width="1300" height="100" rx="8" fill="none" stroke="#54aeff" stroke-width="2"/>
226      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="22" fill="#54aeff">Calculus of Constructions (CoC)</text>
227      <text x="30" y="60" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="13" fill="#b6e3ff">λ2 + λω + λΠ — All three axes of the Lambda Cube. Propositions-as-types.</text>
228      
229      <text x="30" y="85" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775" font-style="italic">Foundational. The Curry-Howard apex. No inhabitants yet.</text>
230    </g>
231    
232    <!-- Arrow up -->
233    <line x1="750" y1="1030" x2="750" y2="1060" stroke="#54aeff" stroke-width="2" marker-end="url(#arrow)"/>
234    
235    <!-- TIER 5: CIC -->
236    <g transform="translate(100, 1070)">
237      <rect x="0" y="0" width="1300" height="180" rx="8" fill="#111417" stroke="#54aeff" stroke-width="3"/>
238      <text x="30" y="35" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="24" fill="#54aeff">Calculus of Inductive Constructions (CIC)</text>
239      <text x="30" y="60" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#b6e3ff">CoC + Inductive Types + Universe Hierarchy — The proof assistant foundation</text>
240      
241      <g transform="translate(30, 80)">
242        <rect x="0" y="0" width="120" height="40" rx="4" fill="#0d1012" stroke="#54aeff" stroke-width="2"/>
243        <text x="60" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#54aeff">Coq/Rocq</text>
244      </g>
245      <g transform="translate(160, 80)">
246        <rect x="0" y="0" width="100" height="40" rx="4" fill="#0d1012" stroke="#54aeff" stroke-width="2"/>
247        <text x="50" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#54aeff">Lean 4</text>
248      </g>
249      <g transform="translate(270, 80)">
250        <rect x="0" y="0" width="80" height="40" rx="4" fill="#111417" stroke="#80ccff"/>
251        <text x="40" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#80ccff">Agda</text>
252      </g>
253      <g transform="translate(360, 80)">
254        <rect x="0" y="0" width="90" height="40" rx="4" fill="#111417" stroke="#80ccff"/>
255        <text x="45" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#80ccff">Idris 2</text>
256      </g>
257      
258      <text x="30" y="160" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775" font-style="italic">"Programs are proofs. Types are theorems. Compilation is verification."</text>
259      <text x="750" y="160" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#54aeff">The shape_pos : shape > 0 proof obligation lives here.</text>
260    </g>
261    
262    <!-- Side note: Nix -->
263    <g transform="translate(1500, 690)">
264      <rect x="0" y="0" width="380" height="160" rx="8" fill="#111417" stroke="#7ec699" stroke-width="2"/>
265      <text x="190" y="30" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="18" fill="#7ec699">Straylight Outlier: Nix</text>
266      <text x="20" y="55" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Lazy, pure, functional DSL</text>
267      <text x="20" y="75" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Untyped at its core (dynamic)</text>
268      <text x="20" y="95" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">But: derivations are pure functions</text>
269      <text x="20" y="115" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">Reproducibility by construction</text>
270      <text x="20" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#7ec699" font-style="italic">The build system as theorem prover.</text>
271    </g>
272    
273    <!-- PureScript vs Elm note -->
274    <g transform="translate(1500, 870)">
275      <rect x="0" y="0" width="380" height="140" rx="8" fill="#111417" stroke="#d19a66" stroke-width="1" stroke-dasharray="5,3"/>
276      <text x="190" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="16" fill="#d19a66">PureScript vs Elm</text>
277      <text x="20" y="50" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#d19a66">PureScript:</text>
278      <text x="100" y="50" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">Full Fω, HKT, type classes</text>
279      <text x="100" y="65" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">FFI escape hatch, row types</text>
280      <text x="20" y="90" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#7ec699">Elm:</text>
281      <text x="100" y="90" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">Intentionally System F only</text>
282      <text x="100" y="105" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">No type classes, no HKT, no FFI</text>
283      <text x="20" y="130" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="10" fill="#596775" font-style="italic">Simplicity vs power. The eternal trade.</text>
284    </g>
285    
286    <!-- Practical notes box -->
287    <g transform="translate(1500, 1030)">
288      <rect x="0" y="0" width="380" height="220" rx="8" fill="#111417" stroke="#596775" stroke-width="1"/>
289      <text x="190" y="25" text-anchor="middle" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="16" fill="#80ccff">Practical Reality</text>
290      
291      <text x="20" y="55" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#54aeff">Rust:</text>
292      <text x="70" y="55" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">System F + affine types (ownership)</text>
293      
294      <text x="20" y="80" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#54aeff">TypeScript:</text>
295      <text x="110" y="80" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">Unsound. Gradual typing.</text>
296      
297      <text x="20" y="105" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#54aeff">Haskell:</text>
298      <text x="90" y="105" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">Fω + GADTs + DataKinds</text>
299      <text x="90" y="120" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">(creeping toward dependent types)</text>
300      
301      <text x="20" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#54aeff">C++:</text>
302      <text x="60" y="145" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">Templates are Turing-complete</text>
303      <text x="60" y="160" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">(accidental type-level programming)</text>
304      
305      <text x="20" y="185" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#54aeff">Zig:</text>
306      <text x="60" y="185" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">comptime ≈ dependent types</text>
307      <text x="60" y="200" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="11" fill="#596775">(without the formalism)</text>
308    </g>
309    
310    <!-- Footer -->
311    <text x="100" y="1360" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#596775">"Villa Straylight was a body grown in upon itself. Each space in some way secret, with a morbid grandiosity."</text>
312    <text x="100" y="1380" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="12" fill="#596775">— Types are the rectilinear chambers. The question is how deep you can go.</text>
313    
314    <text x="1870" y="1370" text-anchor="end" font-family="Berkeley Mono, SF Mono, Consolas, monospace" font-size="14" fill="#596775" opacity="0.6">razorgirl · λ-hierarchy · 2026</text>
315  </svg>