Assumed audience: Software Engineers and Researchers that welcome interesting type systems.
This past Friday, Catarina presented the result of our work identifying what are exactly the usability barriers to adopting Liquid Types.
Liquid Types were initially proposed 17 years ago, and there have been several implementations (targeting ML, C, Javascript, Haskell, Rust, Java). Of these, LiquidHaskell is the most mature and stable. But none of these has become mainstream, not even mainstream in the Haskell community (which is a very specific definition of mainstream).
In this paper we interviewed both past users of LiquidHaskell to understand what have been the challenges as well as take new users thought the LiquidHaskell tutorial and try to understand what are the limitations.
Liquid Types: a primer
Informally, Liquid Types (from Logically Quantified Types) are type systems that allow programmers to refine basic types with predicates drawn from a decidable logic. In practice, it means that we can statically check whether the predicates are true using SMT Solvers.
In practice, it means that you can reason about some things, but not another. However, knowing exactly where this boundary lies is one of the identified challenges.
def f(i: Int | i > 0) : (j:Int | j > i + 1) = ....In this example, the function input is an integer, but it has to be greater than 0 (that is the refinement!). And the function returns a number that is at least 1 larger than the input (that is not only a refined type, but also a dependent type as the type depends on some value that exists in the program.
If you have used Lean, Agda or Coq, Liquid Types are way more limited than the Full Dependent Types that you are used to. But you don’t have to write proofs, the SMT solver will do the proofs for you.
Liquid Types allow you to have guarantees that your program never divides by zero, does not have accesses to positions out of bounds in arrays. More interesting properties rely on the programmer defining auxiliary properties (measures in Liquid Haskell lingo) that keep track of relevant aspects of the program. For instance, we have used this to prevent machine learning classifiers that require balanced datasets from being used with unbalanced datasets. This is done without even running the program (useful if it takes hours to load the dataset just to fail immediately afterwards).
Challenges
One of the main limitations is the lack of proper documentation. The Lean community has also identified this issue and recruited David Thrane Christiansen to write most of it.
In Liquid Types one of the issues is documentation what can and should be used in liquid types. We probably need a very long page of examples (like the seaborn gallery) where users can get ideas of how to use it. We also need some syntactic affordance (ideally interactive) about what is available to be written in refinements (for example, x*2 is okay, but x*y may not be!).
Related to this issue, we need better error messages. Some error messages can include 100 variables and expressions, and it is almost impossible to figure out the problem. We can simplify those expressions, but an error like “3 is not smaller than 2” is also not very useful, without tracking the provenance of those constants. My hypothesis is that an interactive error explorer might be more useful. This is something our group will work on the next couple of months.
Another source of problems is the distinction between Haskell and LiquidHaskell. Not everything that you can write in Haskell is available in the predicates. Furthermore, there other infrastructure issues like needing annotations for Haskell libraries. In our lab, we are working on Aeon, a programming language that has native liquid types, and uses them for automatically generating code. I believe having first-class liquid types will reduce many of the issues when trying Liquid Types.
The most challenging issues are related with writing proofs, especially when you need to include manual proofs to help the SMT solver reason about your code. In practice, you should use Lean for those use cases, because the ergonomics are much better for using manual proofs. In my view, Liquid Types should be used mostly for automated verification, serving as a lightweight system for some assurances about the code. Detecting what are those useful features requires expertise in liquid types and cannot be easily passed on the newcomers. Overcoming this barrier is also a big challenge.
h3 Next Steps
In our lab, we’re planning on addressing first-class liquid types with Aeon and also improving error messages with interactivity. In the University of Lisbon, we are always looking for collaborations and students to work on tackling these challenges.
If you want to learn Liquid Types, you can start with Liquid Haskell, at least until we have the LiquidJava or Aeon tutorials up and going.