Kina.ai

Specification

AI-Native Programming Language: Design Space Series

A six-memo research program exploring the design of an AI-native programming language from a compiler-engineering point of view. The premise: Python's role in ML is bolted-on rather than native, and the components for a genuinely AI-native language exist in research literature but have not been integrated.

The memos

  1. Static vs Dynamic Shapes — The spectrum from NumPy's runtime shapes through JAX's tracing, PyTorch 2's symbolic shapes, Hasktorch's static annotations, to Dex's full dependent types. Thesis: symbolic shapes are where the real design work lives.

  2. Differentiation Through Effects — Reverse-mode AD over pure functions is solved; AD over effectful programs is six different special cases in current systems. Thesis: algebraic effect handlers are the natural unifying framework, and the Random effect's handler is the gradient estimator.

  3. Compositional Sparsity and Structured Tensors — Sparsity is fragmented across storage formats (TACO), hardware-imposed patterns (Ampere 2:4), low-rank factorization (LoRA), and dynamic routing (MoE). Thesis: sparsity should be a refinement on the tensor type, with composition rules that allow widening when structure is lost.

  4. Distributed Programming Model — Sharding is currently process-rank programming with a Python wrapper. Thesis: GSPMD is a type inferencer in disguise; auto-parallelization is constraint solving over the type system; the device mesh is a kind.

  5. Verification — ML compilers do enormous semantic transformations and most have no proofs. Tractable verification targets exist (verified sharding, verified AD over effects, verified sparse codegen). Thesis: ML compiler verification is about a decade behind traditional compiler verification; the missing pieces are bounded research projects, not open theoretical questions.

  6. Hardware Abstraction — Modern AI hardware is a zoo, and the abstraction problem is combinatorial. Thesis: hardware capabilities are a refinement axis on the tensor type; portability is parametric over capability sets; lowering is capability matching. Final cross-memo synthesis appears at the end of this memo.

The thesis, in one paragraph

The "tensor" in an AI-native language is a type with five orthogonal refinement axes — shape, effects, structure, sharding, and hardware capability. Operations compose along all five axes. The compiler infers result-type refinements from operand-type refinements; mismatches at operation boundaries are either type errors or compiler-inserted coercions. Verification is stratified by weight: refinement types at the surface, Verus-style verification for the runtime, Coq/Lean for the high-stakes compiler passes, translation validation during development. The architecture is multi-tier — an algebraic surface language, a typed tensor IR, a capability-typed tile IR, target-specific dialects — wired through MLIR-style lowering. None of the pieces are new; the integration is the contribution.

What kind of document this is

These are research design memos, not a language specification. They sketch a coherent program of research, identify which sub-problems are tractable (1–2 years of work) versus hard (multi-year programs) versus genuinely open, and connect to existing literature where the pieces have been done. They are intentionally opinionated — the unified-type-system thesis is a claim, not a survey conclusion — and the memos are written so that disagreement is possible at specific points rather than only at the level of "I don't buy it."

Reference quality

References are paraphrased from the writer's working knowledge. Major citations (Pearlmutter & Siskind, CompCert, GSPMD, TACO, Brunel/Mazza/Pagani, Triton, MLIR, etc.) are confident. Some specific years/venues for more recent papers may need verification before any external citation. A web-search verification pass would take an hour or two and produce a clean reference list.

Suggested reading order

For a first pass: 1 → 2 → 4 → 6, then 3 and 5 as supporting depth. Memos 1, 2, 4, 6 establish the type-system framework; memo 3 stress-tests it on the structure axis; memo 5 grounds it in a verification methodology.

For a research-program-planning pass: read in order. The cross-memo synthesis sections in memos 4, 5, and 6 explicitly track how the framework holds together as it accumulates dimensions.

For someone deciding whether any of this is worth pursuing as actual research: skip to memo 5 §6 (verified sharding propagation) and memo 6 §11 (hardware capability typing). Those are the two most concrete, most underexploited targets in the series.