24 days of Hackage, 2015: day 23: Liquid Haskell: refinement types for the real world

Table of contents for the whole series

A table of contents is at the top of the article for day 1.

Day 23

(Reddit discussion)

During the course of this article series “24 days of Hackage, 2015”, I’ve made an effort to give a flavor of using QuickCheck to specify contracts that should be satisfied by our code that are not checked at compile time but are checked through randomized testing at run time. But we know that just because code has hundreds or thousands of tests, that is not a proof that code is actually correct for all possible cases. I’ve also used newtype as a way of indicating intent that I want to restrict legal values for a type, such as on day 15 when I laboriously intended refinements of existing types but with no automatically checkable proof that I was populating them correctly.

-- | User input without a newline, and not equal to "secret".
newtype NotSecretString =
  NotSecretString { getNotSecretString :: NotNewlineString }

type NotNewlineString = [NotNewlineChar]

newtype NotNewlineChar =
  NotNewlineChar { getNotNewlineChar :: Char }
  deriving (Show)

This is why I’m so excited about Liquid Haskell, a static analysis system for Haskell that is under very active development. It provides a refinement type system that allows you to write, in a natural and clear way, certain varieties of contracts that can be verified at compile time. I believe this sort of system will be a game changer in the future of programming languages.

What is a refinement type?

A refinement type is a type with some predicate that “refines” what possible values are allowed. In Liquid Haskell, you can add refinement type annotations to Haskell code, embedded in ordinary Haskell comments, and also write your own predicates. It’s great that Liquid Haskell can be introduced into existing Haskell code without disruption or requiring that the Liquid Haskell checker be run in order to compile the Haskell code.

As an example (taken from an official demo), below we have an ordinary key-value association list data type and then we have values of two different refinements of the type where we wanted to check at compile time that the integer key is constrained in the desired way.

data AssocP k v = KVP [(k, v)]

{-@ digitsP :: AssocP {v:Int | (Btwn 0 v 9)} String @-}
digitsP :: AssocP Int String
digitsP = KVP [ (1, "one")
              , (2, "two")
              , (3, "three") ]

{-@ sparseVecP :: AssocP {v:Int | (Btwn 0 v 1000)} Double @-}
sparseVecP :: AssocP Int Double
sparseVecP = KVP [ (12 ,  34.1 )
                 , (92 , 902.83)
                 , (451,   2.95)
                 , (877,   3.1 )]

{-@ predicate Btwn Lo V Hi = (Lo <= V && V <= Hi) @-}

One thing to note about refinement types is that an expression can have more than one refinement type that you define. For example, an Int refined to being between 0 and 9 is of course also an Int refined to being between 0 and 20.

You can use refinements for preconditions and postconditions, and refine function types.

Great live demo site!

Go to the interactive live Liquid Haskell demo site!

Because an excellent demo site already exists, I’m not going to walk through any examples of using Liquid Haskell, although I may look into going back to my old code to retroactively start adding use of Liquid Haskell.

The demo site has dozens of fully worked out examples, embedded in a live environment where you can change the code and rerun the checker to see what happens. Examples include defining a refinement type of a sorted list, so that you can write a sorting function of type (Ord a) => [a] -> IncrList a in which the type requires that it is proved by the solver that your sorting function actually performs a sort as advertised.

How do refinement types work?

Liquid Haskell works by going from refinements to a collection of logic constraints whose verification is outsourced to an off-the-shelf SMT solver, such as Z3, which needs to be installed. (On Mac OS X, I install Z3 with brew install z3.)

I have installed Liquid Haskell globally using Stack:

$ stack install liquidhaskell intern liquid-fixpoint

This installs the liquid executable that you run.

Tutorials, books, blog, discussion group

An extensive, free book, “Programming with Refinement Types: An Introduction to Liquid Haskell”, available both as PDF and as a beautifully readable HTML version.

The Liquid Haskell GitHub repo, with lots of activity there.

The Liquid Haskell blog.

The Google group mailing list.

(Update of 2015-12-30)

Gabriel Gonzalez has put up a tutorial.

Videos

The Liquid Haskell team has been very active in giving presentations about their work. Here are some:

Ranjit Jhala, “Refinement Types for Haskell”

This is from 2014:

(Update of 2015-12-30)

There is a full LambdaConf 2015 video here:

Eric Seidel, “Refinement Types for the Real World”

Niki Vazou, “Bounded Refinement Types”

The recent paper on this work is here.

A note on full-blown dependent types

You might wonder what the relationship is between refinement types and a full-blown dependent type system. I see them both as useful techniques. With full-blown dependent types you can write really fancy types that encode various forms of information (and I’m interested in using dependent types more in 2016 also), but the flexibility and feel of using refinement types seems a win for problems where it is very natural to write down amenable predicates and also to work incrementally, refining gradually.

Conclusion

I’m very excited about Liquid Haskell because it’s bringing refinement types into a real world setting. I expect to try to make real use of it in the coming year, 2016.

All the code

All my code for my article series are at this GitHub repo.