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.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697/// `Borrow A` — a type-level marker that a value is being read, not/// owned. B1 of the borrow design (*Design B: Viability Experiment* //// M2.5): B0 moved `Copy` here, B1 is this file, B2 the escape rule,/// B3 gradual conversion.////// ## What "Option 1" means here////// Three readings of "a normal type constructor with a Copy instance"/// were on the table; this file implements the smallest one,/// deliberately, to isolate the measurement before committing to more:/// **caller-side only.** `Borrow.of x` marks a value as read rather/// than moved at the CALL site, so the same `x` can be handed to/// several borrowing functions without tripping the affine rule/// (`lang/typecheck/affine.mo`). What a borrowing function does with/// the borrow once it has it — whether it may store the underlying/// value, whether pattern matching should work through the wrapper/// directly — is NOT addressed here. Two options were set aside:////// - `Borrow.get` plus a zero-owning-use escape check on the unwrapped/// binder (would need `lang/typecheck/affine.mo`'s `check_binder`/// extended with a new binder provenance for "came from Borrow.get")./// - `match` working through a `Borrow` directly, yielding borrowed/// fields (match ergonomics) — a real type-system feature, not a/// newtype.////// Both stay open; this file's job is to prove the smallest version/// moves the number before either is built.////// ## Representation////// Exactly one constructor, exactly one field — the shape a/// `#[transparent]`-style erasure (M2.5's own risk-flagged step) would/// target. Nothing in THIS file erases it, and this is MEASURED, not/// predicted: a compiled probe's emitted IR shows `Borrow.of` lowering/// to `monad_ctor_Borrow_of`, which calls `alloc_constructor(tag, 1)` —/// a real boxed `Constructor` with a header, exactly as/// `alloc_constructor` (`runtime/src/runtime.c`) caching only nullary/// constructors predicted it would. `lang/src/scope.mo`'s/// `last_colon_colon` is converted to take `Borrow String` despite/// this — deliberately, per the decision recorded in the experiment log:/// the counting win is/// real and measured (`bench/src/affine_report.mo`), and the allocation/// cost is provably ONE PER CALL, not one per character scanned —/// `last_colon_colon` is self-recursive and threads the same `Borrow`/// value through every recursive step unchanged, so only its single/// external caller's one `Borrow.of` wrap ever allocates. (The first/// candidate tried, `alias_map_insert`, was reverted: a corpus-wide grep/// found two more callers in `lang/codegen/qualify.mo`'s hot/// per-declared-name pass — ~3,172 names — which is exactly the danger/// this file's own header warns an unerased `Borrow` risks, and/// converting it there would have paid that cost for real, not just in/// the static count.) Erasure is deliberately left as its own future/// step rather than attempted under this one's time pressure — it means/// teaching `lang/src/codegen/emit.mo`, the central codegen file with/// real miscompile history from careless changes, to special-case this/// constructor as the identity, which deserves its own verification/// pass (an IR diff before/after), not a rushed addition here.use init::copy {Copy}type Borrow A { of (value : A)}/// Project the borrowed value back out. Deliberately UNRESTRICTED for/// now — nothing stops the result from being stored, which is unsound/// in general. That enforcement is exactly what was deferred above/// (the second option's escape check); B1 is measurement, not/// enforcement, and nothing in this experiment rejects a program yet.pub def Borrow.get (b : Borrow A) : A := match b { of v => v }/// `Borrow A` is `Copy` REGARDLESS of `A` — duplicating a borrow copies/// the marker, not the value underneath, which is why this instance/// carries no `[Copy A]` constraint. An UNCONDITIONAL parametric/// instance needed a real fix to `lang/typecheck/copy_class.mo`'s/// instance-admission rule to resolve at all — see that file's/// `instance_unconditionally_copy`, and `bench/src/affine_report.mo`/// for the measurement this instance existing was meant to produce.instance {A : Type} Copy (Borrow A) { def copy (b : Borrow A) : Pair (Borrow A) (Borrow A) := Pair.pair b b}#[test]def test_borrow_get_roundtrips : Bool := I64.beq (Borrow.get (Borrow.of 7)) 7#[test]def test_borrow_of_a_string_roundtrips : Bool := String.beq (Borrow.get (Borrow.of "hi")) "hi"#[test]def test_copy_borrow_duplicates_the_marker : Bool := let b : Borrow I64 := Borrow.of 9 in match Copy.copy b { Pair.pair b1 b2 => I64.beq (Borrow.get b1) 9 && I64.beq (Borrow.get b2) 9, }