An example of subtyping for safety and performance


#1

For a comparison I’ve implemented two small programs, porting it from Java code ( https://www.reddit.com/r/haskell/comments/6znim3/performance_enumerating_all_3674160/ ), this is an (useless) extract of the Rust code:

const N: usize = 24;
type Config = [u8; N];

type Indexes = [usize; N];
const OP0: Indexes = [1,3,0,2,21,20,6,7,4,5,10,11,12,
                      13,14,15,9,8,18,19,16,17,22,23];

fn update(cfg: &Config) -> Config {
    let mut new_cfg: Config = Default::default();
    for i in 0 .. N {
        new_cfg[i] = cfg[OP0[i]];
    }
    new_cfg
}

fn main() {
    use std::str::from_utf8_unchecked;

    const SOLVED: &'static Config = b"RRRRYYYYBBBBOOOOWWWWGGGG";

    let new_cfg = update(SOLVED);

    println!("{}", unsafe { from_utf8_unchecked(&new_cfg) });
}

In this code I’d like to avoid using unsafe code, but I’d also like to keep the performance of from_utf8_unchecked(), avoiding useless UTF8 testing. A way to do this is to introduce subtypes in Rust:

// subtype with enumeration:
subtype Cfg: Ascii = [b'R', b'Y', b'B', b'O', b'W', b'G'];

// Simpler less strict alternative, ranged subtype:
subtype Cfg: Ascii = b'B' ... b'W';

type Config = [Cfg; N];

const SOLVED: &'static Config = b"RRRRYYYYBBBBOOOOWWWWGGGG";

// Using:
fn from_ascii(_: &[Ascii]) -> &str;

// Sloppy typing, subtype implicits converts to the type Ascii:
println!("{}", from_ascii(&new_cfg));

// Alternative:
println!("{}", str::from(&new_cfg));

// More strongly typed alternative:
println!("{}", str::from(Ascii::from(&new_cfg)));

In the last alternative Ascii::from() converts a subtype of Ascii to Ascii. (Note: Ada language has a similar useful feature since long time).


#2

I also want more tools to work with ascii text, converting to and from strings are pretty painful (and slow!). However, I don’t think you need sub-typing to accomplish this at all. Having an AsciiStr type in the stdlib with the appropriate From and Deref impls would alleviate most of the pain. The only thing missing would be an ascii string literal (or a const fn constructor for AsciiStr).


#3

However, I don’t think you need sub-typing to accomplish this at all.

Right, subtyping isn’t not necessary to write Rust code, but I can show you twenty more examples where integral subtyping is useful, it’s a handy feature I’ve missed since the first days of using Rust. So this post was not about Ascii strings, it was just an example of using Ada-style subtypes… I’ll show more usage examples in future posts.


#4

I would not really describe that as “subtyping”. For me, subtyping emphasizes the aspect that one type can be implicitly converted into another, which I think misses the point here.

This is more like “refinement types”: where a type is associated with some arbitrary, possibly nontrivial predicate. As the constraints become more complicated, you’d eventually need an SMT solver to solve it. Haskell has this in the form of a separate tool called LiquidHaskell. Rust could follow a similar route and have a separate implementation using the compiler API.


#5

I would not really describe that as “subtyping”. For me, subtyping emphasizes the aspect that one type can be implicitly converted into another, which I think misses the point here.

In my first post here I’ve shown both situations, Cfg as implicitly convertible to Ascii or not. It’s a design decision, and in this post I am not assumed people want one or the other designs. It still needs a decision.

This is more like “refinement types”: where a type is associated with some arbitrary, possibly nontrivial predicate. As the constraints become more complicated,

No need for refinement typing here and SMT solvers here. It’s just a subset of an integral type, expressed by enumeration or slicing, not general static predicates. It’s an Ada feature. Refinement typing requires a complex language design, lot of work to use them in user code, and the code checking during the compilation requires time (and Rust code compiles slowly already). I prefer to keep things simple and efficient (and my proposal could even be designed to be future-syntax-compatible with refinement typing). If you propose very complex features from the start the probability of seeing the idea implemented are low. Integral subyping isn’t as flexible as refinement typing, but it covers a very wide number of cases in Rust code, and helps give more precision to code (stronger typing) and to avoid some bugs.