# Mathematical Programming Language (MPL)

## Core Symbol Set

### Mathematical Foundation (LaTeX)
- **Variables:** α,β,γ,δ,ε,ζ,η,θ,ι,κ,λ,μ,ν,ξ,ο,π,ρ,σ,τ,υ,φ,χ,ψ,ω
- **Collections:** ∅,∪,∩,⊂,⊃,∈,∉,⊆,⊇
- **Logic:** ∧,∨,¬,⟹,⟺,∀,∃
- **Operations:** +,-,×,÷,∗,∘
- **Relations:** =,≠,<,>,≤,≥,≈,∼
- **Functions:** f: A → B, λ
- **Assignment:** ←
- **Definition:** ≜
- **Structure:** (),[],{},⟨⟩

### Effect Extensions (11 new glyphs)
- **↯** Raise exception
- **↴** Handle exception  
- **‖** Parallel composition
- **⌈⌉** Atomic section/lock
- **⊕** Allocate resource
- **⊖** Release resource
- **𝓜** Module declaration
- **⇐** Import
- **⇒** Export  
- **⇀** Send (network)
- **↽** Receive (network)

### Additional Operators
- **⟨v|e⟩** Choice type (value or error)
- **🖫** File path prefix
- **⇡⇣** Stream positioning
- **⇆** Atomic swap
- **⟪⟫** Deep update path
- **⌜⌝** Code quotation
- **⌞⌟** Code evaluation
- **?** Introspection
- **⧈** Breakpoint
- **✎** Trace/log
- **⏲** Delay
- **⟳** Periodic task
- **〔〕** RAII scope

## Grammar

### Basic Expressions
```
expr ::= variable | literal | operation | function_call | block

variable ::= α | β | γ | ... | ω
literal ::= number | string | path | list | set
operation ::= expr OP expr
function_call ::= f(expr, ...)
block ::= { statement; ... }
```

### Statements
```
assignment ::= variable ← expr
definition ::= variable ≜ expr  
conditional ::= condition ⟹ expr
iteration ::= ∀variable∈set: expr
parallel ::= expr ‖ expr
atomic ::= ⌈expr⌉_lock
exception ::= ↯expr | expr ↴ {↯e ⇒ handler}
```

### Types
```
basic_type ::= ℕ | ℤ | ℚ | ℝ | ℂ | 𝔹
function_type ::= domain → codomain
choice_type ::= ⟨type|type⟩
effect_type ::= type^effect
```

## Example Programs

### Hello World
```
✎"Hello, World!"
```

### Factorial
```
factorial ≜ λn∈ℕ: n≤1 ⟹ 1 | n×factorial(n-1)
result ← factorial(5)
✎result
```

### File Processing with Error Handling
```
processFile ≜ λpath: 🖫path ↴ {
    data ← readFile(path)
    result ← transform(data)
    writeFile(result, 🖫"output.txt")
    ⟨"success"|"failed"⟩
} ↴ {↯e ⇒ ⟨⊥|e⟩}
```

### Concurrent Download
```
downloadAll ≜ λurls: ∀url∈urls: (
    fetchData(url) ‖ processData(url)
) ⟹ mergeResults()
```

### Module Definition
```
𝓜 Mathematics ⇒ {
    π ≜ 3.14159...
    sin ≜ λx∈ℝ: ...
    cos ≜ λx∈ℝ: ...
}

angle ← π/4
result ← Mathematics‧sin(angle)
```

### Resource Management
```
databaseQuery ≜ λquery: 〔
    conn ← database ⊕
    ⌈
        result ← execute(conn, query)
        ✎"Query executed"
        result
    ⌉_db_lock
    conn ⊖
〕
```

### Metaprogramming
```
generateFunction ≜ λname: ⌜
    λx: x × 2
⌝

doubler ← ⌞generateFunction("doubler")⌟
result ← doubler(21)
```

### Real-time System
```
scheduler ≜ ⟳(
    tasks ← getPendingTasks()
    ∀task∈tasks: execute(task) ‖ monitor(task)
    , 100ms
)
```

### Network Server
```
server ≜ λport: 〔
    socket ← bind(port) ⊕
    ∀request: (
        data ← ↽_socket request
        response ← processRequest(data)
        ⇀_socket response
    ) ‖ handleNext()
    socket ⊖
〕
```

### Type-safe Database
```
User ≜ {name: String, age: ℕ∣age>0, email: String}
query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ {
    ↯"Invalid user" ⟹ ⊥
}
```

## Critical Implementation Decisions

