Skip to content

Instantly share code, notes, and snippets.

@Verdagon
Created September 30, 2025 02:04
Show Gist options
  • Save Verdagon/31bb67bef0860bcbad11edec41c6718b to your computer and use it in GitHub Desktop.
Save Verdagon/31bb67bef0860bcbad11edec41c6718b to your computer and use it in GitHub Desktop.
# 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