Skip to main content
metelResearch language · v0.13.0

Exploring new paths to compile-time safety.

Metel is a research language that combines ideas from across modern language design: ownership, effects, capabilities, and more. Free from legacy constraints, it investigates how these tools can work together in a system that is both explicit and practical to use.

Disjoint projections

Hand two slices of one struct to two functions

Each function takes a projection type — Doc.{ title }, Doc.{ body } — so passing a slice moves just that field. The two calls do not overlap, so both are allowed, and sig is still there afterward. Rust does disjoint borrows; moving first-class field projections is a Metel thing.

struct Doc { title: String, body: String, sig: String }


fun headline(part: Doc.{ title }) -> i64 { part.title.len() }
fun render(part: Doc.{ body }) -> i64    { part.body.len() }


fun main() {
    let d := Doc { title = "Metel", body = "the spec", sig = "v0.13" };
    let a := headline(d.{ title });   // moves title out
    let b := render(d.{ body });      // disjoint — moves body out
    println("${a} ${b} ${d.sig}");    // sig untouched
}
In the tutorial
Narrowing

The type tracks what you have moved

Move a field out and the value narrows to a residual type without it; reassign the field and a struct widens back to whole. The checker follows the move state, per path, at compile time.

struct Cart { user: i64, note: String }


fun peek(s: String) -> i64 { s.len() }


fun main() {
    var cart := Cart { user = 7, note = "abandoned" };
    let n := peek(cart.note);        // note moved; cart : Cart.{ user }
    cart.note := "recovered";        // reassigned — cart : Cart again
    println("${cart.note} (${n})");
}
In the tutorial
Closures

Say what the closure does with what it holds

The capture list names each captured binding; a qualifier — var, once, or none — says how the closure uses it. No Fn / FnMut / FnOnce to reverse-engineer.

In the tutorial
Records + row bounds

A record with at least these fields

An anonymous record needs no declaration. A row-bounded function — <record T: { level, .. }> — accepts any record that has a level field and quantifies the rest.

In the tutorial
Negative bounds

Rule a capability out, not just in

extend<T> Secret<T>: !Loggable overrides a blanket impl that would otherwise grant it — the opt-out is a first-class claim, and it wins.

In the reference
dyn Aspect

One list, many concrete types

Any type that implements Shape coerces to dyn Shape, so a List<dyn Shape> holds a Square and a Rect at once — object-safety checked, dispatched at runtime.

In the tutorial