[Proposal] Checking constrained methods at overload resolution time

owenhilyard · April 15, 2025, 8:17pm

This is a discussion thread for the following proposal from @clattner: max/mojo/proposals/requires-clause.md at main · modular/max · GitHub

owenhilyard · April 15, 2025, 8:19pm

@ing a few people who are likely interested.

@sora @Nick @bgreni @Helehex @rd4com

sora · April 15, 2025, 8:31pm

I’ll post a longer, more systematic feedback piece later, this is just a quick opinion.

Yes, to every feature listed in the proposal. But IMO, no, this is absolutely not the direction we should take as the immediate next step for the type system.

Put plainly: it shores up constraint checking (which, one could argue, is already too expressive for its own good), but offers nothing toward constraint propagation, which is the real bottleneck (we see in stdlib and everywhere else). Even with the entire proposal implemented, we still can’t do the following:

struct SIMD[...]:  # No place to express conformance to Boolable
                   # because in general it doesn't conform
  fn __bool__(self: SIMD[_, 1]) -> Bool: ...  # old syntax, but illustrates the point

fn bool[T: Boolable](x: T) -> Bool:
  return x.__bool__()

bool(Int32(0))  # still rejected

This, is the actual pain point. Conditional conformance remains unsolved. Until it is, we’re not moving the needle.

owenhilyard · April 15, 2025, 9:23pm

I’m very happy that we can start discussion on this. Alongside a few other things, the current approaches forces over-use of conditional conformance and gives very poor errors.

Introduction

fn safe_divide[T](a: T, b: T) where (T instanceof Numeric and T.min_value() < 0):

I am very much a fan of, instead of normal trait bounds, letting the “where” clause be an expression that can be evaluated to a boolean at parse time. This solves many headaches I have in Rust’s type system where I want to do something like take a fast path for powers of 2.

Concrete syntax design

How reasonable is it to have the error messages be an expression which evaluates to a String or StringLiteral? I think that being able to use the inputs as part of the error message may make some errors much clearer, especially in parameter-heavy code where the user could lose track of the inputs.

Notice how this puts the constraints where they belong - put the constraints for the SIMD type as a whole on the struct, and put the constraints for the method on the method itself.

I think this is a good idea moving forwards. We should allow the construction of types as desired, and then use requires to constrain functions by what they need. This would let us move most of the collections type constraints to UnknownDestructibility.

Logical extensions (not in scope for this proposal)

I think that requires T instanceof Trait is one of the most desired parts of this feature. Overload-heavy code is painful to write, especially on types that have a lot of constraints, since you end up rewriting most of the parameters for every single function. This general annoyance is part of why many of the stdlib collections still have a CollectionElement constraint, despite it technically being possible to conditionally conform away, because I would have fixed several of them already if not for the myriad of compiler crashes I ran into.

T == Type is good for specialization, but my understanding is that we have those capabilities at elaboration time already.

Primary Limitation

Specifically, there is a proposal to make the comptime interpreter support direct-interpreting parametric IR instead of relying on the elaborator to specialize it before interpretation. If we had that (and a couple other minor things) we could bring it back and make it “actually work and be predictable” into the parser, and solve this in full generality.

This sounds very desirable to me, especially since many of the usecases I would imagine for a feature like this which doesn’t support traits would be something like alignof[T]() == sys.info.cache_line_size() or something similar, and if it has to be an expression with no function calls, all of sys.info is unavailable. requires sys.info.has_avx512() is another example of something I’d like to work.

Alternatives considered

I would shy away from requires in part because it has a very different meaning, and in my opinion is actually closer to defining a trait in some usages. ex:

template<typename T>
concept Addable = requires (T a, T b)
{
    a + b; // "the expression “a + b” is a valid expression that will compile"
};

(taken from cppreference)

I agree with Sora that this does lead us further down the road of implicit trait conformance, since even if we do get some form of struct SIMD[...](Boolable if Self.size == 0) down the line, that just duplicates the requires clause. I think that the Rust style of having impl Trait for T where ... is sufficient. I’ll go bring up the arguments I have around “implicit acceptance of API contracts” if we want to rehash that debate, but my general position is that implicit trait conformance is dangerous and not worth the typing it saves.

In general, I support this because it expands what’s possible in Mojo. However, I think the logical extensions are something which should really be looked at as they are a substantial ergonomics improvements over what currently exists.

gryznar · April 16, 2025, 11:20am

I am not convinced with this flatcase keyword: instanceof. Maybe we can use something shorter in snake_case, like is_a?

Nick · April 17, 2025, 9:06am

