<p>I've recently listened to <a href="https://corecursive.com/009-throw-away-the-irrelevant-with-john-a-de-goes/" rel="nofollow noreferrer">Corecursive episode with John A De Goes</a> and there's one thing that really got me thinking: the idea of type class laws pertaining to performance guarantees. The example discussed in the episode is requiring all instances of a container class type to have constant time random access to their elements.</p>
<p>This made me think of hypothetical Rust trait bounds where one could specify a generic type parameter adhering to some <em>runtime constraints</em>.</p>
<p>I understand this is probably answered in <a href="https://dl.acm.org/doi/10.1145/3209108.3209146" rel="nofollow noreferrer">this paper</a>, at least to some degree, (found in <a href="https://langdev.stackexchange.com/a/2713/1086">this answer</a> to another question), but I was hoping for a more hand-wavy, informal overview here, before even attempting to read the paper <s>(also, I don't have an access yet)</s>.</p>
<p><strong>What would be some required additions to/modifications of Rust for this to become expressible with its type-system?</strong></p>
<p>Considering <a href="https://steveklabnik.com/writing/rusts-golden-rule" rel="nofollow noreferrer">Rust's golden rule</a>, preferably this could be inferred from the function/method signature alone. I was thinking of Zig's approach of requiring explicit passing of an allocator - I'd expect it would be quite straightforward to build upon this facility to describe a generic type such that constructor of its instance doesn't require dynamic allocation. Could other runtime behaviors be &quot;externalized&quot;/made explicit in a similar manner, so that function signature would carry sufficient information?</p>

<compilers><types><traits><compiler-inference>
Expressing runtime constraints with trait-bounds
CC BY-SA 4.0
2023-11-23T19:43:25.350Z
This question feels very broad as currently put, seeking language design choices, evaluations of usefulness, instances in existing languages, commentary on first-class effects, implementation strategies, and type expressions of properties all at once. It would probably do to refine its scope down a bit to a single question. You can find the paper you're looking for [here](https://www.scs.cmu.edu/afs/cs.cmu.edu/Web/People/fp/papers/lics18.pdf), or a longer version [here](https://arxiv.org/pdf/1712.08310.pdf).
Michael Homer
CC BY-SA 4.0
2023-11-23T20:08:33.493Z
@MichaelHomer Thank you for the links! I intended the first question in bold to be *the* question and the rest just a description of my thought process and possible hints as to what exactly I am interested in. Perhaps naively, I thought these all fall under the "language design choices".
gstukelj
CC BY-SA 4.0
2023-11-23T20:13:51.987Z
We have a close reason "Lacks objective design criteria", which is glossed as "This question solicits language designs or design tradeoffs but does not provide sufficient criteria to objectively determine what constitutes a good answer. It should be updated to include a specific design or implementation problem to be solved and should provide additional context to help focus potential answers."; that probably fits this version of the question, so it would be good to [edit] it so that it's clear that it doesn't.
Michael Homer
CC BY-SA 4.0
2023-11-23T20:14:57.367Z
Understood, will edit accordingly.
gstukelj
<p>I see 3 ways to implement this, each with benefits and drawbacks: <a href="https://stackoverflow.com/a/76445965">marker traits</a>, <a href="https://arxiv.org/pdf/2010.07763.pdf" rel="nofollow noreferrer">refinement types</a>, and <a href="https://docs.racket-lang.org/reference/data-structure-contracts.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fmisc..rkt%29._any%2Fc%29%29" rel="nofollow noreferrer">contracts</a>. Marker traits are already in Rust, refinement types and contracts are possible with experimental libraries.</p>
<h1><a href="https://stackoverflow.com/a/76445965">Marker traits</a></h1>
<p><strong>Manually add a marker trait for types where the runtime constraint is met</strong>. If only some instances of a particular type satisfy the constraint, create a <a href="https://workday.github.io/scala/2015/02/05/scala-typesafe-wrappers" rel="nofollow noreferrer">type-safe wrapper</a>. In some cases you may use the type-safe wrapper and skip the trait entirely.</p>
<pre class="lang-rust prettyprint-override"><code>// Example 1
pub trait ConstantTimeRandomAccess {}
impl&lt;T&gt; ConstantTimeRandomAccess for Vec&lt;T&gt; {}
impl&lt;T&gt; ConstantTimeRandomAccess for (T, T, T, T, T) {}
// NO
// impl&lt;T&gt; ConstantTimeRandomAccess for LinkedList&lt;T&gt; {}

// Example 2
pub trait EvenNumber {}
pub struct EvenInteger(i32);
pub struct EvenFloat(f32);

impl EvenNumber for EvenInteger {}
impl EvenNumber for EvenFloat {}
// NO
// impl EvenNumber for i32
pub struct NotEven;
impl TryFrom&lt;i32&gt; for EvenInteger { type Error = NotEven; ... }
impl TryFrom&lt;f32&gt; for EvenFloat { type Error = NotEven; ... }
impl Add for EvenInteger { ... }
impl Add for EvenFloat { ... }

// Usage
fn get_1st_element&lt;T, Col: Collection&lt;T&gt; + ConstantTimeRandomAccess&gt;(collection: &amp;Col) -&gt; &amp;T { 
    collection.get(0).unwrap()
}
fn add_even_numbers&lt;T: EvenNumber + Add&lt;T, Output = T&gt;&gt;(a: T, b: T, c: T, d: T, e: T) -&gt; T {
    a + b + c + d + e
}

fn main() {
    dbg!(get_1st_element(vec![1, 2, 3, 4, 5]));
    dbg!(get_1st_element((&quot;a&quot;, &quot;b&quot;, &quot;c&quot;, &quot;d&quot;, &quot;e&quot;)));
    // Compiler error
    // dbg!(get_1st_element(LinkedList::from([1, 2, 3, 4, 5])));

    dbg!(add_even_numbers(EvenInteger::try_from(2).unwrap(), EvenInteger::try_from(4).unwrap(), EvenInteger::try_from(6).unwrap(), EvenInteger::try_from(8).unwrap(), EvenInteger::try_from(10).unwrap()));
    // Compiler error
    dbg!(add_even_numbers(1, 2, 3, 4, 5));
    // Runtime error :(
    dbg!(add_even_numbers(EvenInteger::try_from(1).unwrap(), EvenInteger::try_from(2).unwrap(), EvenInteger::try_from(3).unwrap(), EvenInteger::try_from(4).unwrap(), EvenInteger::try_from(5).unwrap()));
}
</code></pre>
<p>This is <strong>by far the easiest and most expressive solution</strong>, and you can use it in Rust right now. The drawback is that <strong>the compiler won't actually check the runtime characteristics of the trait</strong>, that is on you. It won't stop you from writing</p>
<pre class="lang-rust prettyprint-override"><code>impl&lt;T&gt; ConstantTimeRandomAccess for LinkedList&lt;T&gt; {}
impl EvenNumber for i32 {}
</code></pre>
<p>A drawback of the type-safe wrapper is that, in order to get a value inside of it, you must check the constraint somewhere at runtime. The optimizer may be smart enough to inline <code>EvenInteger::try_from(2).unwrap()</code> into a no-op, but it won't alert you that <code>EvenInteger::try_from(3).unwrap()</code> is guaranteed to panic.</p>
<h1><a href="https://arxiv.org/pdf/2010.07763.pdf" rel="nofollow noreferrer">Refinement Types</a> (AKA Liquid Types)</h1>
<p><strong>Refinement types are types which have runtime constraints which are checked at compile-time</strong>, typically using SMT solvers.</p>
<p>Refinement type syntax may look something like this:</p>
<pre class="lang-rust prettyprint-override"><code>// Hypothetical syntax as a trait bound
fn add_even_numbers&lt;T: { x: Add&lt;T, Output = T&gt; + Mod&lt;T, Output = T&gt; | x % 2 == 0 }&gt;(a: T, b: T, c: T, d: T, e: T) -&gt; T {
    a + b + c + d + e
}

// Hypothetical syntax as a type bound
type EvenInteger = {v: i32 | v % 2 == 0 };
fn add_even_numbers(a: EvenInteger, b: EvenInteger, c: EvenInteger, d: EvenInteger, e: EvenInteger) -&gt; EvenInteger {
    a + b + c + d + e
}

// Actual syntax in Flux
#[flux::sig(fn(a:i32{a % 2 == 0}, b:i32{b % 2 == 0}, c:i32{c % 2 == 0}, d:i32{d % 2 == 0}, e:i32{e % 2 == 0}) -&gt; i32{r: r % 2 == 0})]
fn add_even_numbers(a: i32, b: i32, c: i32, d: i32, e: i32) -&gt; i32 {
    a + b + c + d + e
}
</code></pre>
<p>Refinement types are <strong>the only solution where the compiler will report violations at compile-time</strong> (contract violations will panic at runtime, and bad marker traits may not crash at all). This makes them essential for programs which must be secure and reliable. The drawback of refinement types is that <strong>current compilers are &quot;dumb&quot;* and need a lot of help to check anything beyond trivial cases</strong>: you can see the Flux website doesn't have any examples beyond <a href="https://flux-rs.github.io/flux/blog/03-vectors.html" rel="nofollow noreferrer">simple vectors</a>, and Liquid Haskell's more &quot;complicated&quot; examples (which are still fairly simple) <a href="https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_10_Case_Study_Associative_Maps.html#/program-pane-18" rel="nofollow noreferrer">use lemmas to aid the refinement checker</a>. Besides being tedious to write, the issue with lemmas is that figuring out when they're needed (vs when your program is just wrong) and then figuring out the right ones can be very difficult and unintuitive. Lastly, because the predicates and proofs are arbitrary, <strong>some refinement types are nearly or straight up impossible for the compiler to check</strong>, like:</p>
<pre class="lang-rust prettyprint-override"><code>// Classic halting problem
fn halts(program: Program) -&gt; bool { ... }

// Example return type
#[flux::sig(fn() -&gt; bool[true])]
fn impossible() -&gt; bool {
    halts(SOME_PROGRAM)
}

// Example argument type
#[flux::sig(fn(p:Program{halts(p)) -&gt; bool)]
fn safe_evaluate(program: Program) -&gt; bool { ... }
</code></pre>
<p>There's a research-project refinement type checker for Rust called <a href="https://flux-rs.github.io/flux/blog/01-introducing-flux.html" rel="nofollow noreferrer">Flux</a> (<a href="https://arxiv.org/abs/2207.04034" rel="nofollow noreferrer">paper</a>), but it seems to be in the early stages. The most popular implementation of refinement types AFAIK is <a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="nofollow noreferrer">Liquid Haskell</a>, though it still needs a lot of help for non-trivial cases and I believe hasn't been used much outside of the Liquid Haskell group themselves. Lastly, <a href="https://coq.inria.fr/" rel="nofollow noreferrer">Coq</a> has refinement types via <a href="https://coq.inria.fr/refman/addendum/program.html" rel="nofollow noreferrer">the &quot;Russel&quot; language extension, available via <code>Program</code> commands</a> (since Russel has terms of type <code>{x : T | P}</code>).</p>
<p>* I will admit the SMT solvers use some very smart algorithms. It's just that formal methods is hard: what a human assumes is obviously true by intuition, can be really difficult to prove.</p>
<h2>Extended refinement types with time / resource constraints</h2>
<p>Technically, <strong>refinement types can't check time and resource constraints</strong>. However, you could create &quot;refinement-like&quot; types, which <strong>extend the refinements from just predicates to also time and resource bounds</strong>. A hypothetical example:</p>
<pre class="lang-rust prettyprint-override"><code>fn get_1st_element&lt;T, Col: Collection&lt;T&gt;{c: c.get is O(1)}&gt;(collection: &amp;Col) -&gt; $T {
    collection.get(0).unwrap()
}
</code></pre>
<p>The problem is that AFAIK there are no such implementations like this, and <strong>time and resource bound checking is in even earlier stages</strong> (compiler would probably be even dumber at proving these). Some early attempts include <a href="https://www.raml.co/interface/" rel="nofollow noreferrer">RAML</a> (an ML which computes the time complexity of functions but doesn't assert it), and the papers <a href="https://dl.acm.org/doi/pdf/10.1145/3434308" rel="nofollow noreferrer"><em>A Unifying Type-Theory for Higher-Order (Amortized) Cost
Analysis</em></a>, <a href="https://dl.acm.org/doi/pdf/10.1145/3498670" rel="nofollow noreferrer"><em>A Cost-Aware Logical Framework</em></a>, and <a href="https://arxiv.org/pdf/2006.16233.pdf" rel="nofollow noreferrer"><em>Liquid Resource Types</em></a>.</p>
<p>Although, checking size complexity is not only possible but straightforward: just refine a collection's # of elements, or refine the value's size directly:</p>
<pre class="lang-rust prettyprint-override"><code>#[flux::fn(v:&amp;Value{size_of_val(v) &lt; 1000})]
fn cant_take_too_large_value(value: &amp;Value) { ... }
</code></pre>
<h2><a href="https://docs.racket-lang.org/reference/data-structure-contracts.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fmisc..rkt%29._any%2Fc%29%29" rel="nofollow noreferrer">Contracts</a></h2>
<p>Contracts are very similar to refinement types (and value contracts may even use the same syntax), the difference is that <strong>contracts are checked at runtime</strong>.</p>
<pre class="lang-rust prettyprint-override"><code>// You could reuse the syntax from refinement types
fn add_even_numbers&lt;T: { x: Add&lt;T, Output = T&gt; + Mod&lt;T, Output = T&gt; | x % 2 == 0 }&gt;(a: T, b: T, c: T, d: T, e: T) -&gt; T {
    a + b + c + d + e
}

// But contracts more commonly have a different syntax with `requires` and `ensures` blocks, e.g. from the `contracts` crate
#[requires(a % 2 == 0)]
#[requires(b % 2 == 0)]
#[requires(c % 2 == 0)]
#[requires(d % 2 == 0)]
#[requires(e % 2 == 0)]
#[ensures(ret -&gt; ret % 2 == 0)]
fn add_even_numbers(a: i32, b: i32, c: i32, d: i32, e: i32) -&gt; i32 {
    a + b + c + d + e
}
</code></pre>
<p>Contracts are sort of a <strong>middle ground between marker traits and refinement types: unlike marker traits they are checked</strong> (albeit at runtime), and <strong>unlike refinement types they don't require proofs</strong> (all you need is to be able to express the contract's assertion in code that runs in reasonable time, no lemmas or hard/undecidable problems). But they are not superior. <strong>Contracts' main drawback is performance</strong>: contracts must be checked every time the function is entered/exited unless the compiler is smart enough to prove them (which is rare), and <strong>some contracts (particularly ones which are <code>O(n)</code> or above, like a contract which checks every element in a large collection) are infeasibly slow to check at all</strong>.</p>
<p>Lastly of course, unless the compiler can prove the contract will always fail (again, rare), contract violations will only be detected at runtime. A rare contract violation may never show up in development or tests, but crash your server in production. At least it won't silently fail and you can track down the bug if the crash is reported.</p>
<p>Rust's <a href="https://crates.io/crates/contracts" rel="nofollow noreferrer"><code>contracts</code> crate</a> provides an implementation of contracts via proc-macro attributes on functions, which add the contract assertions to the function. Many other languages have either native or third-party support for contracts (<a href="https://en.wikipedia.org/wiki/Design_by_contract#Languages_with_native_support" rel="nofollow noreferrer">full list on Wikipedia</a>):</p>
<ul>
<li><a href="https://docs.racket-lang.org/reference/contracts.html" rel="nofollow noreferrer">Racket</a> natively, probably the most complex implementation and widely-used</li>
<li><a href="https://dlang.org/spec/contracts.html" rel="nofollow noreferrer">D</a> natively</li>
<li><a href="https://kt.academy/article/ak-contracts" rel="nofollow noreferrer">Kotlin</a> natively, but experimental and limited</li>
<li>C++ via <a href="https://www.boost.org/doc/libs/master/libs/contract/doc/html/index.html" rel="nofollow noreferrer">boost</a></li>
<li>Java via <a href="https://sebthom.github.io/oval/" rel="nofollow noreferrer">Oval</a> or <a href="https://en.wikipedia.org/wiki/AspectJ" rel="nofollow noreferrer">AspectJ</a></li>
</ul>
<h3>Time and resource contracts</h3>
<p><strong>Contracts may be able to check time and resource constraints, but not always feasibly</strong>. For example, a contract can check that a collection has <code>O(1)</code> random access by timing a bunch of random accesses on the collection and then checking whether they are roughly the same (good), or correlate in some way with the index itself (possibly <code>O(log n)</code>, <code>O(n)</code>, <code>O(n^2)</code>, etc.) A contract can check that a function doesn't run too long easily by setting a timeout and panicking if the function goes beyond the timeout. And a contract can check that a value doesn't exceed a certain length or size by asserting the size, but if doing so requires traversing the entire data-structure, it may be infeasibly slow.</p>
<pre class="lang-rust prettyprint-override"><code>#[requires(probably_has_constant_time_random_access(collection)]
fn get_1st_element&lt;T, Col: Collection&lt;T&gt;&gt;(collection: &amp;Col) -&gt; &amp;T {
    collection.get(0).unwrap()
}

fn probably_has_constant_time_random_access&lt;T, Col: Collection&lt;T&gt;&gt;(collection: &amp;Col) -&gt; &amp;T {
    let indices = 0..collection.len().into_iter().collect::&lt;Vec&lt;_&gt;&gt;();
    indices.shuffle();
    let times = indices.into_iter().take(5).map(|i| {
        time(|| collection.get(i).unwrap())
    });
    times.relative_standard_deviation() &lt; MAX_RSD_WE_STILL_ASSUME_CONSTANT_TIME
}
</code></pre>

CC BY-SA 4.0
2023-11-24T04:36:57.730Z
2023-11-24T04:42:10.770Z
2023-11-24T04:42:10.770Z
tarzh
CC BY-SA 4.0
2023-11-24T21:35:05.410Z
Spec#, Sing#, and Code Contracts.NET did compile-time verification of contracts. Unfortunately, it seems that this avenue was abandoned by Microsoft. Contracts were actually merged into .NET Framework 4, but only a couple releases later, I got the feeling MS was actively avoiding mentioning them, and now they have been removed from .NET Core and .NET and were never part of .NET Standard. From what little I understand, they were actually interpreted as something like Refinement Types. I think there is a proof somewhere that Contracts can be expressed as Refinement Types, however the worst-case
Jörg W Mittag
CC BY-SA 4.0
2023-11-24T21:37:37.233Z
… upper size bound is exponential. They always made a point of contrasting them with Eiffel's, which are checked at runtime.
Jörg W Mittag
# Expressing runtime constraints with trait-bounds
Posted by: username_0 on 2023-11-23
I've recently listened to [Corecursive episode with John A De Goes](https://corecursive.com/009-throw-away-the-irrelevant-with-john-a-de-goes/) and there's one thing that really got me thinking: the idea of type class laws pertaining to performance guarantees. The example discussed in the episode is requiring all instances of a container class type to have constant time random access to their elements.

This made me think of hypothetical Rust trait bounds where one could specify a generic type parameter adhering to some *runtime constraints*.

I understand this is probably answered in [this paper](https://dl.acm.org/doi/10.1145/3209108.3209146), at least to some degree, (found in [this answer](https://langdev.stackexchange.com/a/2713/1086) to another question), but I was hoping for a more hand-wavy, informal overview here, before even attempting to read the paper ~~(also, I don't have an access yet)~~.

**What would be some required additions to/modifications of Rust for this to become expressible with its type-system?**

Considering [Rust's golden rule](https://steveklabnik.com/writing/rusts-golden-rule), preferably this could be inferred from the function/method signature alone. I was thinking of Zig's approach of requiring explicit passing of an allocator - I'd expect it would be quite straightforward to build upon this facility to describe a generic type such that constructor of its instance doesn't require dynamic allocation. Could other runtime behaviors be "externalized"/made explicit in a similar manner, so that function signature would carry sufficient information?
**Tags:** compilers types traits compiler-inference
> **Comments:**
> **username_1**: This question feels very broad as currently put, seeking language design choices, evaluations of usefulness, instances in existing languages, commentary on first-class effects, implementation strategies, and type expressions of properties all at once. It would probably do to refine its scope down a bit to a single question. You can find the paper you're looking for [here](https://www.scs.cmu.edu/afs/cs.cmu.edu/Web/People/fp/papers/lics18.pdf), or a longer version [here](https://arxiv.org/pdf/1712.08310.pdf).  
> **username_0**: @MichaelHomer Thank you for the links! I intended the first question in bold to be *the* question and the rest just a description of my thought process and possible hints as to what exactly I am interested in. Perhaps naively, I thought these all fall under the "language design choices".  
> **username_1**: We have a close reason "Lacks objective design criteria", which is glossed as "This question solicits language designs or design tradeoffs but does not provide sufficient criteria to objectively determine what constitutes a good answer. It should be updated to include a specific design or implementation problem to be solved and should provide additional context to help focus potential answers."; that probably fits this version of the question, so it would be good to [edit] it so that it's clear that it doesn't.  
> **username_0**: Understood, will edit accordingly.  
---
## 1 answers
### Answer by username_2 on 2023-11-24. Score: 3 | Accepted answer
I see 3 ways to implement this, each with benefits and drawbacks: marker traits, refinement types, and contracts. Marker traits are already in Rust, refinement types and contracts are possible with experimental libraries.
Marker traits
Manually add a marker trait for types where the runtime constraint is met. If only some instances of a particular type satisfy the constraint, create a type-safe wrapper. In some cases you may use the type-safe wrapper and skip the trait entirely.
// Example 1
pub trait ConstantTimeRandomAccess {}
impl ConstantTimeRandomAccess for Vec {}
impl ConstantTimeRandomAccess for (T, T, T, T, T) {}
// NO
// impl ConstantTimeRandomAccess for LinkedList {}

// Example 2
pub trait EvenNumber {}
pub struct EvenInteger(i32);
pub struct EvenFloat(f32);

impl EvenNumber for EvenInteger {}
impl EvenNumber for EvenFloat {}
// NO
// impl EvenNumber for i32
pub struct NotEven;
impl TryFrom for EvenInteger { type Error = NotEven; ... }
impl TryFrom for EvenFloat { type Error = NotEven; ... }
impl Add for EvenInteger { ... }
impl Add for EvenFloat { ... }

// Usage
fn get_1st_element + ConstantTimeRandomAccess>(collection: &Col) -> &T { 
    collection.get(0).unwrap()
}
fn add_even_numbers>(a: T, b: T, c: T, d: T, e: T) -> T {
    a + b + c + d + e
}

fn main() {
    dbg!(get_1st_element(vec![1, 2, 3, 4, 5]));
    dbg!(get_1st_element(("a", "b", "c", "d", "e")));
    // Compiler error
    // dbg!(get_1st_element(LinkedList::from([1, 2, 3, 4, 5])));

    dbg!(add_even_numbers(EvenInteger::try_from(2).unwrap(), EvenInteger::try_from(4).unwrap(), EvenInteger::try_from(6).unwrap(), EvenInteger::try_from(8).unwrap(), EvenInteger::try_from(10).unwrap()));
    // Compiler error
    dbg!(add_even_numbers(1, 2, 3, 4, 5));
    // Runtime error :(
    dbg!(add_even_numbers(EvenInteger::try_from(1).unwrap(), EvenInteger::try_from(2).unwrap(), EvenInteger::try_from(3).unwrap(), EvenInteger::try_from(4).unwrap(), EvenInteger::try_from(5).unwrap()));
}

This is by far the easiest and most expressive solution, and you can use it in Rust right now. The drawback is that the compiler won't actually check the runtime characteristics of the trait, that is on you. It won't stop you from writing
impl ConstantTimeRandomAccess for LinkedList {}
impl EvenNumber for i32 {}

A drawback of the type-safe wrapper is that, in order to get a value inside of it, you must check the constraint somewhere at runtime. The optimizer may be smart enough to inline EvenInteger::try_from(2).unwrap() into a no-op, but it won't alert you that EvenInteger::try_from(3).unwrap() is guaranteed to panic.
Refinement Types (AKA Liquid Types)
Refinement types are types which have runtime constraints which are checked at compile-time, typically using SMT solvers.
Refinement type syntax may look something like this:
// Hypothetical syntax as a trait bound
fn add_even_numbers + Mod | x % 2 == 0 }>(a: T, b: T, c: T, d: T, e: T) -> T {
    a + b + c + d + e
}

// Hypothetical syntax as a type bound
type EvenInteger = {v: i32 | v % 2 == 0 };
fn add_even_numbers(a: EvenInteger, b: EvenInteger, c: EvenInteger, d: EvenInteger, e: EvenInteger) -> EvenInteger {
    a + b + c + d + e
}

// Actual syntax in Flux
#[flux::sig(fn(a:i32{a % 2 == 0}, b:i32{b % 2 == 0}, c:i32{c % 2 == 0}, d:i32{d % 2 == 0}, e:i32{e % 2 == 0}) -> i32{r: r % 2 == 0})]
fn add_even_numbers(a: i32, b: i32, c: i32, d: i32, e: i32) -> i32 {
    a + b + c + d + e
}

Refinement types are the only solution where the compiler will report violations at compile-time (contract violations will panic at runtime, and bad marker traits may not crash at all). This makes them essential for programs which must be secure and reliable. The drawback of refinement types is that current compilers are "dumb"* and need a lot of help to check anything beyond trivial cases: you can see the Flux website doesn't have any examples beyond simple vectors, and Liquid Haskell's more "complicated" examples (which are still fairly simple) use lemmas to aid the refinement checker. Besides being tedious to write, the issue with lemmas is that figuring out when they're needed (vs when your program is just wrong) and then figuring out the right ones can be very difficult and unintuitive. Lastly, because the predicates and proofs are arbitrary, some refinement types are nearly or straight up impossible for the compiler to check, like:
// Classic halting problem
fn halts(program: Program) -> bool { ... }

// Example return type
#[flux::sig(fn() -> bool[true])]
fn impossible() -> bool {
    halts(SOME_PROGRAM)
}

// Example argument type
#[flux::sig(fn(p:Program{halts(p)) -> bool)]
fn safe_evaluate(program: Program) -> bool { ... }

There's a research-project refinement type checker for Rust called Flux (paper), but it seems to be in the early stages. The most popular implementation of refinement types AFAIK is Liquid Haskell, though it still needs a lot of help for non-trivial cases and I believe hasn't been used much outside of the Liquid Haskell group themselves. Lastly, Coq has refinement types via the "Russel" language extension, available via Program commands (since Russel has terms of type {x : T | P}).
* I will admit the SMT solvers use some very smart algorithms. It's just that formal methods is hard: what a human assumes is obviously true by intuition, can be really difficult to prove.
Extended refinement types with time / resource constraints
Technically, refinement types can't check time and resource constraints. However, you could create "refinement-like" types, which extend the refinements from just predicates to also time and resource bounds. A hypothetical example:
fn get_1st_element{c: c.get is O(1)}>(collection: &Col) -> $T {
    collection.get(0).unwrap()
}

The problem is that AFAIK there are no such implementations like this, and time and resource bound checking is in even earlier stages (compiler would probably be even dumber at proving these). Some early attempts include RAML (an ML which computes the time complexity of functions but doesn't assert it), and the papers A Unifying Type-Theory for Higher-Order (Amortized) Cost
Analysis, A Cost-Aware Logical Framework, and Liquid Resource Types.
Although, checking size complexity is not only possible but straightforward: just refine a collection's # of elements, or refine the value's size directly:
#[flux::fn(v:&Value{size_of_val(v) < 1000})]
fn cant_take_too_large_value(value: &Value) { ... }

Contracts
Contracts are very similar to refinement types (and value contracts may even use the same syntax), the difference is that contracts are checked at runtime.
// You could reuse the syntax from refinement types
fn add_even_numbers + Mod | x % 2 == 0 }>(a: T, b: T, c: T, d: T, e: T) -> T {
    a + b + c + d + e
}

// But contracts more commonly have a different syntax with `requires` and `ensures` blocks, e.g. from the `contracts` crate
#[requires(a % 2 == 0)]
#[requires(b % 2 == 0)]
#[requires(c % 2 == 0)]
#[requires(d % 2 == 0)]
#[requires(e % 2 == 0)]
#[ensures(ret -> ret % 2 == 0)]
fn add_even_numbers(a: i32, b: i32, c: i32, d: i32, e: i32) -> i32 {
    a + b + c + d + e
}

Contracts are sort of a middle ground between marker traits and refinement types: unlike marker traits they are checked (albeit at runtime), and unlike refinement types they don't require proofs (all you need is to be able to express the contract's assertion in code that runs in reasonable time, no lemmas or hard/undecidable problems). But they are not superior. Contracts' main drawback is performance: contracts must be checked every time the function is entered/exited unless the compiler is smart enough to prove them (which is rare), and some contracts (particularly ones which are O(n) or above, like a contract which checks every element in a large collection) are infeasibly slow to check at all.
Lastly of course, unless the compiler can prove the contract will always fail (again, rare), contract violations will only be detected at runtime. A rare contract violation may never show up in development or tests, but crash your server in production. At least it won't silently fail and you can track down the bug if the crash is reported.
Rust's contracts crate provides an implementation of contracts via proc-macro attributes on functions, which add the contract assertions to the function. Many other languages have either native or third-party support for contracts (full list on Wikipedia):

Racket natively, probably the most complex implementation and widely-used
D natively
Kotlin natively, but experimental and limited
C++ via boost
Java via Oval or AspectJ

Time and resource contracts
Contracts may be able to check time and resource constraints, but not always feasibly. For example, a contract can check that a collection has O(1) random access by timing a bunch of random accesses on the collection and then checking whether they are roughly the same (good), or correlate in some way with the index itself (possibly O(log n), O(n), O(n^2), etc.) A contract can check that a function doesn't run too long easily by setting a timeout and panicking if the function goes beyond the timeout. And a contract can check that a value doesn't exceed a certain length or size by asserting the size, but if doing so requires traversing the entire data-structure, it may be infeasibly slow.
#[requires(probably_has_constant_time_random_access(collection)]
fn get_1st_element>(collection: &Col) -> &T {
    collection.get(0).unwrap()
}

fn probably_has_constant_time_random_access>(collection: &Col) -> &T {
    let indices = 0..collection.len().into_iter().collect::>();
    indices.shuffle();
    let times = indices.into_iter().take(5).map(|i| {
        time(|| collection.get(i).unwrap())
    });
    times.relative_standard_deviation() < MAX_RSD_WE_STILL_ASSUME_CONSTANT_TIME
}
> **Comments:**
> **username_3** (2023-11-24): Spec#, Sing#, and Code Contracts.NET did compile-time verification of contracts. Unfortunately, it seems that this avenue was abandoned by Microsoft. Contracts were actually merged into .NET Framework 4, but only a couple releases later, I got the feeling MS was actively avoiding mentioning them, and now they have been removed from .NET Core and .NET and were never part of .NET Standard. From what little I understand, they were actually interpreted as something like Refinement Types. I think there is a proof somewhere that Contracts can be expressed as Refinement Types, however the worst-case  
> **username_3** (2023-11-24): … upper size bound is exponential. They always made a point of contrasting them with Eiffel's, which are checked at runtime.  
---
