Bosatsu Programming Language

repository·main·Indexed 42 days ago

https://github.com/johnynek/bosatsu

A non-Turing complete, total programming language designed for configuration, queries, and scripting. Bosatsu emphasizes correctness, explicit effects, and local reasoning, drawing inspiration from Python, Haskell, Dhall, and Rust. It includes a CLI (bosatsuj) with configurable caching for library checks and builds, as well as support for Tree-sitter and VS Code syntax highlighting.

Tokens
113.4K
Snippets
237
Records
504
Agent score
53%

What's inside Bosatsu

  1. Overview of the Bosatsu Programming Language

    main

    Bosatsu is a simple, non-Turing complete language designed for configuration, queries, and scripting. It draws inspiration from Python, Haskell, Dhall, and Rust.

    Key characteristics include:

    • Total Language: Designed for correctness with explicit effects.
    • Explicit Dependencies: Dependencies stay explicit, and the package interface is typically visible at the top of the file.
    • Type Inference: Most types are inferred unless a foreign type is explicitly named.
    • Local Reasoning: Prioritizes clarity and local reasoning over minimizing keystrokes.
    • Private-by-default: Package boundaries are private by default to ensure sound logic flow.
  2. Overview of the Bosatsu language

    main

    Bosatsu (菩薩) is a simple, non-Turing complete language designed for configuration, queries, and scripting. It is inspired by Python, Haskell, Dhall, and Rust.

    Key features include:

    • Python-inspired syntax: Supports function definitions, literal integers/strings, lists, list comprehensions, tuples, and (string key) dictionaries.
    • Pattern matching: Powerful pattern matching capabilities.
    • Static type system: Uses a generalization of the Hindley-Milner (Damas-Milner) type system.
    • Data structures: Supports structs (named tuples/data classes) and enums (sum types).
    • Package system: Includes explicit import and export syntax.

    Constraints and 'Un-features':

    • Limited recursion: Recursion is only allowed if it is guaranteed to terminate and cannot create infinite loops.
    • Data structure constraints: Data structures can only be recursive in covariant positions (not in function arguments).
    • No while loops: Iteration is achieved via tail-recursive functions on sub-values or folds. There is no while syntax.
    package Euler/One
    
    # see:
    # https://projecteuler.net/problem=1
    # Find the sum of all the multiples of 3 or 5 below 1000.
    
    operator == = eq_Int
    operator % = mod_Int
    
    def operator ||(x, y):
      True if x else y
    
    def keep(i):
      (i % 3 == 0) || (i % 5 == 0)
    
    def sum(as): as.foldl_List(0, add)
    
    computed = sum([i for i in range(1000) if keep(i)])
    
    test = Assertion(computed == 233168, "expected 233168")
  3. Bosatsu syntax highlighting features

    main

    The Bosatsu VS Code extension provides syntax highlighting for the following language elements:

    • Keywords, functions, structs, enums, and comments
    • Numeric literals
    • Character literals: Uses the format ."x" or .'x'
    • String interpolation: Highlights ${...} and $.{...} patterns
  4. Optimize BigInt construction without temporary copies

    main

    For certain BigInt operations, the runtime avoids the calloc/malloc followed by memcpy pattern. Instead, it uses a direct-final-buffer path where the final BSTS_Integer object is allocated first, and results are written directly into the integer->words array.

    This optimization is most effective for:

    • add (BigInt addition)
    • times (BigInt multiplication)

    Performance gains:

    • add_big_big_pos: ~65% faster.
    • mul_big_small63_direct: ~55% faster.
  5. Behavioral properties of Array operations

    main

    When using Bosatsu/Collection/Array, the following behaviors are guaranteed across all backends (Evaluator, Python, and C):

    • Indexing: For sliced arrays, the first visible element always has index 0. Internal offset is never observable in the public index.
    • Size: size_Array returns the visible length as an exact Int64.
    • Tabulation: tabulate_Array(n, fn) calls fn exactly once for each index 0 .. n - 1 in increasing order. If n <= 0 or n exceeds the shared constructible array cap (Int.MaxValue on JVM/Python, INT_MAX in C), it returns empty_Array.
    • Get or Default: get_or_Array(arr, idx, default) returns the element at idx if 0 <= idx < size_Array(arr). Otherwise, it calls default exactly once, passing the original requested idx (not a clamped value).
    • Zipping: zip_* functions (like zip_map_Array or zip_foldl_Array) truncate to the length of the shorter visible input (min(size_Array(left), size_Array(right))).
    • Reductions: sumf_Array, sumsqf_Array, zip_sumf_Array, and dotf_Array are strict left-to-right Float64 reductions. They do not reorder or tree-reduce, ensuring consistent rounding and NaN behavior. They return 0.0 if the visible array or paired prefix is empty.
  6. Behavioral Invariants for the libuv C Runtime

    main

    After migrating to the libuv C runtime, the following behavioral invariants must hold:

    • Synchronous Equivalence: A Prog with no asynchronous effects must produce the same result, uncaught error, and stack behavior as the previous synchronous interpreter.
    • Suspension Equivalence: Inserting asynchronous suspension at an effect boundary must be observationally equivalent to the old immediate call_fn1(effect_fn, arg) behavior (except for non-blocking scheduling).
    • Error Handling: Recover must handle errors raised after an asynchronous effect identically to errors raised before one.
    • Execution Order: FlatMap callbacks must run in program order for sequential composition; a later continuation cannot run before the effect it depends on completes.
    • Lifecycle & Isolation:
      • Runtime-owned libuv handles cannot outlive their Prog run or test run.
      • Repeated Prog tests in the same process must be isolated at the loop and handle level.
    • Determinism: Static archive paths and system link flags must be deterministic for the same manifest, build context, and recipe version. Vendored dependency ordering must remain topological and deterministic.
    • Error Stability: Existing IO/Core error variants and context strings must remain stable.
  7. Use `external type` for opaque external declarations

    main

    In Bosatsu, opaque external declarations should be declared using the external type syntax. This is the preferred spelling for defining external types that are constructorless and opaque.

    While the legacy external struct syntax is still supported for backward compatibility and behaves identically, all new code and documentation should use external type.

    Syntax Examples

    Preferred Syntax:

    external type Foo

    Legacy Syntax (Supported):

    external struct Foo

    Note on Ambiguity: To avoid parser ambiguity with the keyword type, an external value named type is declared using the syntax external type: Foo.

  8. Protobuf float and double handling in Bosatsu

    main

    In the current implementation (Phase 1), both protobuf float and double fields are represented using the Bosatsu Float64 type to ensure portability.

    Encoding Logic

    • Protobuf double: Uses the existing Float64 bit path to IEEE754 binary64.
    • Protobuf float: The Float64 value is converted to IEEE754 binary32 bits and written as a fixed32.

    Decoding Logic

    • Protobuf double: Reads binary64 and returns a Float64.
    • Protobuf float: Reads binary32 and widens the value to Float64.
  9. Understand the 62-bit signed immediate integer representation

    main

    The Bosatsu C runtime uses a 2-bit tagged-value scheme for its 64-bit BValue type. To optimize performance and reduce heap allocations, the runtime supports signed 62-bit immediate integers.

    Key Characteristics:

    • Tagging: Uses the bottom 2 bits for tags (00 for pointers, 01 for pure values).
    • Payload: The remaining 62 bits are used for the integer payload.
    • Range: Signed 62-bit two's-complement range is [-2^61, 2^61 - 1].
    • Fallback: Values outside this range are automatically represented as heap-allocated big-ints using sign-magnitude storage.

    This architecture allows common large values (like timestamps or large counters) to remain non-allocating while preserving the existing runtime object model.

  10. YAML rendering scalar and container rules

    main

    The Bosatsu YAML renderer follows specific formatting rules to balance human readability with strict parsing correctness:

    Scalar Rules (Strings)

    Strings are rendered unquoted only if all the following are true:

    1. The string is non-empty.
    2. The string contains no whitespace.
    3. The string is not parseable as any JSON value (e.g., it's not a number or null).
    4. The lowercase form is not one of the YAML boolean-like scalars: yes, no, on, or off (case-insensitive).
    5. The characters are in a safe plain-scalar subset to avoid syntax ambiguity.

    Otherwise, strings are rendered using JSON-style double-quoted escaping.

    Container Rules

    • Block Style: Arrays and objects are rendered in block style by default.
    • Arrays: Rendered as - lists with indentation.
    • Objects: Rendered as key: value mappings with indentation.
    • Nesting: Nested structures are rendered on subsequent indented lines.
    • Empty Containers: Empty arrays and objects are rendered concisely as [] and {}.
  11. Preserve laziness in `lazy(() -> x)` via suspension boundaries

    main

    To prevent the optimizer from breaking the semantics of Lazy, Bosatsu uses suspension boundaries to restrict how TypedExprNormalization moves code.

    When the compiler encounters a suspension boundary (Unit -> a lambda), the following optimizations are restricted:

    1. Outward let floating: The compiler will not move a let binding from inside the lambda to a position outside the lambda, even if the expression does not depend on the lambda's arguments.
    2. Outward match floating: The compiler will not move a match scrutinee from inside the lambda to outside.
    3. Immutable value sharing: The shareImmutableValues pass is prohibited from collecting expressions from inside a suspension boundary to create let bindings in the outer scope. This prevents repeated closed expressions inside a thunk from being hoisted out and evaluated eagerly.