Created
September 30, 2025 02:04
-
-
Save Verdagon/31bb67bef0860bcbad11edec41c6718b to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Article Skeleton | |
title options: | |
- A Memory Safety Enigma in the Mojo Standard Library | |
- Mojo's Dependent Types and Memory Safety | |
-------- | |
I was doing my normal thing in Mojo, implementing struct extensions, when I came across this function in the standard library: | |
```mojo | |
@always_inline | |
fn next_ref( | |
mut self, | |
) -> ref [self.src[]._entries[0].value()] Self.Element: | |
``` | |
What in the world is that return type? | |
What's that `self.src[]._entries[0].value()` about? | |
This humble line is a hint at a foundation for some very, very cool things that no other mainstream language can do. | |
Hark, my fellow explorers, and behold the tale of **return origins**. | |
## Generics, Const Generics, and Dependent Types | |
To truly understand what's going on with this line, we have to highlight the difference between three things: | |
- Generics (`List[T]`, `HashMap[K, V]`, etc.) | |
- Const-generics (`SIMD[DType.bfloat16, 8]`, `InlineArray[Int, 8]`) | |
- Compile-time dependent types (`SIMD[DType.bfloat16, 2 * size]`, `InlineArray[Int, M * N]`) | |
I'll cover these, and then talk about how Mojo's origins are actually using dependent types under the hood. | |
(talk about difference between generics and const generics. const generics allows any sort of value, not just types) | |
(Matrix example: `fn multiply[M, N, P](a: Matrix[M, N], b: Matrix[N, P]) -> Matrix[M, P]`) | |
(talk about difference between const generics and dependent types) | |
(examples: `SIMD[dtype, 2 * size]`, `Array[T, M * N]`) | |
(Answer the question: What does "type level algebra" enable? show SIMD.join: `fn join(self, other: Self) -> SIMD[dtype, 2 * size]:` to show a simple example that is practical and useful) | |
(Aside: Why does rebind come up, and why is rebind not needed for "x*2" vs "2*x" (answer: always inline builtin)) | |
(maybe mention run-time dependent types, `Vec<i32, n>` where `n` is a runtime value, and mention how its rare and mojo doesn't try to have these) | |
## Compile-Time Dependent Types | |
Mojo's dependent types work because they're built on **comptime evaluation** rather than reasoning and complex constraint solvers. | |
In traditional dependent type systems, when the user writes: | |
``` | |
fn process[N: Int](arr: Array[T, fibonacci(N)]) -> ... | |
``` | |
...the compiler thinks "I need to *prove* that fibonacci(N) terminates, and then compute its result!" | |
In other words, the compiler has to solve the halting problem. | |
Mojo's approach is based on the fact that we don't *have* to solve the halting problem. Let's just *run the function.* | |
Suddenly, when you take that stance, all the problems melt away, and you get useful dependent types in a language. | |
Take this example Mojo program: | |
```mojo | |
@parameter | |
fn fibonacci(n: Int) -> Int: | |
if n <= 1: return n | |
return fibonacci(n-1) + fibonacci(n-2) | |
fn process[N: Int](arr: InlineArray[T, fibonacci(N)]) -> ... | |
``` | |
There's a comptime evaluator inside our instantiator, so when the user asks for a `process[9]`, it just runs the `fibonacci(9)` at compile time, and comes up with 34. The resulting `process` signature is this: | |
``` | |
fn process[9](arr: InlineArray[T, 34]) -> ... | |
``` | |
In other words, comptime execution is what makes Mojo's compile-time dependent types work, with no constraint solving, no theorem proving, nothing. | |
It works for `2 * size`, `fibonacci(N)`, any deterministic computation, and even memory safety things like `self.first`, like we'll see below! | |
## Mojo's Origins are Compile-time Dependent Types | |
Mojo's origins use compile-time dependent types as well. | |
(example: `fn get_first_ref(ref self: Container) -> ref [self.first] Int`) | |
(second example:) | |
``` | |
@fieldwise_init | |
struct Container: | |
var first: Int | |
var second: Int | |
fn get_first_ref(ref self: Container) -> ref [self.first] Int: | |
return self.first | |
fn get_second_ref(ref self: Container) -> ref [self.second] Int: | |
return self.second | |
fn takes_two_muts(mut a: Int, mut b: Int): | |
pass | |
fn test(): | |
var container = Container() | |
takes_two_muts(get_first_ref(container), get_second_ref(container)) | |
``` | |
(talk about how thats not possible in any other language) | |
(talk about how rust gets close, can do this intra-function, but not inter-function like this) | |
(talk about the architectural implications. whats something big and relatable that this enables? are there any big projects where this would have helped?) | |
## `next_ref` | |
(full example using `next_ref`'s `-> ref [self.src[]._entries[0].value()] Self.Element`, to explain that first line) | |
## Conclusion | |
(conclusion here) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment