1
$\begingroup$

I've recently listened to Corecursive episode 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, at least to some degree, (found in this answer 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, 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?

$\endgroup$
4
  • 1
    $\begingroup$ 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, or a longer version here. $\endgroup$
    – Michael Homer
    Nov 23, 2023 at 19:43
  • $\begingroup$ @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". $\endgroup$
    – gstukelj
    Nov 23, 2023 at 20:08
  • $\begingroup$ 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. $\endgroup$
    – Michael Homer
    Nov 23, 2023 at 20:13
  • $\begingroup$ Understood, will edit accordingly. $\endgroup$
    – gstukelj
    Nov 23, 2023 at 20:14

1 Answer 1

1
$\begingroup$

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<T> ConstantTimeRandomAccess for Vec<T> {}
impl<T> ConstantTimeRandomAccess for (T, T, T, T, T) {}
// NO
// impl<T> ConstantTimeRandomAccess for LinkedList<T> {}

// 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<i32> for EvenInteger { type Error = NotEven; ... }
impl TryFrom<f32> for EvenFloat { type Error = NotEven; ... }
impl Add for EvenInteger { ... }
impl Add for EvenFloat { ... }

// Usage
fn get_1st_element<T, Col: Collection<T> + ConstantTimeRandomAccess>(collection: &Col) -> &T { 
    collection.get(0).unwrap()
}
fn add_even_numbers<T: EvenNumber + Add<T, Output = T>>(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<T> ConstantTimeRandomAccess for LinkedList<T> {}
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<T: { x: Add<T, Output = T> + Mod<T, Output = T> | 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<T, Col: Collection<T>{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<T: { x: Add<T, Output = T> + Mod<T, Output = T> | 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<T, Col: Collection<T>>(collection: &Col) -> &T {
    collection.get(0).unwrap()
}

fn probably_has_constant_time_random_access<T, Col: Collection<T>>(collection: &Col) -> &T {
    let indices = 0..collection.len().into_iter().collect::<Vec<_>>();
    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
}
$\endgroup$
2
  • 1
    $\begingroup$ 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 $\endgroup$ Nov 24, 2023 at 21:35
  • 1
    $\begingroup$ … upper size bound is exponential. They always made a point of contrasting them with Eiffel's, which are checked at runtime. $\endgroup$ Nov 24, 2023 at 21:37

This site is temporarily in read-only mode and not accepting new answers.

Not the answer you're looking for? Browse other questions tagged .