LiquidHaskell Refinement Types for Haskell


#1

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):
http://ucsd-progsys.github.io/lh-workshop/

There is also a language with a similar (but better?) type system:
https://www.fstar-lang.org/

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…


#2

Perhaps it could be implemented as some sort of plugin first? Certainly looks very useful, but it does look like it would be hard to add it in a backwards compatible way…


#3

This is useful reading, authored by the speaker: Programming with Refinement Types: An Introduction to LiquidHaskell.


#4

I’ve said “better integrated” because if the refined types find a particular array access can’t be out of bounds, the compiler must use get_unchecked/get_unchecked_mut, even in safe code. Without such integration, the refinement typing is less useful.

This shows a basic implementation:

A possible syntax for the type refinements (better integrated in the language compared to LiquidHaskell):

let x: i32 { x >= 0 } = 10;

There’s also need for few new keywords like “lemma”, and some effect typing as in F*.

Can you explain why? Do you mean in Rust, its type system, or its standard library?


#5

Ah, sorry. Yes, I mean to get full advantage out of it, you’d want the standard library annotated. But this could cause breakages to existing code.