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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660use lib {}// Bool tests#[test]def test_bool_true : Bool := if true then true else false#[test]def test_bool_false : Bool := if false then false else true#[test]def test_bool_not_true : Bool := if not true then false else true#[test]def test_bool_not_false : Bool := if not false then true else false#[test]def test_bool_and : Bool := true && true#[test]def test_bool_and_false : Bool := if true && false then false else true#[test]def test_bool_or : Bool := if false || true then true else false#[test]def test_bool_or_false : Bool := if false || false then false else true// Numeric literal tests#[test]def test_hex_literal_i64 : Bool := 0xFF == 255#[test]def test_hex_literal_u32_suffix : Bool := 0xBADBEEFu32 == 195935983u32#[test]def test_hex_literal_negative : Bool := -0x10 == -16#[test]def test_hex_literal_uppercase_prefix : Bool := 0XCAFE == 51966// I64 tests#[test]def test_i64_add : Bool := 1 + 2 == 3#[test]def test_i64_sub : Bool := 5 - 3 == 2#[test]def test_i64_mul : Bool := 4 * 3 == 12#[test]def test_i64_div : Bool := 10 / 2 == 5#[test]def test_i64_add_zero : Bool := 0 + 0 == 0#[test]def test_i64_mul_zero : Bool := 42 * 0 == 0#[test]def test_i64_sub_order : Bool := 10 - 3 == 7// List testsdef empty_list : List I64 := List.empty#[test]def test_list_empty : Bool := match empty_list { empty => true, cons _ _ => false }#[test]def test_list_not_empty : Bool := not (List.is_empty [1, 2, 3])#[test]def test_get_0 : Bool := some 1 == (List.get 0 [1, 2, 3])#[test]def test_get_1 : Bool := some 2 == (List.get 1 [1, 2, 3])#[test]def test_get_2 : Bool := some 3 == (List.get 2 [1, 2, 3])#[test]def test_get_max : Bool := none == (List.get 4 [1, 2, 3])#[test]def test_get_neg1 : Bool := none == (List.get (-1) [1, 2, 3])#[test]def test_get_empty : Bool := none == (List.get 0 ([] : List I64))def first_of_empty : Option I64 := List.first List.empty#[test]def test_list_first_none : Bool := match first_of_empty { some _ => false, none => true }#[test]def test_list_single : Bool := not (List.is_empty [42])// Option testsdef none_opt : Option I64 := none#[test]def test_option_none : Bool := match none_opt { some _ => false, none => true }#[test]def test_option_get_or_default_some : Bool := Option.get_or_default 0 (some 42) == 42#[test]def test_option_get_or_default_none : Bool := Option.get_or_default 99 none_opt == 99// Result testsdef err_val : Result String I64 := err "fail"#[test]def test_result_err : Bool := match err_val { ok _ => false, err _ => true }// String tests#[test]def test_string_length : Bool := String.length "hello" == 5#[test]def test_string_empty_length : Bool := String.length "" == 0#[test]def test_string_is_empty : Bool := String.is_empty ""#[test]def test_string_not_empty : Bool := not (String.is_empty "hello")// Nat tests#[test]def test_nat_zero : Bool := match Nat.zero { zero => true, succ _ => false }#[test]def test_nat_succ : Bool := match Nat.succ Nat.zero { zero => false, succ n => match n { zero => true, succ _ => false } }// Operator tests#[test]def test_pipe_forward : Bool := 5 |> fn x => x + 1 |> fn x => x == 6def double (x : I64) : I64 := x * 2#[test]def test_apply_back : Bool := double 3 == 6// String slice/drop tests#[test]def test_string_slice_basic : Bool := String.slice "hello" 0 3 == "hel"#[test]def test_string_slice_middle : Bool := String.slice "hello" 1 3 == "ell"#[test]def test_string_slice_past_end : Bool := String.slice "hi" 0 10 == "hi"#[test]def test_string_drop_basic : Bool := String.drop 3 "hello" == "lo"#[test]def test_string_drop_none : Bool := String.drop 0 "hello" == "hello"#[test]def test_string_drop_all : Bool := String.drop 10 "hi" == ""// String starts_with tests#[test]def test_string_starts_with : Bool := String.starts_with "hel" "hello"#[test]def test_string_not_starts_with : Bool := not (String.starts_with "world" "hello")#[test]def test_string_starts_with_empty : Bool := String.starts_with "" "hello"#[test]def test_empty_starts_with_empty : Bool := String.starts_with "" ""// Unit tests#[test]def test_unit : Bool := match unit { unit => true }// Struct testsstruct Point { x: I64, y: I64,}#[test]def test_struct_construct_and_match : Bool := let pt : Point := { x := 1, y := 2 } in match pt { mk x y => true }#[test]def test_eq_in_plain_match : Bool := match List.cons 5 List.empty { cons x _ => x == 5 }#[test]def test_struct_eq_in_match : Bool := let pt : Point := { x := 1, y := 2 } in match pt { mk x y => x + y == 3 }#[test]def test_struct_wildcard : Bool := let pt : Point := { x := 10, y := 20 } in match pt { mk x _ => x == 10 }struct DefaultedBox { w: I64, h: I64 := 100,}#[test]def test_struct_default_value : Bool := let r : DefaultedBox := { w := 50 } in match r { mk w h => h == 100 }#[test]def test_struct_update_syntax : Bool := let p1 : Point := { x := 1, y := 2 } in let p2 : Point := { p1 with x := 10 } in match p2 { mk x y => x == 10 && y == 2 }// Optics/indexed-monad tests: `Lens`/`IndexedMonad` compiling at all is// already exercised for free by every OTHER test in this file (any real// checker regression in either would fail the whole file to load, not// just one isolated test) -- `optics_tests.mo` is where `Lens`'s actual// behavior (get/set/over) gets real, non-trivial runtime coverage.// Nat arithmetic tests#[test]def test_nat_add_zero : Bool := Nat.eq (Nat.add Nat.zero Nat.zero) Nat.zero#[test]def test_nat_add_one_one : Bool := let one := Nat.succ Nat.zero in let two := Nat.succ (Nat.succ Nat.zero) in Nat.eq (Nat.add one one) two#[test]def test_nat_sub_self : Bool := let one := Nat.succ Nat.zero in Nat.eq (Nat.sub one one) Nat.zero#[test]def test_nat_eq_false : Bool := Bool.not (Nat.eq Nat.zero (Nat.succ Nat.zero))// Vec dependent type tests#[test]def test_vec_nil_match : Bool := match Vec.nil { nil => true }#[test]def test_vec_nil_type : Bool := let v : Vec Nat.zero I64 := Vec.nil in match v { nil => true }#[test]def test_vec_cons_type : Bool := let v : Vec (Nat.succ Nat.zero) I64 := Vec.cons 42 Vec.nil in match v { cons h t => h == 42 }#[test]def test_vec_cons_pattern : Bool := let v : Vec (Nat.succ Nat.zero) I64 := Vec.cons 42 Vec.nil in match v { cons h t => h == 42 }#[test]def test_vec_cons_head : Bool := match Vec.cons 42 Vec.nil { cons h t => h == 42 }#[test]def test_vec_cons_tail_nil : Bool := match Vec.cons 42 Vec.nil { cons h t => match t { nil => true } }// Tuple tests//// No separate "construct only" tests here -- `test_tuple_pair_match`/// `test_tuple_triple_nested_match` below build the exact same tuples and// additionally verify their contents via `match`, so a construct-only// twin would check strictly less while covering nothing new.#[test]def test_tuple_pair_match : Bool := let t : Pair I64 Bool := (1, true) in match t { Pair.pair a b => (a == 1) && (b == true) }#[test]def test_tuple_triple_nested_match : Bool := let t : Pair I64 (Pair Bool String) := (1, true, "hi") in match t { Pair.pair a rest => match rest { Pair.pair b c => (a == 1) && (b == true) && (c == "hi") } }#[test]def test_tuple_parens_expr : Bool := let x := (1 + 2) in x == 3#[test]def test_tuple_nested_expr : Bool := let t : Pair I64 Bool := (1 + 1, 2 == 2) in match t { Pair.pair a b => (a == 2) && b }#[test]def test_match_wildcard : Bool := match Option.some 42 { some x => x == 42, _ => false }#[test]def test_match_wildcard_fallback : Bool := match Option.none { some x => false, _ => true }#[test]def test_match_wildcard_only : Bool := match Option.some 1 { _ => true }#[test]def test_match_wildcard_exact_first : Bool := match Option.some 5 { some x => x == 5, _ => false }#[test]def test_match_wildcard_discard_arg : Bool := match Option.some 99 { some _ => true, _ => false }// -- Id monad tests --#[test]def test_id_unwrap : Bool := match Id.run (Id.id true) { true => true, false => false }#[test]def test_id_unwrap_false : Bool := match Id.run (Id.id false) { true => false, false => true }// `Eq.refl`/`Sort`/`Prop`/`Type`-as-value tests below are genuinely// type-checking-only: `Eq`'s only inhabitant is `refl` and a `Sort`// value carries no runtime-observable structure at all (see// `lower_core_ir.rs`'s `IrLit::Sort` -- deliberately opaque), so there is// nothing further to inspect once construction/annotation type-checks;// `true` here is the correct body, not a stand-in for a missing// assertion, the same way a `#[test]` that only needs to confirm "this// compiles" legitimately can be.#[test]def test_eq_refl_apply : Bool := let refx := Eq.refl 1 in true#[test]def test_eq_refl_apply_str : Bool := let refx := Eq.refl "hello" in true#[test]def test_eq_refl_type : Bool := let refx : Eq I64 1 1 := Eq.refl 1 in true// -- Sort universe tests —#[test]def test_sort_formation : Bool := let _type : Sort 2 := Sort 1 in true#[test]def test_sort_cumulativity : Bool := let t : Sort 1 := Sort 0 in true#[test]def test_pi_universe : Bool := let _f : (Sort 1 -> Sort 2) := fn x => x in true// -- Prop/Type/Pred in value position —#[test]def test_type_as_value_arg : Bool := let _x : Sort 1 := get_sort Type in true#[test]def test_prop_as_value_arg : Bool := let _x : Sort 1 := get_sort Prop in true#[test]def test_pred_as_value_arg : Bool := let _x : Sort 1 := get_sort Pred in true#[test]def test_id_type_with_prop : Bool := let _x : Sort 0 := get_identity Prop in true#[test]def test_id_type_with_pred : Bool := let _x : Sort 0 := get_identity Pred in true#[test]def test_prop_nested_inference : Bool := let _x : Sort 1 := get_identity (get_sort Prop) in truedef get_sort {A : Sort 1} (x : Sort 1) : Sort 1 := xdef get_identity {A : Sort 1} (x : A) : A := x// BOrd Bool tests#[test]def test_bord_bool_lt_false_true : Bool := BOrd.lt false true#[test]def test_bord_bool_lt_true_false : Bool := Bool.not (BOrd.lt true false)#[test]def test_bord_bool_lt_false_false : Bool := Bool.not (BOrd.lt false false)#[test]def test_bord_bool_lt_true_true : Bool := Bool.not (BOrd.lt true true)#[test]def test_bord_bool_gt_true_false : Bool := BOrd.gt true false#[test]def test_bord_bool_gt_false_true : Bool := Bool.not (BOrd.gt false true)#[test]def test_bord_bool_gt_true_true : Bool := Bool.not (BOrd.gt true true)#[test]def test_bord_bool_gt_false_false : Bool := Bool.not (BOrd.gt false false)// -- Type propagation tests --#[test]def test_match_with_let_annotation : Bool := let result : Option I64 := Option.some 42 in match result { Option.some x => true, Option.none => false }#[test]def test_do_bind_with_match : IO Bool := do { let x <- IO.pure (Option.some 42); match x { Option.some _ => IO.pure true, Option.none => IO.pure false }}// -- Type inference tests (without annotations) --#[test]def test_let_match_no_annotation : Bool := let result := Option.some 42 in match result { Option.some _ => true, Option.none => false }// -- Comonad tests --#[test]def test_comonad_id_extract : Bool := Comonad.extract (Id.id 42) == 42#[test]def test_comonad_id_duplicate_is_the_same_context_twice : Bool := Id.run (Id.run (Comonad.duplicate (Id.id 42))) == 42// The lambda parameter is annotated -- its carrier is only known from the// call's SECOND argument, which the checker has not inferred yet when it// checks this one, so an unannotated `a` stays a hole and `+` resolves// against the wildcard-headed `instance [Add A] HAdd A A A` bridge, which// then calls itself until the driver dies by signal (the same class of bug// `app_arg_expected_type_from_callee`'s doc comment records for// `Foldable.foldr`).#[test]def test_comonad_id_extend_maps_over_the_context : Bool := Id.run (Comonad.extend (fn (a : Id I64) => Id.run a + 1) (Id.id 41)) == 42#[test]def test_comonad_pair_extract_is_the_second_component : Bool := Comonad.extract (Pair.pair 10 3) == 3#[test]def test_comonad_pair_duplicate_carries_the_environment_into_both : Bool := match Comonad.duplicate (Pair.pair 10 3) { Pair.pair e inner => match inner { Pair.pair e2 a => e == 10 && e2 == 10 && a == 3 } }// Same reason as `test_comonad_id_extend_maps_over_the_context` above: the// lambda parameter needs an explicit annotation.#[test]def test_comonad_pair_extend_applies_with_the_environment_in_scope : Bool := match Comonad.extend (fn (w : Pair I64 I64) => Comonad.extract w + 1) (Pair.pair 10 3) { Pair.pair e b => e == 10 && b == 4 }