3 ms·
I think Yatima's type system is intended to be more powerful than Rust's. In particular, its dependent types would allow the compiler to enforce properties of d
by nicoty 5y ago
I think Yatima's type system is intended to be more powerful than Rust's. In particular, its dependent types would allow the compiler to enforce properties of data at compile time. E.g., it can be used to ensure that function only accepts/returns a list of values of a particular length (aka a vector) at compile time, which afaik isn't possible with Rust's type system.
- jcburnham 5y agoOh, yeah, I didn't even mention this on my other comment, haha. Rust doesn't have dependent-types (except outside of a few niche places like const-generics) and only limited/non-user-exposed sub-structural types. There's a whole range of interesting applications that that those features open up, from compiler optimizations to formal verification.