I like where @clattner’s proposal is headed. I definitely think Mojo needs something akin to requires. In fact, I think we should probably go a bit further: I think Mojo needs several related features that depend upon flow-sensitive analysis, in the way that requires does.

Below, I briefly cover each of these features. My goal is to encourage Modular to see requires as being part of a larger set of language features.

Future Mojo features that are built upon flow-sensitive analyses

1. Conditional `fn` and `struct` definitions (falsity forbidden)

Chris proposes using require clauses to demand that parameters meet certain constraints:

fn foo[size: Int](...)
  requires size.is_power_of_2():

However, a more general design could offer much more utility. In particular, it would be helpful to use require clauses to demand that arguments meet certain constraints:

fn __div__(self, divisor: Int) -> Self
  requires divisor != 0:

fn submit(self) requires self.validated():

In other languages, this feature is known as preconditions or invariants. These are old and relatively well-explored concepts, although they haven’t been popular in recent decades.

To check preconditions at compile time, we would need to track the set of proven-true Boolean statements at each point in a program’s control flow. Chris suggested tracking this information for @parameter if. I think we should (eventually) do this for all kinds of branches. For mutable runtime variables, we would also need to invalidate Boolean statements after their operands have been mutated. Figuring out the right semantics for this will be a bit tricky (thanks to side effects), but I don’t see any major roadblocks.

Once we have preconditions, we will probably also want postconditions, i.e. conditions that are guaranteed to be true at the moment a function returns.

These concepts naturally augment each other: one function’s postcondition is another function’s precondition:

fn validate(self) ensures self.validated():

fn submit(self) requires self.validated():

This feature would require a lot more motivation, and a lot more design work. It would be off-topic to take this thread in that direction, but hopefully readers get the gist of how pre+postconditions might work, and why they might be useful.

2. Conditional exceptions (falsity ⇒ no exception)

In the last section we discussed forbidding the calling context from being in a certain state. To give the programmer more freedom, we could instead declare such a state to be a prerequisite for an exception:

fn pop(self) -> T
  raises if len(self) == 0:

This offers the programmer more choices than a require statement does. The programmer can either:

Let the exception propagate outward from the call site. (A require statement does not offer this option.)
Prove that they are calling the function in such a way that no exception will occur. (For example, because len(self) > 0.)

In my opinion, the above example—List.pop()—is already a decent use case for this feature. Dict.pop() is a similar use case. There are likely many other uses. This feature deserves a proper proposal.

Note 1: I gave additional motivation for raises if syntax (and yields if syntax) as part of my proposal on introducing a “yields” effect. (For defining functions that are generic over whether they suspend.)

Note 2: In the above signature for List.pop(), I put raises after the return type, to be consistent with requires. IMO, when requires is introduced, Modular should consider making this corresponding change to raises.

3. Conditional mutation (falsity ⇒ no mutation)

On top of conditional raises, we can also investigate the merits of conditional mut. One particular use case would have enormous utility: For a mutation that invalidates pointers, it would be helpful to be able to declare the mutation as being conditional on some precondition (not) being met. This gives the programmer to opportunity to prove that an operation doesn’t invalidate pointers in their particular context of use:

struct List[T: CollectionElement]:
  fn append(self, item: T)
    mut self._len  # unconditional mut
    mut (self.ptr, self.capacity) if self._len == self.capacity:  # conditional

# ------------- Example usage --------------
var nums = List[Int](...)
# Obtain a pointer into the buffer
var p = Pointer(nums[0])
# Check if `append` will reallocate
if nums._len < nums.capacity:
    nums.append(x)  # This operation DOESN'T mutate nums.ptr
    print(p[])      # The element pointer can still be dereferenced
else:
    nums.append(x)  # This operation MIGHT mutate nums.ptr
    # print(p[])    # The pointer is NOT valid

Note: The semantics of pointer invalidation is much more subtle than the above program suggests. For starters: popping from a List or an InlineList needs to invalidate element pointers even if the buffer pointer remains fixed. Therefore, please don’t mistake the above example as presenting a complete solution to pointer invalidation. At best, it’s a component of a larger solution.

I’ve been working on a “complete solution” over the last year. I hope to publish an update 1-2 months from now.

Summary

There are at least 4 different features based on the idea of “constrained function calling” that Mojo should consider:

requires clauses (preconditions) (on parameters AND arguments)
ensures clauses (postconditions)
conditional exceptions (raises if)
conditional mutation (mut if) (only relevant to pointer invalidation)

I understand that requires clauses are Modular’s immediate priority. But at the very least, I would suggest that Modular keep these other features in mind when requires clauses are being implemented. In doing so, you might save yourself some implementation work in the future.

My 2 cents on keywords

