Liquid Types for Haskell

Niki Vazou, Eric Seidel, and Ranjit Jhala

UC San Diego

Try liquidHaskell

By raising Exceptions...

div :: Int -> Int -> Int

>> 1 `div` 0 :: Int
>> *** Expeption: divide by zero

of many kinds

(!!) :: [a] -> Int -> a

>> [1, 2, 3] !! 4 :: Int
>> *** Expeption: index too large

Or by having "unexpected behaviour"...

sort :: [Int] -> [Int]

>> sort [4, 2, 35, 4, 6] :: [Int]
>> [6, 4, 35, 2, 4]

Refine Classical Types with Logical Predicates

NotZero = {v:Int | v != 0}

By preventing Exceptions...

div :: Int -> NotZero -> Int

>> 1 `div` 0 
>> Refinement Type Error

of many kinds

(!!) :: xs: [a] -> Range(0, len xs) -> a

>> [1, 2, 3] !! 4
>> Refinement Type Error

Or by enforcing "expected behaviour"...

sort :: [Int] -> IncreasingList

>> sort [4, 2, 35, 4, 6] :: [Int]
>> [2, 4, 4, 6, 35]