Language Inspirations and Target Matrix

A practical research note for the AI-native language design.

Goal: identify existing languages/systems that should inform this project's data types, primitive set, effect model, and multi-target compilation strategy.

This note is intentionally actionable: each source language maps to concrete design decisions, not just references.

1) Design constraints from this project

From Phase 0 + forward tracks, the language needs to satisfy all of these at once:

1. Tensor-first static typing with shape/refinement constraints and SMT discharge.
2. Explicit, optimizable core IR (small primitive set, predictable lowering).
3. Self-modeling trajectory (transformations like AD/sharding increasingly expressed in-language, not ad hoc compiler internals).
4. Multi-target lowering (CPU, NVIDIA CUDA, later AMD/TPU/dataflow targets).
5. Verification path (Lean-friendly formal core, proof-relevant semantics).

Any borrowed design must be evaluated against those five constraints.

2) Languages/systems worth borrowing from

A. Dex

Why relevant

• Closest "typed tensor language" precedent.
• Strong treatment of index-space semantics and array programming in a typed setting.

Borrow

• Tensor-as-indexed-function mental model.
• Compact core calculus for array ops.
• Shape-polymorphic style where useful, while keeping decidable checking.

Caution

• Keep your stricter explicitness where it helps lowering/verification.
• Avoid importing complexity that hurts OCaml implementation velocity in Phase 1.

B. Futhark

Why relevant

• Mature example of a small functional array language compiled to high-performance backends (incl. GPU).

Borrow

• Primitive discipline and fusion-minded IR choices.
• Cost-model-aware design for bulk array operators.
• Tooling expectations for performance transparency.

Caution

• Futhark's tradeoffs are HPC-first; your roadmap also needs effects, ecosystem extension, and proof track.

C. JAX / XLA / StableHLO ecosystem

Why relevant

• Production-proven transformation stack (vmap, grad, pjit/sharding) and shape-aware lowering flow.

Borrow

• Separation of user-level ergonomics from canonical lowered form.
• Transform-centric architecture (program rewrites as first-class concern).
• Multi-device sharding as typed/constraint-driven transformation.

Caution

• Avoid Python-level dynamism and tracing opacity in your core language contract.
• Keep your explicit core IR; don't regress into hidden semantics.

D. Koka / Eff / Multicore OCaml effects

Why relevant

• Your roadmap depends on effect-structured AD/self-modeling in later phases.

Borrow

• Algebraic effects + handlers as the semantic mechanism for transformations.
• Effect typing discipline and row-like reasoning.
• Practical implementation strategies in OCaml ecosystem (important for current compiler language).

Caution

• Keep effect surface staged by phase; don't overload Phase 1 core with Phase 2 concerns.

E. Rust (type and runtime discipline)

Why relevant

• Already your runtime language.
• Strong model for explicitness around memory/ABI boundaries.

Borrow

• Trait-oriented organization for runtime API surfaces (when you leave simple admissibility tables).
• ABI stewardship discipline.
• Safety + performance engineering culture for long-lived runtime.

Caution

• Do not mirror Rust's type complexity in the front-end language unless it clearly benefits tensor typing and proofs.

F. Lean/Coq/Isabelle ecosystem (verification style)

Why relevant

• You already committed to Lean for mechanization.

Borrow

• Proof-friendly core definitions (small-step semantics, preservation/progress structure).
• Separation of executable implementation from proof model.

Caution

• Keep the spec minimal enough to be mechanizable; avoid semantic features that explode proof effort too early.

G. MLIR ecosystem (not a language, but unavoidable substrate)

Why relevant

• Practical path to multi-target code generation today.

Borrow

• Dialect staging and progressive lowering discipline.
• Target-specific lowering without changing front-end type story.

Caution

• Ensure the language's semantic commitments stay independent of transient MLIR pass behavior.

3) Type-system additions likely needed beyond Phase 0

If the initiative is truly "AI-native" and not "tensor-only," these are likely necessary extensions:

1. Product/record types for model/config/runtime metadata.
2. Sum/enum/result types for control/data states and typed failures.
3. Effect-annotated function types once Phase 2 starts (T -> U !{effects}).
4. Capability/sharding annotations in types (later phases) for hardware and distributed concerns.
5. Potential non-tensor domain types (e.g., dataframe/schema-typed values) as first-class library-level extensions.

Keep the rule: tensor-first core, but not tensor-only language.

4) Primitive-set guidance from cross-language comparison

Near-term practical guidance:

1. Keep Phase 0's strict core explicitness (good for implementation and proofs).
2. Add high-leverage primitives as Phase 1 extensions where verbosity is clearly pathological:
   • variadic-batch matmul,
   • softmax primitive (or equivalent canonical lowering surface),
   • gather family when data-dependent indexing becomes unavoidable.
3. Push ergonomics to surface sugar (Phase 7), not core semantic ambiguity.

This matches lessons from Futhark/JAX-like systems: small explicit kernels + ergonomic front-end can coexist.

5) Multi-target strategy: what to model now

For "multiple targets," model these dimensions explicitly in design docs before implementation grows:

1. Target capability profile (tensor cores, bf16/fp8 availability, memory model, collectives).
2. Numerical behavior policy by target class (reproducibility/perf tradeoffs).
3. Lowering contracts from core ops to target-specific kernels.
4. Fallback hierarchy (e.g., CUDA specialized -> generic GPU -> CPU reference).

This is where hardware-abstraction and verification tracks intersect: capability constraints should be typed, not hidden in backend code.

6) Recommended concrete next steps

1. Add an ADR for language inspiration policy: what is borrowed from Dex/Futhark/JAX/effects systems and what is intentionally rejected.
2. In Phase 1 planning docs, add a short section "Primitive pressure from real workloads" linking directly to real-world examples.
3. Draft a Phase 2 pre-spec note for effect-typed function signatures using OCaml-handler-informed semantics.
4. Define a target matrix doc (CPU/CUDA/ROCm/TPU-future) with required capability traits and expected primitive coverage.

7) Bottom line

The best design posture for this project is:

• Dex/Futhark-style typed array core
• JAX-style transformation awareness
• Koka/Eff/OCaml-effects-style self-modeling path
• Rust-style runtime/ABI discipline
• Lean-friendly formal minimalism
• MLIR-backed multi-target practicality

That combination is credible for an AI-native language that is both implementable now and extensible toward self-modeling later.