daitai-language v1.4 — Formal Specification

Creator: Joakim Cöster · joakim@daitai.org
Version: 1.3.1
Status: Normative
Date: 2026-03-30

---

1. Introduction

daitai-language is an algebraic, object-oriented pseudolanguage designed to specify algorithms clearly and deterministically. It is not executable — it exists for reasoning, transformation, and transpilation to Java, C++, TypeScript, Python, Rust, Go, and WebAssembly.

Clarity, determinism, and correctness are strictly more important than expressiveness or convenience.

---

2. Authority

This document is normative. If a construct, keyword, or behavior is not explicitly permitted by this document, it is forbidden.

---

3. Design Principles

---

4. Lexical Structure

4.1 Keywords

class    interface   enum        function    method
static   return      if          else        for
in       while       match       case        val
this     import      module      implements  extends

4.2 Algebraic Keywords (v1.2)

MONOID        GROUP         RING          SEMIRING
LATTICE       CATEGORY      FUNCTOR       APPLICATIVE
MONAD         COMONAD       FREEMONAD     ARROW
ARROWCHOICE   ARROWLOOP     PROFUNCTOR    BIFUNCTOR
CONTRAVARIANT NATURALTRANSFORM  COALGEBRA
YONEDA        LEFTKAN       RIGHTKAN      ADJUNCTION
GALOIS        TOPOS         OPERAD        FALGEBRA
MONOIDALCATEGORY  STRINGDIAGRAM
ENRICHEDCATEGORY  TRACEDMONOIDAL
TWOCATEGORY       COMPACTCLOSED
DOUBLECATEGORY    MULTICATEGORY
MOE               MULTIMODAL
INFINITYGROUPOID  SHEAF
SPLITCOALGEBRA

4.3 Literals

42              -- Int
3.14            -- Float
true, false     -- Bool
"hello"         -- String
None            -- Optional<T> (empty)
Some(x)         -- Optional<T> (with value)
/pattern/flags  -- Regex (v1.1)

4.4 Operators

+  -  *  /  %           -- Arithmetic
== != < > <= >=         -- Comparison
&& || !                 -- Logic
|>                      -- Pipeline
.                       -- Member access

4.5 Comments

-- Line comment
{- Block comment -}

4.6 Indentation

Indentation (whitespace) is significant and defines blocks, similar to Python.

---

5. Type System

5.1 Base Types

5.2 Generic Types

5.3 Regex (v1.1)

val pattern: Regex = /[a-z]+/i
function matches(s: String, r: Regex) -> Bool
function findAll(s: String, r: Regex) -> List<String>

5.4 Type Variables

Type variables are written in uppercase: T, A, B, K, V.

function map<A, B>(list: List<A>, f: (A) -> B) -> List<B>

5.5 Value Semantics

• All types are compared structurally
• No reference identity
• No null — Optional<T> is always used

---

6. Declarations

6.1 Classes (Product Types)

class Vec3:
    x: Float
    y: Float
    z: Float

    method add(other: Vec3) -> Vec3:
        return Vec3(x = this.x + other.x, y = this.y + other.y, z = this.z + other.z)

    static method zero() -> Vec3:
        return Vec3(x = 0.0, y = 0.0, z = 0.0)

Rules:

• All fields are immutable (val semantics)
• Methods are pure — this is read-only
• Constructors have no logic
• Equality is structural

6.2 Interface (Sum Types / Shapes)

interface Shape

class Circle implements Shape:
    center: Vec2
    radius: Float

class Rectangle implements Shape:
    topLeft: Vec2
    width: Float
    height: Float

Rules:

• Interfaces have no fields
• Interfaces have no methods with bodies
• No default implementation
• Nominal typing

6.3 Enums

enum Direction:
    North
    South
    East
    West

6.4 Algebraic Data Types (v1.1)

enum Tree<T>:
    Leaf(value: T)
    Branch(left: Tree<T>, right: Tree<T>)

6.5 Functions

function distance(a: Vec2, b: Vec2) -> Float:
    val dx: Float = b.x - a.x
    val dy: Float = b.y - a.y
    return sqrt(dx * dx + dy * dy)

Rules:

• Pure — no side effects
• No global variables
• No closures (v1.0) — closures permitted in v1.1 with restrictions

6.6 Modules

module Geometry:
    class Vec2:
        x: Float
        y: Float
    function dot(a: Vec2, b: Vec2) -> Float:
        return a.x * b.x + a.y * b.y

---

7. Control Flow

7.1 if/else (expression)

val result: Int = if x > 0: x else: -x

7.2 for

for item in list:
    process(item)

7.3 while (restrictive)

while condition:
    body

7.4 match (v1.1)

match shape:
    case Circle(c, r):
        return pi * r * r
    case Rectangle(tl, w, h):
        return w * h

Match must be exhaustive — all variants are covered.

7.5 Forbidden Control Flow

---

8. Error Handling

enum ParseError:
    InvalidFormat
    Overflow

function parseInt(s: String) -> Result<Int, ParseError>:
    if isValid(s):
        return Ok(toInt(s))
    else:
        return Err(ParseError.InvalidFormat)

---

