nat
Type-level natural number literals
moon add tonyfettes/nat@0.1.1
Download zipAuthor
Version
0.1.1
License
Apache-2.0
Last updated
6 months ago
Downloads
3K
README#tonyfettes/nat
A MoonBit library for type-level natural number literals.
#Overview
This library provides a way to represent natural numbers at the type level in
MoonBit. While the numeric values are computed at runtime, the type-level
encoding allows the type system to track and verify numeric constraints at
compile time. It supports both decimal and hexadecimal number systems.
#Features
- Type-level natural numbers: Encode natural numbers directly in the type system
- Decimal literals: Use types like Od1, Od2, etc. to represent decimal digits (0-9)
- Hexadecimal literals: Use types like Ox1, OxA, etc. to represent hexadecimal digits (0-F)
- Runtime conversion: Convert type-level numbers to runtime Int or UInt64 values
- Static type checking: Ensure numeric constraints are verified at compile time
#Use Cases
Type-level natural numbers are particularly useful for:
- Multi-dimensional arrays with statically known sizes: Encode array dimensions in the type system to prevent dimension mismatches at compile time
- C FFI (Foreign Function Interface): Represent fixed-size buffers, array dimensions, or other numeric constants required by C APIs in a type-safe manner
- Compile-time constraints: Any scenario where you need to enforce numeric constraints through the type system
#Usage
#Basic Usage
// Convert a type-level number to UInt64
///|
let value = to_uint64((_ : Od42[Z]) => ()) // Returns 42 as UInt64
// Convert to Int
///|
let int_value = to_int((_ : Od42[Z]) => ()) // Returns 42 as Int#Decimal Numbers
Decimal digits are represented using types Od0 through Od9:
to_uint64((_ : Od5[Z]) => ()) // 5
to_uint64((_ : Od3[Od21[Z]]) => ()) // 321
to_uint64((_ : Od12[Od34[Od56[Z]]]) => ()) // 123456The digits are composed right-to-left, with Z representing zero at the base.
#Hexadecimal Numbers
Hexadecimal digits are represented using types Ox0 through OxF:
to_uint64((_ : OxA[Z]) => ()) // 10
to_uint64((_ : OxF[Z]) => ()) // 15
to_uint64((_ : Ox12[Ox34[Ox56[Z]]]) => ()) // 0x123456#Multi-digit Numbers
You can compose larger numbers by nesting digit types. Pre-defined convenience
types are available for common two-digit combinations:
// Using convenience types
to_uint64((_ : Od12[Z]) => ()) // 12
to_uint64((_ : Od99[Z]) => ()) // 99
// Using nested types
to_uint64((_ : Od2[Od10[Z]]) => ()) // 210#Installation
Add this to your moon.mod.json dependencies:
moon update
moon add tonyfettes/nat#API
#Types
- Z: Represents zero at the base of a number
- Od0[T] through Od9[T]: Decimal digit types
- Ox0[T] through OxF[T]: Hexadecimal digit types
- Pre-defined convenience types for two-digit combinations (e.g., Od10, Od42, Ox1A)
#Functions
pub fn[T : ToUInt64] to_uint64(_ : (T) -> Unit) -> UInt64
pub fn[T : ToInt] to_int(_ : (T) -> Unit) -> IntConvert a type-level number to a runtime value.
#How It Works
The library uses MoonBit's trait system to encode numbers at the type level.
Each digit type implements the ToUInt64 and ToInt traits, which recursively
compute the numeric value at runtime by multiplying the accumulated value by the
base (10 for decimal, 16 for hexadecimal) and adding the digit. While the
computation happens at runtime, the type-level encoding allows the compiler to
verify numeric constraints and dimensions at compile time.
#License
Apache-2.0
#Contributing
Contributions are welcome! Please feel free to submit issues or pull requests.
#Od0
type Od0[_]
#Od1
type Od1[_]#Od2
type Od2[_]#Od3
type Od3[_]#Od4
type Od4[_]#Od5
type Od5[_]#Od6
type Od6[_]#Od7
type Od7[_]#Od8
type Od8[_]#Od9
type Od9[_]#Ox0
type Ox0[_]#Ox1
type Ox1[_]#Ox2
type Ox2[_]#Ox3
type Ox3[_]#Ox4
type Ox4[_]#Ox5
type Ox5[_]#Ox6
type Ox6[_]#Ox7
type Ox7[_]#Ox8
type Ox8[_]#Ox9
type Ox9[_]#OxA
type OxA[_]#OxB
type OxB[_]#OxC
type OxC[_]#OxD
type OxD[_]#OxE
type OxE[_]#OxF
type OxF[_]#Z
type ZType-level natural number literals
0.1.1
Apache-2.0
Updated 6 months ago
3K downloads