I don’t have a strong opinion on requires… except that its name should ideally complement a future keyword for postconditions, e.g. ensures. (requires+ensures have precedent in other languages.) I’m not a huge fan of where, because it’s a tad vague.

Chris’s proposal uses instanceof for trait bounds, e.g. T instanceof Stringable. I would suggest using is instead, because:

It’s available. (It’s currently only defined on (instance, instance) and (class, class) pairs.)
It’s much shorter than instanceof, and reads more cleanly.

Example:

fn sort(self) requires T is Comparable:

owenhilyard · April 17, 2025, 12:49pm

fn __div__(self, divisor: Int) -> Self
  requires divisor != 0:

I think that this is close to the “contracts” feature of C++ and Ada. It is something I think is worth exploring, but given that it inspects runtime values, at least in some hardening modes, or requires compile-time knowledge that a given condition is true, it’s probably best to not shackle requires to contracts. If Mojo does go down this road, postconditions would also be welcome. This could also Mojo down the Agda/Lean/Rocq route, which is probably best avoided unless someone can find a way to make it “less mathy”.

fn pop(self) -> T
  raises if len(self) == 0:

I think this is only doable if len(self) is compile-time known, since this changes code generation.

Conditional mutation / pointer invalidation

While it’s nice the feature is useful there, I don’t think we should weigh the usefulness of this feature for a model that hasn’t even been fully written down yet when deciding whether to adopt it.

Chris’s proposal uses instanceof for trait bounds, e.g. T instanceof Stringable. I would suggest using is instead

Strongly agree on is. It feels slightly more pythonic to me, since instanceof is a function in python, and it “reads better” (ex: fn foo[T](...) requires T is Stringable). Even for things like T is Iterator[U], it still reads reasonably well. Given my experience with a similar feature in Rust, I expect to be typing it a LOT, to the degree that if we go for instanceof I would request an LSP-powered shorthand (think psvm → public static void main(String[] args) {} for Java in Jetbrains IDEs).

Nick · April 18, 2025, 12:29am

I think that this is close to the “contracts” feature of C++ and Ada. […] given that it inspects runtime values, at least in some hardening modes, or requires compile-time knowledge that a given condition is true, it’s probably best to not shackle requires to contracts.

I am not proposing that the compiler generate implicit instructions for checking runtime values. I am proposing that the compiler perform the exact same parse-time checking that Chris is proposing, i.e. contextual invariants. In the case of my __div__ example, this would mean that __div__ is only able to be invoked at a point in the control flow that is guarded by the condition divisor != 0. Mojo programmers would need to manually insert this check.

It’s probably not constructive to argue that feature X of language Y would be troublesome in Mojo, because at the time of writing, nobody has suggested that Mojo adopt feature X of language Y. In my last post, I was merely enumerating some benefits of being able to reason about “functions with pre- or post-conditions”. I wasn’t talking about a feature of any particular language.

I think raises if len(self) == 0 this is only doable if len(self) is compile-time known, since this changes code generation.

You’re assuming that the function is specialized to the value of this expression. I am not.

In my mind, the purpose of this condition is not to influence specialization. It’s to allow the caller to ignore the error path of List.pop in contexts where they have already confirmed that the list is non-empty. Again, this is related to Chris’s tracking of contextual invariants.

That said, the compiler might wish to generate two implementations of a function tagged with raises if <runtime-expr>: one for calling contexts where the expression is known to be false, and one for calling contexts where it isn’t. The former implementation would have lower runtime overhead. But this is just an optimization; it’s not my central point.

[Conditional mutation / pointer invalidation] While it’s nice the feature is useful there, I don’t think we should weigh the usefulness of this feature for a model that hasn’t even been fully written down yet when deciding whether to adopt it.

Yes I agree it’s too early to evaluate whether mut if <cond> is a good idea. But I wanted to put it out there in public. Chris might find it interesting, because he’s been doing most of the design and implementation work for origins.

rd4com · April 18, 2025, 2:11am

Interesting, there is also:

trait MyTrait:
     ...

That are part of the whole system

owenhilyard · April 18, 2025, 11:02am

I am not proposing that the compiler generate implicit instructions for checking runtime values.

Sorry, I didn’t mean to imply that. There are hardening modes for the C++ contracts proposal which would require runtime checks, and I think that it may be worthwhile to investigate a feature like that for Mojo. Of course, I want everything to be free at runtime that can be, but there are absolutely projects for which “crash if these invariants are violated” is a better idea than raw speed. For example, filesystems, if they detect a broken invariant in an in-memory data structure, are somewhat duty bound to tear everything down as fast as it can to safeguard the data on the disk. Some of my concern is around “fragile” checks which might easily break if constant propagation can’t be guaranteed.