daitai-language v1.4 — 正式仕様書

Creator: Joakim Cöster · joakim@daitai.org
バージョン: 1.3.1
ステータス: 規範的
日付: 2026-03-30

---

1. はじめに

daitai-languageは、アルゴリズムを明確かつ決定論的に仕様記述するために設計された代数的オブジェクト指向疑似言語です。実行可能ではなく、推論・変換・Java、C++、TypeScript、Python、Rust、Go、WebAssemblyへのトランスパイルのために存在します。

明確性、決定論、正確性は、表現力や利便性よりも厳密に重要です。

---

2. 権威

本文書は規範的です。本文書で明示的に許可されていない構文、キーワード、動作は禁止されています。

---

3. 設計原則

---

4. 字句構造

4.1 キーワード

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

4.2 代数キーワード (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 リテラル

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

4.4 演算子

+  -  *  /  %           -- 算術
== != < > <= >=         -- 比較
&& || !                 -- 論理
|>                      -- パイプライン
.                       -- メンバーアクセス

4.5 コメント

-- 行コメント
{- ブロックコメント -}

4.6 インデント

インデント（空白）は有意であり、Pythonと同様にブロックを定義します。

---

5. 型システム

5.1 基本型

5.2 ジェネリック型

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 型変数

型変数は大文字で記述: T, A, B, K, V。

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

5.5 値セマンティクス

• すべての型は構造的に比較される
• 参照同一性なし
• nullなし — 常にOptional<T>を使用

---

6. 宣言

6.1 クラス（積型）

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)

規則:

• すべてのフィールドは不変（valセマンティクス）
• メソッドはpure — thisは読み取り専用
• コンストラクタにロジックなし
• 等価性は構造的

6.2 Interface（和型 / シェイプ）

interface Shape

class Circle implements Shape:
    center: Vec2
    radius: Float

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

規則:

• インターフェースにフィールドなし
• インターフェースに本体を持つメソッドなし
• デフォルト実装なし
• 名前的型付け

6.3 Enum

enum Direction:
    North
    South
    East
    West

6.4 代数的データ型 (v1.1)

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

6.5 関数

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)

規則:

• Pure — 副作用なし
• グローバル変数なし
• クロージャなし (v1.0) — v1.1で制限付きクロージャ許可

6.6 モジュール

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. 制御フロー

7.1 if/else（式）

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

7.2 for

for item in list:
    process(item)

7.3 while（制限的）

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は網羅的でなければなりません — すべてのバリアントをカバーします。

7.5 禁止された制御フロー

---

8. エラーハンドリング

enum ParseError:
    InvalidFormat
    Overflow

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

---

9. 代数構造 (v1.1)

daitai-language v1.1は、抽象代数と圏論の代数構造を組み込みでサポートしています。

9.1 代数

9.2 圏論 — 基礎

9.3 圏論 — 上級

9.4 圏論 — モノイダル圏 & 高次

9.5 その他

9.6 構文例

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. トランスパイルターゲット

daitai-languageは以下にトランスパイルします：

---

11. 禁止された構文

---

12. 正式文法 (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. 意味規則

13.1 スコープとシンボルテーブル

• 各ブロックが新しいスコープを導入
• シャドウイングは禁止
• すべての名前は使用前に宣言が必要

13.2 型検査

• すべての式は静的型を持つ
• 型変数はインスタンス化時に統一される
• 暗黙の型変換なし

13.3 純粋性チェック

• 関数とメソッドは状態をミューテートしてはならない
• 副作用なし（IO、ロギング、乱数）
• メソッド内でthisは読み取り専用

13.4 制御フロー検証

• if/elseのすべての分岐は同じ戻り値型でなければならない
• matchは網羅的でなければならない
• 到達不能な文は禁止

13.5 代数法則

トランスパイラは代数宣言がその法則（結合律、恒等律等）を満たすことを検証すべき(SHOULD)ですが、これはv1.1では非規範的です。

---

14. バージョン履歴

---

15. 代数構造 — リファレンス (v1.2)

15.1 基礎代数

15.2 圏論

15.3 高次抽象

15.4 普遍的構成

15.5 代数的データ分析

15.6 ドメイン固有 (v1.2)

15.7 高次ホモトピー理論 & 動的成長 (v1.3)

∞-Groupoid — HoTT（ホモトピー型理論）の基礎。型は∞-groupoidです。用途：知識がpath-connected空間に存在し、何もアクセス不能にならない忘却防止メモリ。

Sheaf — 接合理論：局所的に整合的なデータは常に大域的に整合的なデータに持ち上げ可能。用途：各エキスパートが局所知識を持ち、整合的な全体に統合されるMoEコヒーレンス。H¹(Sheaf) = 0 ⟹ 矛盾なし。

SplitCoalgebra — 余代数的ニューロン分裂：ニューロンがストレス下で分裂し (rate² > 閾値)、Topos部分対象分類子Ωで検証。用途：意味損失なしの動的アーキテクチャ成長。

---

16. 量子力学的代数 (v1.4)

16.1 ヒルベルト空間ソート

v1.4はディラック記法リテラルと量子計算のための代数的ソートを導入します：

Ket        -- |ψ⟩  (ヒルベルト空間の列ベクトル)
Bra        -- ⟨φ|  (行ベクトル、Ketの随伴)
Operator   -- 線形演算子 A: H → H
Complex    -- 複素数 a + bi

16.2 量子リテラル

|0⟩, |1⟩, |+⟩, |−⟩       -- 標準量子ビット
|ψ⟩ = α|0⟩ + β|1⟩        -- 重ね合わせ
⟨φ| = ⟨0|γ* + ⟨1|δ*      -- ブラ (共役転置)
⟨φ|ψ⟩                     -- 内積 (スカラー ∈ Complex)
|ψ⟩⟨φ|                    -- 外積 (Operator)

16.3 キーワード

KET           BRA           OPERATOR      COMPLEX
HILBERTSPACE  OBSERVABLE    MEASUREMENT
UNITARYGROUP  DENSITYMATRIX QUANTUMCHANNEL

16.4 代数的構造

16.5 ディラック代数

以下の演算子恒等式はコンパイル時に検証されます：

⟨φ|ψ⟩ = (⟨ψ|φ⟩)*                    -- 共役対称性
⟨φ|(α|ψ₁⟩ + β|ψ₂⟩) = α⟨φ|ψ₁⟩ + β⟨φ|ψ₂⟩  -- 線形性
(|ψ⟩⟨φ|)† = |φ⟩⟨ψ|                   -- 外積の随伴
Σ_i |i⟩⟨i| = I                       -- 完全性関係

16.6 量子ゲート (事前定義演算子)

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

量子+トポス結合: MEASUREMENTはトポスの部分対象分類子Ωを使用して、測定結果を直観主義論理の真理値として形式的に処理します。ボルンの規則は、DENSITYMATRIXから確率分布のSHEAFへの自然変換として表現されます。

---

17. 将来 (v1.5、非規範的)

• 高カインド型
• エフェクトシステム (代数的エフェクト)
• 依存型 (制限付き)
• 線形型 (量子ノークローニング定理)
• 代数法則の形式検証
• ∞-圏 (完全な∞-圏論)
• 高次オペラド (∞-オペラド)
• スペクトル系列 (ホモロジー代数)
• 永続的ホモロジー (位相的データ解析)
• 量子誤り訂正 (安定化符号)
• 位相的量子計算 (エニオン、組紐群)