### Lexical Layer
- **Unicode Normalization:** NFC on ingest, reject mixed forms
- **Symbol Input:** Cross-platform keymap (Ctrl+Alt+g → γ) + ASCII escapes (\gamma → γ)
- **Semicolon handling:** Require explicit `;` everywhere except before `}`
- **Comments:** `--` for single-line comments (to end of line), `{- ... -}` for multi-line comments (nestable)
- **String Literals:** 
  - Standard strings: `"..."` with escape sequences (`\n`, `\t`, `\\`, `\"`, `\u{XXXXXX}`)
  - Raw strings: `"""..."""` for multi-line, no escape processing
- **Path Literals:** Both `🖫"path"` and `\path"path"` supported for compatibility
- **Number Literals:** Decimal (`123`, `3.14`), hex (`0x1A`), binary (`0b1101`), with optional type suffixes later

### Operator Precedence Table
| Level | Operators | Associativity |
|-------|-----------|---------------|
| 9 | function application | left |
| 8 | ↯ ✎ ? ⧈ ⏲ (prefix) | right |
| 7 | ∘ | left |
| 6 | × ÷ ∗ | left |
| 5 | + - | left |
| 4 | = ≠ < > ≤ ≥ ≈ ∼ | non-assoc |
| 3 | ∧ | left |
| 2 | ∨ | left |
| 1 | ⟹ | right |
| 0 | ← | right |
| -1 | ‖ | left |
| -2 | ; | left |

### Grammar Resolutions
- **Block semantics:** Every statement returns value (ML-style)
- **Conditional associativity:** Right-associative (a⟹b⟹c = a⟹(b⟹c))
- **Choice type parsing:** Different tokens for |value vs |type contexts

### Type System Extensions
- **Effect polymorphism:** `map : (A→ᴱ B) → List A →ᴱ List B`
- **Linear resources:** Compile-time ⊕/⊖ tracking, 〔〕 = linear region sugar
- **Exception types:** `f : A →⟨E⟩ B` where E is union of raised types

### Concurrency Semantics
- **Memory model:** Happens-before with acquire/release on ⌈⌉
- **Parallel failure:** Fail-fast, cancel siblings, aggregate choice types
- **Deadlock detection:** Optional --debug-sync runtime verifier

### Module System
- **Naming:** `𝓜‧A‧B` in source → `A/B.mpl` on disk
- **Re-export:** `Vector ⇒ 𝓜‧LinearAlgebra‧Vector`
- **Versioning:** `𝓜 LinearAlgebra@1.2.0 ⇒ { ... }`

### Missing Syntax (M1 Requirements)

#### Pattern Matching
```
match expr with
| pattern₁ ⟹ expr₁
| pattern₂ ⟹ expr₂
end

pattern ::= _ | literal | variable
          | ⟨Left pattern⟩ | ⟨Right pattern⟩    // choice
          | {field₁ = pattern₁, …}              // records
          | (pattern₁, pattern₂, …)             // tuples
```

#### Parametric Types
```
type_abs ::= ΛT. expr     // type lambda
type_app ::= expr [T]     // application

map ≜ ΛA. ΛB. λf: A→ᴱ B. λxs: List A. …
```

#### Foreign Function Interface
```
𝓜 Crypto@0.1.0 uses "libcrypto.so" {
    foreign digest      : 🖫Path →⟨IOErr⟩ Digest
    foreign randomBytes : ℕ → Bytes
}
```

### Static Semantics Rules

#### Region Typing
```
Γ ⊢ e₁ : Resource r          Γ, h:r ⊢ e₂ : α
───────────────────────────────────────────────   (REGION)
Γ ⊢ 〔 x ← e₁ ; e₂ ; x ⊖ 〕 : α
```

#### Exception Handling
```
Γ ⊢ e₁ : α             Γ ⊢ e₂ : β           Γ ⊢ e₃ : β
─────────────────────────────────────────────────────────  (HANDLE)
Γ ⊢ e₁ ↴ { ↯x ⇒ e₂ } : β  ▷  Eff = (Eff(e₁) - {Raise ε}) ∪ Eff(e₂)
```

### M0 Exit Criteria
1. All spec examples parse and pretty-print round-trip
2. No shift/reduce conflicts in grammar
3. 10,000 random token sequences don't crash parser

## Implementation Roadmap
1. **M0:** ANTLR grammar + 500 LOC test suite
2. **M1:** Hindley-Milner + row effects + linearity checker
3. **M2:** Stack VM with green threads + deterministic GC
4. **M3:** Self-hosting (stdlib + compiler in MPL)
5. **M4:** LLVM backend with vectorized math ops
6. **M5:** Package manager (fetch/build/run workflow)

This specification provides a complete foundation for implementing a mathematical programming language that maintains cognitive universality while supporting all modern programming paradigms.