From bc29dfe50a38ca349982ee2afa998a8aaf3a204c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Mon, 27 Apr 2026 21:34:34 +0200 Subject: [PATCH] docs: Update documentation with new features --- AGENTS.md | 52 ++++++++++++++++++++++- docs/src/dependent-types.md | 14 +++---- docs/src/getting-started.md | 36 ++++++++-------- docs/src/inductive-types.md | 4 +- docs/src/instances.md | 4 +- docs/src/io-monad.md | 44 +++++++++++++++++++- docs/src/modules.md | 8 ++-- docs/src/reference.md | 82 ++++++++++++++++++++++++++----------- init/io.mo | 5 +++ 9 files changed, 188 insertions(+), 61 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 5c49b2c..f6c0684 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -108,6 +108,56 @@ def factorial (n: I64) : I64 := // With implicit parameters def identity {A : Type} (x: A) : A := x + +// Do block syntax (alternative to :=) +def greet (name : String) : IO Unit { + println name +} + +// Do block with multiple statements +def multi_step : IO Unit { + println "Step 1"; + let value := 42 + println "Done" +} +``` + +### Do Notation + +Do notation provides syntactic sugar for monadic operations. It can be used with the `do { ... }` syntax or directly in function definitions using `{ ... }`. + +```monad +// Standard do notation +def example : IO Unit := do { + x <- get_value + let y := x + 1 + return y +} + +// Do block in function definition (equivalent) +def example : IO Unit { + x <- get_value + let y := x + 1 + return y +} +``` + +Do blocks support three kinds of statements: + +| Statement | Syntax | Desugars To | +|-----------|--------|-------------| +| Bind | `x <- monadic_expr` | `Monad.bind monadic_expr (fn x => ...)` | +| Let | `let x := value` | `let x := value in ...` | +| Return | `return value` | `Monad.pure value` | +| Expression | `expr` | `Monad.bind expr (fn _ => ...)` | + +Multiple expressions must be separated by semicolons: + +```monad +def multi : IO Unit { + println "first"; + println "second" +} ``` ### Lambda Expressions @@ -225,4 +275,4 @@ def function_name (args: Types) : ReturnType - Lowercase identifiers for functions/variables - Uppercase for types/type classes - Prefer descriptive names -- Comment with `//` +- Comment with `//` (never `--`) diff --git a/docs/src/dependent-types.md b/docs/src/dependent-types.md index 5a6164d..b2a53ad 100644 --- a/docs/src/dependent-types.md +++ b/docs/src/dependent-types.md @@ -17,8 +17,8 @@ The `{A : Type}` syntax introduces implicit arguments that are inferred by the t ```monad def identity {A : Type} (x : A) : A := x --- Called without specifying A: -def result := identity 42 -- A is inferred as I64 +// Called without specifying A: +def result := identity 42 // A is inferred as I64 ``` ## Type Annotations @@ -34,7 +34,7 @@ def x : I64 := 42 The `_` placeholder (Hole) tells the type checker to infer the type: ```monad -def x := _ -- Type will be inferred +def x := _ // Type will be inferred ``` ## Universe Levels @@ -42,9 +42,9 @@ def x := _ -- Type will be inferred `Type` represents the universe of types (universe 0). You can also use higher universes: ```monad -Type -- Universe 0 -Type 1 -- Universe 1 -Type 2 -- Universe 2 +Type // Universe 0 +Type 1 // Universe 1 +Type 2 // Universe 2 ``` ## Prop @@ -65,7 +65,7 @@ type Result E A { err (e : E) } --- Result takes type parameters E and A +// Result takes type parameters E and A def success : Result String I64 := ok 42 ``` diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 634fe9f..c09e598 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -44,10 +44,10 @@ Every Monad program follows this basic structure: Monad supports explicit type annotations. The basic types include: ```monad -def x : I64 := 42 -- 64-bit integer -def name : String := "Monad" -- String -def flag : Bool := true -- Boolean -def nothing : Unit := unit -- Unit type (single value) +def x : I64 := 42 // 64-bit integer +def name : String := "Monad" // String +def flag : Bool := true // Boolean +def nothing : Unit := unit // Unit type (single value) ``` You can also use other integer types: `I32`, `U64`, `U32`, `U16`, `U8`. @@ -57,13 +57,13 @@ You can also use other integer types: `I32`, `U64`, `U32`, `U16`, `U8`. Functions are defined using `def` with curried parameters: ```monad --- Simple function +// Simple function def double (n : I64) : I64 := n + n --- Multi-parameter function (curried) +// Multi-parameter function (curried) def add (a : I64) (b : I64) : I64 := a + b --- With type annotation on the result +// With type annotation on the result def greeting : String := "Hello" ``` @@ -72,7 +72,7 @@ def greeting : String := "Hello" Function application is written with spaces: ```monad -def result := double (add 3 4) -- result = 14 +def result := double (add 3 4) // result = 14 ``` ### Anonymous Functions (Lambdas) @@ -96,7 +96,7 @@ def isZero (n : Nat) : Bool := succ _ => false } --- Pattern matching on booleans +// Pattern matching on booleans def not (b : Bool) : Bool := match b { true => false, @@ -141,18 +141,18 @@ Monad supports infix operators with defined precedence: use init use math -def result : I64 := 3 + 4 * 2 -- 11 (multiplication binds tighter) +def result : I64 := 3 + 4 * 2 // 11 (multiplication binds tighter) ``` Built-in operators include: -- `(+)` -- Addition (via `I64.add`) -- `(*)` -- Multiplication (via `HMul.mul`) -- `(++)` -- List append -- `(&&)` -- Boolean and -- `(||)` -- Boolean or -- `(>>=)` -- Monad bind -- `(<|)` -- Function application (reverse) -- `(|>)` -- Pipeline (forward application) +- `(+)` // Addition (via `I64.add`) +- `(*)` // Multiplication (via `HMul.mul`) +- `(++)` // List append +- `(&&)` // Boolean and +- `(||)` // Boolean or +- `(>>=)` // Monad bind +- `(<|)` // Function application (reverse) +- `(|>)` // Pipeline (forward application) ## Summary diff --git a/docs/src/inductive-types.md b/docs/src/inductive-types.md index a87a420..c3c64b0 100644 --- a/docs/src/inductive-types.md +++ b/docs/src/inductive-types.md @@ -65,8 +65,8 @@ Monad supports list literal syntax `[a, b, c]`, which desugars using the `FromLi ```monad def nums := [1, 2, 3] --- Desugars to: --- FromListLiteral.cons 1 (FromListLiteral.cons 2 (FromListLiteral.cons 3 FromListLiteral.empty)) +// Desugars to: +// FromListLiteral.cons 1 (FromListLiteral.cons 2 (FromListLiteral.cons 3 FromListLiteral.empty)) ``` ## Result Type diff --git a/docs/src/instances.md b/docs/src/instances.md index 4482f86..08eb9c0 100644 --- a/docs/src/instances.md +++ b/docs/src/instances.md @@ -55,7 +55,7 @@ Type class parameters can be implicit and auto-resolved: ```monad def doubleList [Add A] (xs : List A) : List A := - -- Uses Add.add through instance resolution + // Uses Add.add through instance resolution ... ``` @@ -75,7 +75,7 @@ Once an instance is defined, its methods are available through the class: use init use math -def result : I64 := 3 + 4 -- Uses I64.add via Add instance +def result : I64 := 3 + 4 // Uses I64.add via Add instance ``` ## Summary diff --git a/docs/src/io-monad.md b/docs/src/io-monad.md index 21f67f7..5ca1c13 100644 --- a/docs/src/io-monad.md +++ b/docs/src/io-monad.md @@ -51,7 +51,9 @@ instance Monad IO { ## Do Notation -The `do` block sequences IO actions: +The `do` block sequences IO actions. Two equivalent syntaxes are available: + +### Standard `do { ... }` syntax ```monad use io @@ -60,11 +62,49 @@ open IO def greet : IO Unit := do { println "Enter your name:" - // name <- getLine -- Note: getLine not yet implemented + // name <- getLine // Note: getLine not yet implemented println "Hello!" } ``` +### Inline do block syntax + +Functions can use `{ ... }` directly instead of `:= do { ... }`: + +```monad +use io +open IO + +def greet : IO Unit { + println "Enter your name:" + println "Hello!" +} + +def greetWithName (name : String) : IO Unit { + let greeting := "Hello, " ++ name + println greeting +} +``` + +### Do Block Statements + +| Statement | Syntax | Desugars To | +|-----------|--------|-------------| +| Bind | `x <- action` | `Monad.bind action (fn x => ...)` | +| Let | `let x := value` | `let x := value in ...` | +| Return | `return value` | `Monad.pure value` | +| Expression | `expr` | `Monad.bind expr (fn _ => ...)` | + +Multiple statements are separated by semicolons: + +```monad +def multiStep : IO Unit { + println "Step 1"; + let value := 42 + println "Step 2" +} +``` + ## Native Functions IO operations are implemented as native functions that call Rust code: diff --git a/docs/src/modules.md b/docs/src/modules.md index 2661b8c..95b268b 100644 --- a/docs/src/modules.md +++ b/docs/src/modules.md @@ -42,10 +42,10 @@ Now `println` is available directly instead of `IO.println`. The prelude opens several types by default: ```monad -open Unit -- makes `unit` available -open Bool -- makes `true`, `false` available -open Result -- makes `ok`, `err` available -open Option -- makes `some`, `none` available +open Unit // makes `unit` available +open Bool // makes `true`, `false` available +open Result // makes `ok`, `err` available +open Option // makes `some`, `none` available ``` ## Module Paths diff --git a/docs/src/reference.md b/docs/src/reference.md index a6f4922..262d47a 100644 --- a/docs/src/reference.md +++ b/docs/src/reference.md @@ -33,15 +33,15 @@ fn x => x + 1 ## Let Expressions ```monad --- Inline style +// Inline style let x := 10 in x + 1 --- Semicolon style +// Semicolon style let x := 10; let y := 20; in x + y --- With type annotation +// With type annotation let x : I64 := 10 in x + 1 ``` @@ -62,14 +62,35 @@ if condition then thenBranch else elseBranch ## Do Notation +Two equivalent syntaxes are available: + ```monad -do { +// Standard syntax +def example : IO Unit := do { + name <- action; + let x := value; + return value +} + +// Inline do block (equivalent) +def example : IO Unit { name <- action; let x := value; return value } ``` +### Statement Types + +| Statement | Syntax | Desugars To | +|-----------|--------|-------------| +| Bind | `x <- action` | `Monad.bind action (fn x => ...)` | +| Let | `let x := value` | `let x := value in ...` | +| Return | `return value` | `Monad.pure value` | +| Expression | `expr` | `Monad.bind expr (fn _ => ...)` | + +Multiple statements are separated by semicolons. + ## Struct Values ```monad @@ -110,13 +131,13 @@ infix (operator) := functionName | Operator | Precedence | Associativity | Function | |----------|------------|---------------|----------| -| `|>` | 5 | Left | `apply_fun` | -| `<|` | 5 | Right | `fun_apply` | +| `\|>` | 5 | Left | `apply_fun` | +| `<\|` | 5 | Right | `fun_apply` | | `>>=` | 10 | Right | `Monad.bind` | | `.` | 12 | Right | Dot macro (path) | | `<*>` | 15 | Left | `Applicative.apply` | -| `<|>` | 20 | Left | - | -| `||` | 25 | Right | `Bool.or` | +| `<\|>` | 20 | Left | - | +| `\|\|` | 25 | Right | `Bool.or` | | `&&` | 30 | Right | `Bool.and` | | `==`, `!=` | 40 | Left | - | | `++` | 50 | Right | `List.append` | @@ -127,25 +148,25 @@ infix (operator) := functionName ## Type Definitions ```monad --- Simple type +// Simple type type Bool { true, false } --- Type with parameters +// Type with parameters type Result E A { ok (a : A), err (e : E) } --- Type with constructors carrying data +// Type with constructors carrying data type Option A { some (a : A), none } --- Empty type +// Empty type type Void {} ``` @@ -161,12 +182,12 @@ struct Point { ## Class Definitions ```monad --- Simple class +// Simple class class Functor (F : Type -> Type) { def map (f : A -> B) : (F A) -> F B } --- Class with constraints +// Class with constraints class [Functor F] Applicative (F : Type -> Type) { def pure : A -> F A def apply : F (A -> B) -> F A -> F B @@ -176,13 +197,13 @@ class [Functor F] Applicative (F : Type -> Type) { ## Instance Definitions ```monad --- Simple instance +// Simple instance instance FromListLiteral List { def cons (a : A) (l : List A) : List A := List.cons a l def empty : List A := List.empty } --- Instance with constraints +// Instance with constraints instance [Add A] Add (List A) { def add (a b : List A) : List A := List.append a b } @@ -191,16 +212,27 @@ instance [Add A] Add (List A) { ## Function Definitions ```monad --- Basic function +// Basic function def add (a : I64) (b : I64) : I64 := a + b --- With implicit parameters +// With implicit parameters def identity {A : Type} (x : A) : A := x --- With constraints +// With constraints def double [Add A] (x : A) : A := HAdd.add x x --- Native function +// Do block syntax (alternative to :=) +def greet (name : String) : IO Unit { + println name +} + +// Do block with multiple statements +def multiStep : IO Unit { + println "Step 1"; + println "Step 2" +} + +// Native function @[native println] def IO.println (s : String) : IO Unit ``` @@ -208,13 +240,13 @@ def IO.println (s : String) : IO Unit ## Modules ```monad --- Import module +// Import module use io --- Open module (no prefix needed) +// Open module (no prefix needed) open IO --- Access by path +// Access by path IO.println "hello" ``` @@ -283,8 +315,8 @@ IO.println "hello" ### Pipeline -- `fun_apply (f : A -> B) (a : A) : B` -- `f <| a` -- `apply_fun (a : A) (f : A -> B) : B` -- `a |> f` +- `fun_apply (f : A -> B) (a : A) : B` — `f <| a` +- `apply_fun (a : A) (f : A -> B) : B` — `a |> f` ## CLI Usage diff --git a/init/io.mo b/init/io.mo index dfb72dd..3a10381 100644 --- a/init/io.mo +++ b/init/io.mo @@ -16,3 +16,8 @@ instance Monad IO { @[native println] def IO.println (s: String) : IO Unit + +// TODO support constraints +// def IO.println [ToString A] (a: A) : IO Unit := +// IO.println_raw (ToString.to_string a) + -- 2.51.2