Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573pub type Any { any {A : Type} (value: A)}pub class Functor (F: Type -> Type) { def map (f: A -> B) : (F A) -> F B}pub class FromListLiteral (L : Type -> Type := List) { def cons (a : A) (L A) : L A def empty : L A }/// Hetrogenous addition classpub class HAdd A B C { def add : A -> B -> C}/// Homogenous additionpub class Add A { def add : A -> A -> A}pub instance [HAdd A A A] Add A { def add (a b : A) : A := HAdd.add a b}pub instance [Add A] HAdd A A A { def add (a b : A) : A := Add.add a b}/// Heterogeneous multiplicationpub class HMul A B C { def mul : A -> B -> C}/// Subtractionpub class Sub A { def sub : A -> A -> A}pub class Div A { def div : A -> A -> A}pub infix (+) := HAdd.addpub infix (/) := Div.divpub infix (*) := HMul.mulpub infix (-) := Sub.subpub class [Functor F] Applicative (F: Type -> Type) { def pure : A -> F A def apply : F (A -> B) -> F A -> F B}pub class [Applicative M] Monad (M: Type -> Type) { def bind (a : M A) (f : A -> M B) : M B def pure : A -> M A}pub infix (>>=) := Monad.bind/// Dual of `Monad`: `extract` pulls the value out of a context; `duplicate`/// and `extend` push the context inwards. All three are required -- the usual/// `extend f = map f . duplicate` default would need a `Functor` superclass/// constraint, and a superclass constraint gets no slot in the dictionary.pub class Comonad (W : Type -> Type) { def extract (W A) : A def duplicate (W A) : W (W A) def extend (f : W A -> B) (W A) : W B}/// State monad: thread state S through a monad M./// Single-param class (M only) — S is an implicit forall variable,/// like Map's K/V, so `KnownInstances` can key on the monad's concrete/// head (e.g. `State`), not a variable.pub class MonadState (M : Type -> Type) { def get : M S def set (s : S) : M Unit def modify_get (f : S -> Pair S A) : M A /// Modify the state and return unit def modify (f : S -> S) : M Unit := modify_get (fn s => Pair.pair (f s) unit) /// Get the state, apply a function, and return the result def get_map (f : S -> A) : M A := modify_get (fn s => Pair.pair s (f s))}/// Lift computations from monad `m` into monad `n`pub class MonadLift (m : Type -> Type) (n : Type -> Type) { def monad_lift (a : m A) : n A}/// Transitive monad lift. The reflexive instance (lifting from/// `m` to `m`) is the identity below; for other pairs, provide/// an instance that delegates to `MonadLift`.pub class MonadLiftT (m : Type -> Type) (n : Type -> Type) { def monad_lift_t (a : m A) : n A}/// Reflexive: lifting from m to m is the identitypub instance MonadLiftT m m { def monad_lift_t (a : m A) : m A := a}pub type Void {}/// UTF8 stringpub type String { of_bytes (List U8)}/// UTF8 code pointpub type Char { of_bytes (List U8)}pub class ToString A { def to_string (a : A) : String}/// Primitive number typespub type I64 {}pub type I32 {}pub type I16 {}pub type I8 {}pub type U64 {}pub type U32 {}pub type U16 {}pub type U8 {}pub type F64 {}pub type F32 {}/// Opaque C pointer for the `#[extern "c"]` FFI. A `Ptr` value is the/// raw machine word under every backend; never match, compare or print/// one (the `FdStream` convention, std/src/stream.mo).pub type Ptr {}/// The NULL pointer — `SSL_set_verify`'s callback argument is the first/// caller (motes/tls).#[native "ptr_null"]pub def Ptr.null : Ptr/// The fixed `(void*)-1` sentinel (SQLite's `SQLITE_TRANSIENT` is one/// user). It takes no input, so unlike a general I64-to-Ptr conversion it/// cannot produce an arbitrary address.#[native "ptr_minus_one"]pub def Ptr.minus_one : Ptrpub type Unit { unit}// TODO: the `open ... {...}` filters below are hand-verified against// bare usage across the WHOLE codebase, not just this file — prelude's// own `open`s are unconditionally chained into every other file's scope// (see `GlobalScopeData::from_module`), so a filter based on what THIS// file alone references (what `monad-rs organize-imports` computes by// default) would under-count and break other files that rely on these// names being ambiently bare (e.g. `unit`, `not`, `err`). Re-verify by// hand if this file's `open`s ever change.open Unit {unit}pub type Bool { true, false}open Bool {and, false, not, or, true}/// Trivially true proposition (unit in Prop)pub type True : Prop { trivial}open True {trivial}/// Propositional equality: Eq A a b lives in Prop (Sort 0)pub type Eq (A : Sort 1) (a : A) (b : A) : Prop { refl : Eq A a a}/// Native J eliminator for propositional equality#[native "eq_rec"]pub def Eq.rec (A : Sort 1) (a : A) (P : (b : A) -> Eq A a b -> Sort 1) (h : P a (Eq.refl a)) (b : A) (e : Eq A a b) : P b e/// Equalspub class BEq A { def beq : A -> A -> Bool}pub instance BEq Bool { def beq (a b : Bool) : Bool := if a then b else (Bool.not b)}// TODO Constraint resolving// def BEq.not_beq [BEq A] (a b : A) : Bool := not (a == b)pub infix (==) := BEq.beq// infix (!=) := BEq.not_beq/// Ordered comparisonpub class BOrd A { def lt (a b : A) : Bool def gt (a b : A) : Bool // TODO fix default implementations // def lte (a b : A) : Bool := not (BOrd.gt a b) // def gte (a b : A) : Bool := not (BOrd.lt a b)}pub infix (<) := BOrd.lt// TODO// infix (<=) := BOrd.lte// infix (>=) := BOrd.gtepub infix (>) := BOrd.gtpub instance BOrd Bool { def lt (a b : Bool) : Bool := if a then false else b def gt (a b : Bool) : Bool := if a then Bool.not b else false}/// Hashable: produce a hash value for an element.pub class Hashable A { def hash (a : A) : U64}pub type DefaultValue (A: Type) (default : A) { default}pub def Bool.not (b : Bool) : Bool := if b then false else truepub def Bool.and (a b : Bool) : Bool := if a then b else falsepub infix (&&) := Bool.andpub def Bool.or (a b : Bool) : Bool := if a then true else bpub infix (||) := Bool.orpub type Result E A { ok (a: A), err (e: E)}/// Whether `r` is `Result.ok` -- for a caller that checks an effect's/// outcome (a test asserting a write landed) without needing its value.pub def Result.is_ok {E A : Type} (r : Result E A) : Bool := match r { Result.ok _ => true, Result.err _ => false }pub type Pair A B { pair (first : A) (second : B)}/// The product comonad: `E` is a read-only environment, so `extract` is the/// second component and `duplicate` copies it into both halves.pub instance {E : Type} Comonad (Pair E) { def extract (p : Pair E A) : A := match p { Pair.pair _ a => a } def duplicate (p : Pair E A) : Pair E (Pair E A) := match p { Pair.pair e a => Pair.pair e (Pair.pair e a) } def extend (f : Pair E A -> B) (p : Pair E A) : Pair E B := match p { Pair.pair e a => Pair.pair e (f (Pair.pair e a)) }}/// Dependent pair: the second component's TYPE may depend on the first/// component's VALUE -- e.g. `Sigma Nat (fn n => Vec n A)` pairs a/// length with a vector of exactly that length.////// The non-dependent `Pair A B` above is the special case/// `Sigma A (fn _ => B)`. Both are kept: recovering `fn _ => B` at every/// tuple literal would need higher-order unification, so `Pair` remains/// what the tuple syntax desugars to.////// `snd`'s declared type applies `B` to the EARLIER field `fst`. That/// shape was unrepresentable until constructor parameter lists were made/// to bind; before that the mention dangled and was silently generalized/// into an unrelated implicit.pub type Sigma (A : Type) (B : A -> Type) { dpair (fst : A) (snd : B fst)}/// Existential quantification -- `Sigma` restricted to a `Prop`-valued/// family, so the pair itself lands in `Prop`.////// Declared separately rather than defined as a `Sigma` because there is/// no universe polymorphism yet: `Sigma A B` is unconditionally in/// `Type` (`Sort 1`), so an `Exists` built from it would lose the `Prop`/// discipline. Merging the two is for when universe levels become/// variables.pub type Exists (A : Type) (P : A -> Prop) : Prop { intro (a : A) (proof : P a)}/// First projection. Non-dependent, so ordinary match typing suffices.////// NOTE the prelude ships no `Sigma` VALUE and no test that builds one./// Constructing `Sigma.dpair a b` requires `B a` to reduce, i.e./// conversion checking: the self-hosted checker has it (beta + delta,/// lang/src/typecheck/whnf.mo) but the Rust host does not. Construction/// is covered by source-string tests in/// lang/src/tests/typecheck_examples_tests.mo, which run through the/// self-hosted checker only.////// The second projection `Sigma.snd (p : Sigma A B) : B (Sigma.fst p)`/// is deliberately absent: checking it needs the arm's expected type to/// see `p` refined to `Sigma.dpair a b` (scrutinee refinement), and then/// `Sigma.fst (Sigma.dpair a b)` reduced away by iota. Neither checker/// does the refinement step today -- `p` stays a variable, so iota has/// no constructor to fire on. See plans/type-system/sigma-types.md.pub def Sigma.fst {A : Type} {B : A -> Type} (p : Sigma A B) : A := match p { Sigma.dpair a _ => a }open Result {err, ok}pub type Option A { some (a: A), none}open Option {none, some}pub def Option.get_or_default (default : A) (self : Option A) : A := match self { some a => a, none => default }pub type Nat { zero, succ (n : Nat)}pub def Nat.add (a b : Nat) : Nat := match a { zero => b, succ n => Nat.succ (Nat.add n b) }pub def Nat.sub (a b : Nat) : Nat := match b { zero => a, succ n => match a { zero => Nat.zero, succ m => Nat.sub m n } }pub def Nat.mul (a b : Nat) : Nat := match a { zero => Nat.zero, succ n => Nat.add b (Nat.mul n b) }pub def Nat.eq (a b : Nat) : Bool := match a { zero => match b { zero => true, succ _ => false }, succ n => match b { zero => false, succ m => Nat.eq n m } }pub instance BEq Nat { def beq (a b : Nat) : Bool := Nat.eq a b}pub instance Add Nat { def add (a b : Nat) : Nat := Nat.add a b}pub instance Sub Nat { def sub (a b : Nat) : Nat := Nat.sub a b}pub def Lens [Functor F] {F : Type -> Type} (S: Type) (T: Type) (A: Type) (B : Type) : Type := (A -> F B) -> S -> F Tpub type List A { empty, cons (a : A) (List A) : List A}pub instance FromListLiteral List { def cons (a: A) (l : List A) : List A := List.cons a l def empty : List A := List.empty}pub def List.is_empty (self : List A) : Bool := match self { empty => true, cons a tail => false, _ => true }pub def List.append (a b : List A) : List A := match a { empty => b, cons el_a tail => List.cons el_a (List.append tail b), _ => b }/// Append b to value apub class Append A { def append (a b : A) : A}pub infix (++) := Append.appendpub def List.first (self : List A) : Option A := match self { empty => none, cons a tail => some a, _ => none }pub def List.last (self : List A) : Option A := match self { empty => none, cons a tail => if List.is_empty tail then some a else List.last tail, _ => none }pub def List.flatten (self : List (List A)) : List A := match self { empty => List.empty, cons list tail => List.append list (List.flatten tail), _ => List.empty }pub def List.tail (l : List A) : List A := match l { empty => List.empty, cons a tail => tail, _ => List.empty }pub def List.map (f : A -> B) (self: List A) : List B := match self { empty => List.empty, cons a tail => List.cons (f a) (List.map f tail), _ => List.empty }pub instance Functor List { // `List.map` (not the recursive `Functor.map`) -- a match-arm PATTERN- // bound variable (`tail`, from `cons a tail => ...`) is never added to // `env` by `resolve_class_call_term`'s term walker (`lang/scope.mo`, // only `Term.lam`-introduced bindings are, see its own doc comment) -- // a distinct gap from the bare-local-var one already fixed, caught by // the new fail-fast check (`no instance found for 'Functor.map'`) this // instance's own recursive call had been silently hitting. `List.map` // (just above) is the identical concrete implementation, already // correct and non-generic -- reuse it instead of chasing this gap here. def map (f : A -> B) (self: List A) : List B := match self { empty => List.empty, cons a tail => List.cons (f a) (List.map f tail), _ => List.empty }}/// A length-indexed vector: Vec len A is a list of exactly len elements of type Apub type Vec (len : Nat) A { nil : Vec Nat.zero A, cons (head : A) (tail : Vec len A) : Vec (Nat.succ len) A}pub def fun_apply (f : A -> B) (a : A) : B := f apub infix (<|) := fun_applypub def apply_fun (a : A) (f : A -> B) : B := f apub infix (|>) := apply_fun/// Indexed monad: M I J A/// I = initial index, J = final index, A = valuepub class IndexedMonad (M : Type -> Type -> Type -> Type) { def pure (a : A) : M I I A def bind (a : M I J A) (f : A -> M J K B) : M I K B /// Map across the value (preserving indices) def map (f : A -> B) (ma : M I J A) : M I J B := bind ma (fn a => pure (f a)) /// Sequence two actions, discarding the first value def and_then (first : M I J A) (second : M J K B) : M I K B := bind first (fn _ => second) /// Lift a pure value into the indexed monad at any index def lift (a : A) : M I I A := pure a}/// Any `IndexedMonad M` at equal indices (`M I I`) is a regular `Monad`./// This bridge instance provides `Monad (M I I)` for every `IndexedMonad M`,/// enabling do-notation for indexed monads without type-checker changes.pub instance {I : Type} [IndexedMonad M] Monad (M I I) { def pure (a : A) : M I I A := IndexedMonad.pure a def bind (a : M I I A) (f : A -> M I I B) : M I I B := IndexedMonad.bind a f}/// Indexed state monad: thread state S through an indexed monad M./// State operations preserve the index (M I I), so they can be/// sequenced in any position without changing the protocol state./// Single-param class (M only) — S is implicit forall, same as/// `MonadState` above.pub class IndexedMonadState (M : Type -> Type -> Type -> Type) { def get : M I I S def set (s : S) : M I I Unit def modify_get (f : S -> Pair S A) : M I I A}/// Lift computations from indexed monad `m` into indexed monad `n`pub class IndexedMonadLift (m : Type -> Type -> Type -> Type) (n : Type -> Type -> Type -> Type) { def monad_lift (a : m I J A) : n I J A}// The cubical interval and its operations (univalence.md Stages 1-5),// as BODY-LESS marker defs inside a `with Cubical` block. The// `#[cubical "..."]` MARKER, never the bare spelling, is what binds:// `build_scope_def` (lang/src/scope.mo) enters the def's prefixed name// into `ScopeData.cubical_prims`, and the checker rewrites a resolved// reference to that name into the `Term.cubical` it stands for. The// signatures carry name resolution and type the UNDER-APPLIED case;// the checker's cubical probe handles every saturated one. `I` is// NEVER an inductive: one case split on a dimension destroys// univalence.with Cubical { #[cubical "interval"] def I : Type #[cubical "i0"] def i0 : Cubical.I #[cubical "i1"] def i1 : Cubical.I #[cubical "ineg"] def ineg (i : Cubical.I) : Cubical.I #[cubical "imeet"] def imeet (i : Cubical.I) (j : Cubical.I) : Cubical.I #[cubical "ijoin"] def ijoin (i : Cubical.I) (j : Cubical.I) : Cubical.I #[cubical "pathp"] def PathP (A : Cubical.I -> Type) (a : A Cubical.i0) (b : A Cubical.i1) : Type #[cubical "transp"] def transp (A : Cubical.I -> Type) (a : A Cubical.i0) : A Cubical.i1 #[cubical "face_eq0"] def face_eq0 (i : Cubical.I) : Cubical.I #[cubical "face_eq1"] def face_eq1 (i : Cubical.I) : Cubical.I #[cubical "is_one"] def is_one (i : Cubical.I) : Type #[cubical "hcomp"] def hcomp (A : Type) (phi : Cubical.I) (u : Cubical.I -> Cubical.is_one phi -> A) (u0 : A) : A}