One of the best talks of the last LambdaConf, “LambdaConf 2015 - LiquidHaskell Refinement Types for Haskell Ranjit Jhala”:
In this talk he actually teaches you the basics of LiquidHaskell, this is awesome. For certain kinds of code I’d like to use a “LiquidRust” (but with its types better integrated in Rust).
During the talk he uses this active document (similar to Rust by example):
There is also a language with a similar (but better?) type system:
The type refinements, automatically proved by the Z3 SMT solver, are able to remove bound tests from arrays (while keeping the program safe), avoid other mistakes, and generally they could help the compiler produce more efficient binaries and remove some kinds of bugs. This seems quite fitting for the Rust design purposes (despite perhaps you don’t want to refine all the types of your Rust program, or to use refinement typing in all your Rust programs. There are probably situations where using refinement typing is overkill or too much work. But I think a “gradual typing” with refinement typing is possible).
LiquidHaskell is an optional type system that you can lay over the regular Haskell type system. LiquidHaskell programs are just regular Haskell programs with some added comments that express the refined types. If you remove those comments, the Haskell code still compiles.
But it’s not just a matter of adding an optional type system. If you have refinement typing you can be sure a certain function always returns a meaningful result. So if currently such Rust function returns an Option<> you are wasting CPU registers and CPU instructions. Such function doesn’t need to return an Option. So refinement typing influences the design of the API too. If you introduce some kind of refinement typing in Rust you may want to rewrite some functions (or better to add alternative functions) of its standard library to not return Option/Result, but to return just the naked value…