9. Algebraic Structures (v1.1)

daitai-language v1.1 has built-in support for algebraic structures from abstract algebra and category theory.

9.1 Algebra

9.2 Category Theory — Fundamentals

9.3 Category Theory — Advanced

9.4 Category Theory — Monoidal & Higher

9.5 Other

9.6 Example Syntax

MONOID StringConcat over String:
    combine(a, b) = a + b
    empty = ""

FUNCTOR ListF<A, B>:
    map(f: (A) -> B, fa: List<A>) -> List<B>:
        return fa.map(f)

MONAD MaybeM<A>:
    pure(a: A) -> Optional<A>:
        return Some(a)
    flatMap(ma: Optional<A>, f: (A) -> Optional<B>) -> Optional<B>:
        match ma:
            case Some(a): return f(a)
            case None: return None

TWOCATEGORY Cat2:
    vcomp(alpha, beta) = verticalCompose(alpha, beta)
    hcomp(alpha, beta) = horizontalCompose(alpha, beta)
    identity2(f) = identityTwoCell(f)
    whiskerL(f, alpha) = leftWhisker(f, alpha)
    whiskerR(alpha, f) = rightWhisker(alpha, f)

---

10. Transpilation Targets

daitai-language transpiles to:

---

11. Forbidden Constructs

---

12. Formal Grammar (EBNF)

program        = { declaration } ;

declaration    = classDecl
               | interfaceDecl
               | enumDecl
               | functionDecl
               | moduleDecl
               | algebraDecl ;

classDecl      = "class" IDENT [ typeParams ] [ "implements" IDENT ] ":"
                   INDENT { fieldDecl | methodDecl | staticMethod } DEDENT ;

interfaceDecl  = "interface" IDENT [ typeParams ] ;

enumDecl       = "enum" IDENT [ typeParams ] ":"
                   INDENT { enumVariant } DEDENT ;

enumVariant    = IDENT [ "(" fieldList ")" ] ;

functionDecl   = "function" IDENT [ typeParams ] "(" paramList ")" "->" typeRef ":"
                   INDENT block DEDENT ;

moduleDecl     = "module" IDENT ":"
                   INDENT { declaration } DEDENT ;

algebraDecl    = algebraKW IDENT [ algebraOver ] [ typeParams ] ":"
                   INDENT { operationDecl } DEDENT ;

algebraKW      = "MONOID" | "GROUP" | "RING" | "SEMIRING" | "LATTICE"
               | "CATEGORY" | "FUNCTOR" | "APPLICATIVE" | "MONAD"
               | "COMONAD" | "FREEMONAD" | "ARROW" | "ARROWCHOICE"
               | "ARROWLOOP" | "PROFUNCTOR" | "BIFUNCTOR" | "CONTRAVARIANT"
               | "NATURALTRANSFORM" | "COALGEBRA" | "YONEDA"
               | "LEFTKAN" | "RIGHTKAN" | "ADJUNCTION" | "GALOIS"
               | "TOPOS" | "OPERAD" | "FALGEBRA"
               | "MONOIDALCATEGORY" | "STRINGDIAGRAM"
               | "ENRICHEDCATEGORY" | "TRACEDMONOIDAL"
               | "TWOCATEGORY" | "COMPACTCLOSED"
               | "DOUBLECATEGORY" | "MULTICATEGORY"
               | "MOE" | "MULTIMODAL"
               | "INFINITYGROUPOID" | "SHEAF" | "SPLITCOALGEBRA" ;

algebraOver    = "over" typeRef ;

fieldDecl      = IDENT ":" typeRef ;

methodDecl     = "method" IDENT "(" paramList ")" "->" typeRef ":"
                   INDENT block DEDENT ;

staticMethod   = "static" methodDecl ;

operationDecl  = IDENT "(" paramList ")" [ "->" typeRef ] "=" expr ;

typeRef        = IDENT [ "<" typeRef { "," typeRef } ">" ]
               | "(" typeRef { "," typeRef } ")" "->" typeRef ;

typeParams     = "<" IDENT { "," IDENT } ">" ;

paramList      = [ param { "," param } ] ;
param          = IDENT ":" typeRef ;

block          = { statement } ;

statement      = valDecl
               | returnStmt
               | ifExpr
               | forLoop
               | whileLoop
               | matchExpr
               | expr ;

valDecl        = "val" IDENT ":" typeRef "=" expr ;
returnStmt     = "return" expr ;

ifExpr         = "if" expr ":" INDENT block DEDENT
                 [ "else" ":" INDENT block DEDENT ] ;

forLoop        = "for" IDENT "in" expr ":" INDENT block DEDENT ;
whileLoop      = "while" expr ":" INDENT block DEDENT ;

matchExpr      = "match" expr ":"
                   INDENT { matchCase } DEDENT ;
matchCase      = "case" pattern ":" INDENT block DEDENT ;

pattern        = IDENT [ "(" pattern { "," pattern } ")" ]
               | literal ;

expr           = literal
               | IDENT
               | expr "." IDENT
               | expr "(" argList ")"
               | expr binOp expr
               | unaryOp expr
               | expr "|>" expr
               | "(" expr ")"
               | ifExpr
               | matchExpr ;

