Initial commit: MPL specification and M0 documentation
- Complete language specification (math_prog_lang.md) - M0 blocker tracking issue template - Glyph escape sequences reference - Operator precedence table - Example programs from specification - Project README Ready for pre-M0 implementation phase
This commit is contained in:
developtheweb
commit
57efd37df6
15 changed files with 602 additions and 0 deletions
79
ISSUE_M0_BLOCKERS.md
Normal file
79
ISSUE_M0_BLOCKERS.md
Normal file
|
|
@ -0,0 +1,79 @@
|
|||
# 🚀 Lock lexical & grammar spec for M0
|
||||
|
||||
## Overview
|
||||
This issue tracks the resolution of three critical blockers that must be decided before implementing the ANTLR 4 grammar for MPL. These decisions are required to ensure the lexer can be implemented without surprises and that all M0 exit criteria are objectively testable.
|
||||
|
||||
## Blockers
|
||||
|
||||
### 1. Comment Syntax 🚫
|
||||
**Status:** MISSING
|
||||
**Decision needed by:** Before lexer PR is merged
|
||||
**Rationale:** Source files cannot compile without comment support
|
||||
|
||||
**Options to consider:**
|
||||
- `--` till EOL (Ada/Haskell style)
|
||||
- `/* ... */` (C style)
|
||||
- `#` till EOL (Python/Ruby style)
|
||||
- Support for both single-line and multi-line comments
|
||||
|
||||
**Recommendation:** Use `--` for single-line and `{- ... -}` for multi-line (Haskell-style) to align with functional paradigm
|
||||
|
||||
### 2. String Literal Rules ⚠️
|
||||
**Status:** INCOMPLETE
|
||||
**Decision needed by:** Before lexer PR is merged
|
||||
**Rationale:** Required for hello-world sample
|
||||
|
||||
**Decisions needed:**
|
||||
- Escape sequences: Standard set (`\n`, `\t`, `\\`, `\"`) + Unicode (`\u{1F600}`)
|
||||
- String delimiters: Double quotes only or support for raw strings?
|
||||
- Multi-line string support?
|
||||
- String interpolation syntax (or defer to M1)?
|
||||
|
||||
**Recommendation:**
|
||||
- Use `"..."` for regular strings with standard escapes
|
||||
- Add `"""..."""` for multi-line raw strings (no escapes)
|
||||
- Defer interpolation to M1
|
||||
|
||||
### 3. Path Literal Fallback ⚠️
|
||||
**Status:** INCOMPLETE
|
||||
**Decision needed by:** Before lexer PR is merged
|
||||
**Rationale:** `🖫` glyph may not render on all systems
|
||||
|
||||
**Options:**
|
||||
- Make `🖫` required (pure Unicode approach)
|
||||
- Add ASCII escape like `@path"..."` or `#path"..."`
|
||||
- Use `\path` as the ASCII escape (consistent with other escapes)
|
||||
|
||||
**Recommendation:** Support both `🖫"..."` and `\path"..."` for maximum compatibility
|
||||
|
||||
## Additional Lexical Decisions
|
||||
|
||||
### ASCII Escape Mapping
|
||||
Need complete one-to-one table for all Unicode glyphs. Current partial list:
|
||||
- `\gamma` → `γ`
|
||||
- `\lam` or `\lambda` → `λ`
|
||||
- `\Rightarrow` → `⇒`
|
||||
- etc.
|
||||
|
||||
### Number Literal Format
|
||||
- Decimal: `123`, `123.456`, `1.23e10`
|
||||
- Hex: `0x1A2B`
|
||||
- Binary: `0b1101`
|
||||
- Suffixes: `_i32`, `_f64`, `_bigint` (or defer to M1?)
|
||||
|
||||
## Exit Criteria
|
||||
Once this issue is closed, we can:
|
||||
- [ ] Implement the lexer with confidence
|
||||
- [ ] Parse all example programs
|
||||
- [ ] Generate syntax highlighting for editors
|
||||
- [ ] Create the `glyph-escapes.md` reference
|
||||
|
||||
## Action Items
|
||||
1. Make decisions on all three blockers
|
||||
2. Update `math_prog_lang.md` with decisions
|
||||
3. Create `docs/lexical-spec.md` with complete token rules
|
||||
4. Tag specification as `v0.1-alpha`
|
||||
|
||||
---
|
||||
**Assignee:** @developtheweb
|
||||
**Labels:** `blocker`, `M0`, `specification`, `grammar`
|
||||
31
README.md
Normal file
31
README.md
Normal file
|
|
@ -0,0 +1,31 @@
|
|||
# Mathematical Programming Language (MPL)
|
||||
|
||||
A programming language that maintains cognitive universality while supporting all modern programming paradigms through mathematical notation.
|
||||
|
||||
## Quick Start
|
||||
|
||||
```mpl
|
||||
✎"Hello, World!"
|
||||
```
|
||||
|
||||
## Repository Structure
|
||||
|
||||
- `math_prog_lang.md` - Complete language specification
|
||||
- `ISSUE_M0_BLOCKERS.md` - Critical decisions needed before M0 implementation
|
||||
- `glyph-escapes.md` - ASCII escape sequences for all Unicode glyphs
|
||||
- `precedence.csv` - Operator precedence table
|
||||
- `examples/` - Example programs from the specification
|
||||
|
||||
## M0 Milestones
|
||||
|
||||
1. ✅ Language specification consolidated
|
||||
2. ✅ Pre-M0 audit completed
|
||||
3. 🚧 Resolve lexical blockers (see ISSUE_M0_BLOCKERS.md)
|
||||
4. ⏳ Implement ANTLR 4 grammar
|
||||
5. ⏳ Create test suite (500 LOC)
|
||||
6. ⏳ Achieve M0 exit criteria
|
||||
|
||||
## Contact
|
||||
|
||||
- GitHub: @developtheweb
|
||||
- Email: developtheweb@protonmail.com
|
||||
1
examples/01_hello_world.mpl
Normal file
1
examples/01_hello_world.mpl
Normal file
|
|
@ -0,0 +1 @@
|
|||
✎"Hello, World!"
|
||||
3
examples/02_factorial.mpl
Normal file
3
examples/02_factorial.mpl
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
factorial ≜ λn∈ℕ: n≤1 ⟹ 1 | n×factorial(n-1)
|
||||
result ← factorial(5)
|
||||
✎result
|
||||
6
examples/03_file_processing.mpl
Normal file
6
examples/03_file_processing.mpl
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
processFile ≜ λpath: 🖫path ↴ {
|
||||
data ← readFile(path)
|
||||
result ← transform(data)
|
||||
writeFile(result, 🖫"output.txt")
|
||||
⟨"success"|"failed"⟩
|
||||
} ↴ {↯e ⇒ ⟨⊥|e⟩}
|
||||
3
examples/04_concurrent_download.mpl
Normal file
3
examples/04_concurrent_download.mpl
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
downloadAll ≜ λurls: ∀url∈urls: (
|
||||
fetchData(url) ‖ processData(url)
|
||||
) ⟹ mergeResults()
|
||||
8
examples/05_module_definition.mpl
Normal file
8
examples/05_module_definition.mpl
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
𝓜 Mathematics ⇒ {
|
||||
π ≜ 3.14159
|
||||
sin ≜ λx∈ℝ: ...
|
||||
cos ≜ λx∈ℝ: ...
|
||||
}
|
||||
|
||||
angle ← π/4
|
||||
result ← Mathematics‧sin(angle)
|
||||
9
examples/06_resource_management.mpl
Normal file
9
examples/06_resource_management.mpl
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
databaseQuery ≜ λquery: 〔
|
||||
conn ← database ⊕
|
||||
⌈
|
||||
result ← execute(conn, query)
|
||||
✎"Query executed"
|
||||
result
|
||||
⌉_db_lock
|
||||
conn ⊖
|
||||
〕
|
||||
6
examples/07_metaprogramming.mpl
Normal file
6
examples/07_metaprogramming.mpl
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
generateFunction ≜ λname: ⌜
|
||||
λx: x × 2
|
||||
⌝
|
||||
|
||||
doubler ← ⌞generateFunction("doubler")⌟
|
||||
result ← doubler(21)
|
||||
5
examples/08_realtime_system.mpl
Normal file
5
examples/08_realtime_system.mpl
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
scheduler ≜ ⟳(
|
||||
tasks ← getPendingTasks()
|
||||
∀task∈tasks: execute(task) ‖ monitor(task)
|
||||
, 100ms
|
||||
)
|
||||
9
examples/09_network_server.mpl
Normal file
9
examples/09_network_server.mpl
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
server ≜ λport: 〔
|
||||
socket ← bind(port) ⊕
|
||||
∀request: (
|
||||
data ← ↽_socket request
|
||||
response ← processRequest(data)
|
||||
⇀_socket response
|
||||
) ‖ handleNext()
|
||||
socket ⊖
|
||||
〕
|
||||
4
examples/10_type_safe_database.mpl
Normal file
4
examples/10_type_safe_database.mpl
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
User ≜ {name: String, age: ℕ∣age>0, email: String}
|
||||
query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ {
|
||||
↯"Invalid user" ⟹ ⊥
|
||||
}
|
||||
150
glyph-escapes.md
Normal file
150
glyph-escapes.md
Normal file
|
|
@ -0,0 +1,150 @@
|
|||
# MPL Glyph Escape Sequences
|
||||
|
||||
This document provides the authoritative mapping between ASCII escape sequences and UTF-8 glyphs for the Mathematical Programming Language (MPL).
|
||||
|
||||
## Core Mathematical Symbols
|
||||
|
||||
### Greek Letters (Variables)
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\alpha` | U+03B1 | α | Variable |
|
||||
| `\beta` | U+03B2 | β | Variable |
|
||||
| `\gamma` | U+03B3 | γ | Variable |
|
||||
| `\delta` | U+03B4 | δ | Variable |
|
||||
| `\epsilon` | U+03B5 | ε | Variable |
|
||||
| `\zeta` | U+03B6 | ζ | Variable |
|
||||
| `\eta` | U+03B7 | η | Variable |
|
||||
| `\theta` | U+03B8 | θ | Variable |
|
||||
| `\iota` | U+03B9 | ι | Variable |
|
||||
| `\kappa` | U+03BA | κ | Variable |
|
||||
| `\lambda` or `\lam` | U+03BB | λ | Lambda/Function |
|
||||
| `\mu` | U+03BC | μ | Variable |
|
||||
| `\nu` | U+03BD | ν | Variable |
|
||||
| `\xi` | U+03BE | ξ | Variable |
|
||||
| `\omicron` | U+03BF | ο | Variable |
|
||||
| `\pi` | U+03C0 | π | Variable/Constant |
|
||||
| `\rho` | U+03C1 | ρ | Variable |
|
||||
| `\sigma` | U+03C3 | σ | Variable |
|
||||
| `\tau` | U+03C4 | τ | Variable |
|
||||
| `\upsilon` | U+03C5 | υ | Variable |
|
||||
| `\phi` | U+03C6 | φ | Variable |
|
||||
| `\chi` | U+03C7 | χ | Variable |
|
||||
| `\psi` | U+03C8 | ψ | Variable |
|
||||
| `\omega` | U+03C9 | ω | Variable |
|
||||
|
||||
### Set Theory
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\emptyset` | U+2205 | ∅ | Empty set |
|
||||
| `\union` or `\cup` | U+222A | ∪ | Set union |
|
||||
| `\intersect` or `\cap` | U+2229 | ∩ | Set intersection |
|
||||
| `\subset` | U+2282 | ⊂ | Proper subset |
|
||||
| `\supset` | U+2283 | ⊃ | Proper superset |
|
||||
| `\in` | U+2208 | ∈ | Element of |
|
||||
| `\notin` | U+2209 | ∉ | Not element of |
|
||||
| `\subseteq` | U+2286 | ⊆ | Subset or equal |
|
||||
| `\supseteq` | U+2287 | ⊇ | Superset or equal |
|
||||
|
||||
### Logic
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\and` or `\wedge` | U+2227 | ∧ | Logical and |
|
||||
| `\or` or `\vee` | U+2228 | ∨ | Logical or |
|
||||
| `\not` or `\neg` | U+00AC | ¬ | Logical not |
|
||||
| `\implies` or `\Rightarrow` | U+27F9 | ⟹ | Implication |
|
||||
| `\iff` or `\Leftrightarrow` | U+27FA | ⟺ | If and only if |
|
||||
| `\forall` | U+2200 | ∀ | Universal quantifier |
|
||||
| `\exists` | U+2203 | ∃ | Existential quantifier |
|
||||
|
||||
### Operations
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\times` | U+00D7 | × | Multiplication |
|
||||
| `\div` | U+00F7 | ÷ | Division |
|
||||
| `\ast` | U+2217 | ∗ | Generic operator |
|
||||
| `\circ` | U+2218 | ∘ | Function composition |
|
||||
|
||||
### Relations
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\neq` or `\ne` | U+2260 | ≠ | Not equal |
|
||||
| `\leq` or `\le` | U+2264 | ≤ | Less than or equal |
|
||||
| `\geq` or `\ge` | U+2265 | ≥ | Greater than or equal |
|
||||
| `\approx` | U+2248 | ≈ | Approximately equal |
|
||||
| `\sim` | U+223C | ∼ | Similar to |
|
||||
|
||||
### Special Symbols
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\leftarrow` or `\gets` | U+2190 | ← | Assignment |
|
||||
| `\coloneq` | U+225C | ≜ | Definition |
|
||||
| `\rightarrow` or `\to` | U+2192 | → | Function type |
|
||||
|
||||
## Effect Extensions
|
||||
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\raise` | U+21AF | ↯ | Raise exception |
|
||||
| `\handle` | U+21B4 | ↴ | Handle exception |
|
||||
| `\parallel` | U+2016 | ‖ | Parallel composition |
|
||||
| `\lceil` | U+2308 | ⌈ | Atomic section start |
|
||||
| `\rceil` | U+2309 | ⌉ | Atomic section end |
|
||||
| `\oplus` | U+2295 | ⊕ | Allocate resource |
|
||||
| `\ominus` | U+2296 | ⊖ | Release resource |
|
||||
| `\module` | U+1D49C | 𝓜 | Module declaration |
|
||||
| `\Leftarrow` | U+21D0 | ⇐ | Import |
|
||||
| `\Rightarrow` | U+21D2 | ⇒ | Export |
|
||||
| `\send` | U+21C0 | ⇀ | Send (network) |
|
||||
| `\receive` | U+21BD | ↽ | Receive (network) |
|
||||
|
||||
## Additional Operators
|
||||
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\langle` | U+27E8 | ⟨ | Choice type/angle bracket left |
|
||||
| `\rangle` | U+27E9 | ⟩ | Choice type/angle bracket right |
|
||||
| `\path` | U+1F5AB | 🖫 | File path prefix |
|
||||
| `\up` | U+21E1 | ⇡ | Stream position up |
|
||||
| `\down` | U+21E3 | ⇣ | Stream position down |
|
||||
| `\swap` | U+21C6 | ⇆ | Atomic swap |
|
||||
| `\llangle` | U+27EA | ⟪ | Deep update path start |
|
||||
| `\rrangle` | U+27EB | ⟫ | Deep update path end |
|
||||
| `\ulcorner` | U+231C | ⌜ | Code quotation start |
|
||||
| `\urcorner` | U+231D | ⌝ | Code quotation end |
|
||||
| `\llcorner` | U+231E | ⌞ | Code evaluation start |
|
||||
| `\lrcorner` | U+231F | ⌟ | Code evaluation end |
|
||||
| `\query` | U+003F | ? | Introspection |
|
||||
| `\break` | U+2A08 | ⧈ | Breakpoint |
|
||||
| `\trace` | U+270E | ✎ | Trace/log |
|
||||
| `\delay` | U+23F2 | ⏲ | Delay |
|
||||
| `\periodic` | U+27F3 | ⟳ | Periodic task |
|
||||
| `\lbracket` | U+3014 | 〔 | RAII scope start |
|
||||
| `\rbracket` | U+3015 | 〕 | RAII scope end |
|
||||
|
||||
## Type System Symbols
|
||||
|
||||
| ASCII Escape | Unicode | Glyph | Usage |
|
||||
|-------------|---------|-------|-------|
|
||||
| `\nat` or `\N` | U+2115 | ℕ | Natural numbers |
|
||||
| `\int` or `\Z` | U+2124 | ℤ | Integers |
|
||||
| `\rat` or `\Q` | U+211A | ℚ | Rational numbers |
|
||||
| `\real` or `\R` | U+211D | ℝ | Real numbers |
|
||||
| `\complex` or `\C` | U+2102 | ℂ | Complex numbers |
|
||||
| `\bool` or `\B` | U+1D539 | 𝔹 | Booleans |
|
||||
| `\bot` | U+22A5 | ⊥ | Bottom type |
|
||||
|
||||
## Usage Notes
|
||||
|
||||
1. **Input methods:**
|
||||
- Direct Unicode input (recommended for supported editors)
|
||||
- ASCII escape sequences (for compatibility)
|
||||
- Editor-specific shortcuts (e.g., Ctrl+Alt+g → γ)
|
||||
|
||||
2. **Lexer behavior:**
|
||||
- Escapes are processed during tokenization
|
||||
- Unknown escapes result in compilation error
|
||||
- Mixed Unicode/ASCII in same file is allowed
|
||||
|
||||
3. **Pretty-printing:**
|
||||
- Always outputs Unicode glyphs (never escapes)
|
||||
- Configurable fallback to ASCII for terminals without Unicode support
|
||||
275
math_prog_lang.md
Normal file
275
math_prog_lang.md
Normal file
|
|
@ -0,0 +1,275 @@
|
|||
# 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 `}`
|
||||
|
||||
### 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.
|
||||
13
precedence.csv
Normal file
13
precedence.csv
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
Level,Operators,Associativity,Description
|
||||
9,function application,left,Function call f(x) or f x
|
||||
8,"↯ ✎ ? ⧈ ⏲ (prefix)",right,Unary prefix operators
|
||||
7,∘,left,Function composition
|
||||
6,× ÷ ∗,left,Multiplication and division
|
||||
5,+ -,left,Addition and subtraction
|
||||
4,= ≠ < > ≤ ≥ ≈ ∼,non-associative,Comparison operators
|
||||
3,∧,left,Logical AND
|
||||
2,∨,left,Logical OR
|
||||
1,⟹,right,Implication
|
||||
0,←,right,Assignment
|
||||
-1,‖,left,Parallel composition
|
||||
-2,;,left,Statement sequencing
|
||||
|
Loading…
Add table
Add a link
Reference in a new issue