Would it make sense for Julia to adopt refinement types?

Internals & Design
1

Refinement types enrich a language’s type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code.

Rust and some other programming languages are experimenting with them.

Would it make sense for Julia to have them?

1 Like
2

Sounds like what we call “interfaces” (e.g. AbstractArray), and although there is no official formalism, there are several attempts worth mentioning like Interfaces.jl or RequiredInterfaces.jl

5 Likes
3

I may be wrong, but it seems that refinement types restrict the range of possible values of a type, while Interfaces.jl or RequiredInterfaces.jl help to restrict types that do not have certain methods.

For example, refinement types help to restrict the range of acceptable values that the absolute function can return.

#[flux::sig(fn (n:i32) -> i32{v:0<=v && n<=v})]
pub fn abs(n: i32) -> i32 {
    if 0 <= n {
        n
    } else {
        0 - n
    }
}

https://flux-rs.github.io/flux/blog/01-introducing-flux.html

2 Likes
4

That is correct, but since refinement types are much more complicated to both implement & use than more simple interfaces (which we’d still need either way), I think the point of @gdalle is that the current problems in the Julia ecosystem would not be addressed by just adding refinement types.

Yes, that is correct. Note that the example given doesn’t translate to Julia, because of the underflow on 0 - typemin(Int32). In Julia, this is always defined as wraparound arithmetic, while IIRC this panics in Rust in debug mode.

EDIT:

In release mode, rustc doesn’t even want to compile this: Rust Playground

3 Likes
5

Understood. Refinement types wouldn’t solve any problems that the Julia ecosystem has, but they would open up Julia to new applications like Liquid Haskell did in the Haskell ecosystem.

1 Like
6

Personally I’m quite a fan of the idea of refinement types in Julia, and find the paper you linked rather compelling.

We often write code that requires positive, even, or non-empty values, and so a type system that allows for this level of detail to be specified both seems like a route for a higher standard of robustness that is possible to be specified using “plain” old interfaces.

The way I like to look at refinement types is that they’re compile-time contracts. My understanding is that the main complexity as a result is that suddenly you then need something like Z3 in the compiler, and describing that as a tough sell seems like an understatement.

For a quick intro and a motivating example, I’d recommend this short article introducing Haskell’s refined library: Announcing the refinement types library – Functional programming debugs you

4 Likes
7

I’m understanding 10% of this at most, but I think I’m seeing at least 2 very different approaches going on. Rust’s seems to leave the original type alone, but the compiler errors when an asserted condition of its values can’t be proven. Haskell’s on the other hand wraps the type into a separate Refined type, and you must unrefine it to extract the value for normal computation. Apparently unwrapping is done at compile-time (no runtime cost), and the wrapping and verification can be done at compile-time with refineTH; there is also refineTH_ to refine then unrefine immediately, which I’m interpreting as a compile-time assertion.

Either way, it sounds like static analysis and AOT compilation, so I’m not sure how it’ll fit well into Julia. The Rust code examples I (think I) understand rely on computation of values knowable at compile-time; does that mean we need runtime verification otherwise, especially in interactive sessions? I’m definitely too unfamiliar with the topic and languages to know how formal verification is used and how refinement types play into that.

1 Like
8

I would love to see refinement types myself. Having tinkered with Ada/SPARK in the past, I am convinced this is great and straightforward way to avoid many bugs.

Once the annotations are in place, a lot can be done to improve program quality, from injecting dynamic tests, to a full formal verification of the entire program.

It is not clear if there is a single best approach, probably a mix of different approaches is best.

As a first step, we’d need a way to attach additional specifications to variables or return values of functions, such as

  • range
  • set membership
  • arbitrary predicates

I don’t think there is currently a way to add attributes to variables, but the user-facing syntax could look like this:
@annotation 0 < x < 10
@annotation myPredicate(x) == true
The annotations could also go into docstrings:

"""
N counts the 
@annotation n > 0
"""
n::Integer

Based on these annotations, libraries could generate tests, add dynamic checks, or try to statically prove the assertions.

Such checks would not have to be part of the core, different verification tools could use different approaches. As an example, one tool could verify ranges, while another tool could verify physical units.

Some libraries to study for inspiration:

https://docs.adacore.com/spark2014-docs/html/ug/en/source/type_contracts.html#predicates

These annotations could also be used, very naturally, to implement design by contract:

https://www.cs.cmu.edu/~csd-phd-blog/2023/rust-verification-with-verus/

Variable annotations would also nicely enable design by contract

Additionally, they would also be useful for physical units, e.g. through Unitful.jl.

3 Likes