literal        = INT | FLOAT | STRING | "true" | "false" | "None" | regexLit ;
regexLit       = "/" regexBody "/" { regexFlag } ;

binOp          = "+" | "-" | "*" | "/" | "%" | "==" | "!=" | "<" | ">"
               | "<=" | ">=" | "&&" | "||" ;
unaryOp        = "-" | "!" ;

---

13. Semantic Rules

13.1 Scope & Symbol Table

• Each block introduces a new scope
• Shadowing is forbidden
• All names must be declared before use

13.2 Type Checking

• All expressions have a static type
• Type variables are unified at instantiation
• No implicit type conversion

13.3 Purity Check

• Functions and methods must not mutate state
• No side effects (IO, logging, random)
• this is read-only in methods

13.4 Control Flow Validation

• All branches in if/else must have the same return type
• Match must be exhaustive
• No unreachable statements

13.5 Algebraic Laws

The transpiler SHOULD verify that algebraic declarations satisfy their laws (associativity, identity, etc.) but this is non-normative in v1.1.

---

14. Version History

---

15. Algebraic Structures — Reference (v1.2)

15.1 Fundamental Algebra

15.2 Category Theory

15.3 Higher Abstraction

15.4 Universal Constructions

15.5 Algebraic Data Analysis

15.6 Domain-Specific (v1.2)

15.7 Higher Homotopy Theory & Dynamic Growth (v1.3)

∞-Groupoid — The foundation of HoTT (Homotopy Type Theory). Types are ∞-groupoids. Usage: anti-forgetting memory where knowledge lives in a path-connected space — nothing can become inaccessible.

Sheaf — Gluing theory: locally consistent data can always be lifted to globally consistent data. Usage: MoE coherence where each expert has local knowledge that must integrate into a consistent whole. H¹(Sheaf) = 0 ⟹ no conflicts.

SplitCoalgebra — Coalgebraic neuron-split: neurons split under stress (rate² > threshold) and are verified via Topos subobject classifier Ω. Usage: dynamic architecture growth without semantic loss.

---

16. Quantum Mechanical Algebra (v1.4)

16.1 Hilbert Space Sorts

v1.4 introduces native Dirac notation literals and algebraic sorts for quantum computation:

Ket        -- |ψ⟩  (column vector in Hilbert space)
Bra        -- ⟨φ|  (row vector, adjoint of Ket)
Operator   -- linear operator A: H → H
Complex    -- complex number a + bi

16.2 Quantum Literals

|0⟩, |1⟩, |+⟩, |−⟩       -- Standard qubits
|ψ⟩ = α|0⟩ + β|1⟩        -- Superposition
⟨φ| = ⟨0|γ* + ⟨1|δ*      -- Bra (conjugate transpose)
⟨φ|ψ⟩                     -- Inner product (scalar ∈ Complex)
|ψ⟩⟨φ|                    -- Outer product (Operator)

16.3 Keywords

KET           BRA           OPERATOR      COMPLEX
HILBERTSPACE  OBSERVABLE    MEASUREMENT
UNITARYGROUP  DENSITYMATRIX QUANTUMCHANNEL

16.4 Algebraic Structures

16.5 Dirac Algebra

The following operator identities are verified at compile time:

⟨φ|ψ⟩ = (⟨ψ|φ⟩)*                    -- Conjugate symmetry
⟨φ|(α|ψ₁⟩ + β|ψ₂⟩) = α⟨φ|ψ₁⟩ + β⟨φ|ψ₂⟩  -- Linearity
(|ψ⟩⟨φ|)† = |φ⟩⟨ψ|                   -- Adjoint of outer product
Σ_i |i⟩⟨i| = I                       -- Completeness relation

16.6 Quantum Gates (predefined operators)

PAULIX    = |0⟩⟨1| + |1⟩⟨0|           -- Pauli-X (NOT)
PAULIY    = -i|0⟩⟨1| + i|1⟩⟨0|        -- Pauli-Y
PAULIZ    = |0⟩⟨0| - |1⟩⟨1|           -- Pauli-Z
HADAMARD  = (|0⟩⟨0| + |0⟩⟨1| + |1⟩⟨0| - |1⟩⟨1|) / √2
CNOT      = |00⟩⟨00| + |01⟩⟨01| + |10⟩⟨11| + |11⟩⟨10|

Quantum + Topos coupling: MEASUREMENT uses the Topos subobject classifier Ω to formally handle measurement outcomes as truth values in intuitionistic logic. The Born rule is expressed as a natural transformation from DENSITYMATRIX to SHEAF of probability distributions.

---

17. Future (v1.5, non-normative)

• Higher-Kinded Types
• Effect System (algebraic effects)
• Dependent Types (limited)
• Linear Types (quantum no-cloning theorem)
• Formal verification of algebraic laws
• ∞-Category (full ∞-category theory)
• Higher Operad (∞-operad)
• Spectral Sequences (homological algebra)
• Persistent Homology (topological data analysis)
• Quantum Error Correction (stabilizer codes)
• Topological Quantum Computation (anyons, braid groups)