LiquidHaskell: Liquid Types for Haskell

Niki Vazou

(UC San Diego)
(Awake Networks)

LiquidHaskell at Awake Networks

- Verification of packet-analysis - all functions are terminating & total - safe ByteString indexing

Well-Typed Programs Can Go Wrong

The Heartbleed Bug.

Heartbleed is a security bug in the OpenSSL cryptography library (April 2014).

The HEartbleed Bug.

The Heartbleed Bug in Haskell

λ> :m +Data.Text Data.Text.Unsafe
λ> let text = pack "Niki"
λ> :t takeWord16
    takeWord16 :: Int -> Text -> Text

True is a bad argument

λ> takeWord16 True text

    Couldn't match expected type ‘Int’ with actual type ‘Bool’
    In the first argument of ‘takeWord16’, namely ‘True’
    In the expression: takeWord16 True text

But, 10 is a good argument

Reveal 6 extra characters...
λ>  takeWord16 10 text

Partial Functions

λ> :t head
head :: [a] -> a

λ> head "Awake"

λ> head []
*** Exception: Prelude.head: empty list

Functional Correctness

λ> fib 1 <= fib 42
λ> mapReduce 42 sum (+) [1..20]

Goal: Extend Type System

  • To prevent wider class of errors

  • To enforce program specific properties


  1. Refinements Types
  2. Data Types
  3. Termination
  4. Reflection
  5. Case Study: MapReduce
  6. Awake Statistics


  • Diverse Code Bases

  • 10KLoc / 56 Modules

  • Memory Safety, Termination, Functional Correctness

Inference is Crucial


  • Specifications: 1 / 10 LOC (ok)

  • Compile Time: 1s / 10 LOC (not ok!)


Refinement Types: Automated Dependent Typing via SMT

Properties: Predicates + Types
Proofs: SMT Solvers + Subtyping
Inference: Abstract Interpretation + Hindley-Milner

Thank You!

cabal install liquidhaskell
online demo @