Initial commit: Mathematical Programming Language (MPL)
A proof-of-concept parser demonstrating that programming languages can be built entirely from mathematical notation, enabling cognitive universality in computing. MPL replaces English keywords with mathematical symbols, making programming accessible to the 80% of humanity who don't speak English. Every design decision follows the Fatima Test: "Will this make sense to a 10-year-old who doesn't speak English?" Current implementation: - Complete ANTLR 4 grammar with 70+ mathematical operators - Parser supporting all major programming paradigms - Zero grammar ambiguities - ASCII escape sequences for every Unicode symbol This release contains: - Core parser implementation - Grammar specification - Example programs - Comprehensive documentation - Whitepaper outlining the vision Note: This is a parser-only proof of concept. Programs can be parsed but not executed. The interpreter and runtime are future work.
This commit is contained in:
developtheweb@protonmail.com
commit
3cf435b41e
43 changed files with 5528 additions and 0 deletions
281
math_prog_lang.md
Normal file
281
math_prog_lang.md
Normal file
|
|
@ -0,0 +1,281 @@
|
|||
# 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.
|
||||
Loading…
Add table
Add a link
Reference in a new issue