> {-@ LIQUID "--no-termination" @-}
> {-@ LIQUID "--short-names" @-}
>
> module Basics where
>
> import Prelude hiding (head, max)
> import qualified Data.ByteString.Char8 as B
> import qualified Data.ByteString.Unsafe as B
> import Data.List (find)
> import Language.Haskell.Liquid.Prelude
Well-typed programs can't go wrong.
> dog = B.pack "dog"
< λ> B.unsafeIndex dog 2
< 103
< λ> B.unsafeIndex dog 10
< 0
< λ> B.unsafeIndex dog 10000000000
< segmentation fault
That's no good, it would be nice if the type system could prevent us from doing
that. Today I'm going to present our experience in designing such a type system,
and in using it to verify over 10KLoC of real Haskell code.
Refinement Types
================
We'll start with a lightning tour of LiquidHaskell before getting into the
gritty benchmarks.
A refinment type is a Haskell type where each component of the type is annotated
with a predicate from an SMT-decidable logic. For example,
< {v:Int | v >= 0 && v < 100}
describes the set of `Int`s that are between 0 and 100. We'll make heavy use of
*aliases* to simplify the types, e.g.
> {-@ predicate Btwn Lo N Hi = Lo <= N && N < Hi @-}
> {-@ type Rng Lo Hi = {v:Int | Btwn Lo v Hi} @-}
< Rng 0 100
is equivalent to the first type.
To double check note that,
> {-@ okRange :: [Rng 0 100] @-}
> okRange = [1,10,30] :: [Int]
but, of course,
> {-@ badRange :: [Rng 0 100] @-}
> badRange = [1,10,300] :: [Int]
We can describe a function's *contract* by refining its input and output types
with our desired pre- and post-conditions.
> {-@ range :: lo:Int -> hi:{Int | lo <= hi} -> [Rng lo hi] @-}
This type tells us that `range` accepts two `Int`s, the second being larger than
the first, and returns a `[Int]` where all of the elements are between `lo` and
`hi`. Now if we implement `range`
> range :: Int -> Int -> [Int]
> range lo hi
> | lo <= hi = lo : range (lo + 1) hi
> | otherwise = []
LiquidHaskell complains that `lo` is not *strictly* less than `hi`!
Fortunately, that's easily fixed, we'll just replace the `<=` in the guard with `<`.
> {-@ range' :: lo:Int -> hi:{Int | lo <= hi} -> [Rng lo hi] @-}
> range' :: Int -> Int -> [Int]
> range' lo hi
> | lo < hi = lo : range' (lo + 1) hi
> | otherwise = []
Holes
-----
Typing out the base Haskell types can be tedious, especially since GHC will
infer them. So we use `_` to represent a *type-hole*, which LiquidHaskell will
automatically fill in by asking GHC. For example, if we wrote a function
`rangeFind` with type
< (Int -> Bool) -> Int -> Int -> Maybe Int
we could write the refined type
> {-@ rangeFind :: _ -> lo:_ -> hi:{_ | lo <= hi} -> Maybe (Rng lo hi) @-}
> rangeFind f lo hi = find f $ range lo hi
Note that in order for `rangeFind` to type-check, LiquidHaskell has to infer
that `find` returns a `Maybe (Rng lo hi)` (show off liquid-pos-tip), which it
does by instantiating `find`s type parameter `a` with `Rng lo hi`.
Ok, we can talk about Integers, what about arbitrary, user-defined datatypes?
Measures
========
Let's go one step further with `range` and reason about the length of the
resulting list. Given that
< range 0 2 == [0,1]
and
< range 1 1 == []
it looks like the length of the output list should be `hi - lo`, but how do we
express that in LiquidHaskell?
(Instead of defining an index that is baked into the type definition)
we'll define a *measure*, which you can think of as a *view* of the datatype.
< {-@ measure len :: [a] -> Int
< len ([]) = 0
< len (x:xs) = 1 + (len xs)
< @-}
Measures look like Haskell functions, but they're *not*. They are a very
restricted subset of inductively-defined Haskell functions with a single
equation per data constructor. LiquidHaskell translates measures into refined
types for the data constructors, e.g.
< [] :: {v:[a] | len v = 0}
< (:) :: _ -> xs:_ -> {v:[a] | len v = len xs + 1}
ASIDE: another great spot to show off liquid-pos-tip.
NV: state that measures are uninterpreted functions into logic
> mylist = 1 : []
LiquidHaskell's interpretation of measures is a key distinction from indexed
data types, because we can define multiple measures independently of the actual
type definition, and LiquidHaskell will just conjoin the refinements arising
from the individual measures.
ASIDE: perhaps quickly show by defining `measure null` as a throwaway.
With our measure in hand we can now specify our final type for `range`
> {-@ range'' :: lo:Int -> hi:{Int | lo <= hi} -> {v:[Rng lo hi] | len v = hi - lo } @-}
Notice that we don't need to change the implementation at all, LiquidHaskell
accepts it as is!
> range'' :: Int -> Int -> [Int]
> range'' lo hi
> | lo < hi = lo : range'' (lo + 1) hi
> | otherwise = []
We can also give precise specifications to, e.g., `append`
> {-@ append :: xs:_ -> ys:_ -> {v:_ | len v = len xs + len ys} @-}
> append [] ys = ys
> append (x:xs) ys = x : append xs ys
Refined Data Types
------------------
Sometimes we *want* every instance of a type to satisfy some invariant. Every
row in a `CSV` table should have the same number of columns.
NV: Universal invariants that we get by type polymorphism is not trivial,
so maybe give a simple type like [{v:Int | v > 0}]
before going into [ListL a cols]
> data CSV a = CSV { cols :: [String], rows :: [[a]] }
> {-@ type ListL a L = {v:[a] | len v = len L} @-}
> {-@ data CSV a = CSV { cols :: [String], rows :: [ListL a cols] } @-}
Since the invariant is *baked into* the refined type definition, LiquidHaskell
will reject *any* `CSV` value that does not satisfy the invariant.
> good_2 = CSV [ "Month", "Days"]
> [ ["Jan", "31"]
> , ["Feb", "28"] ]
> bad_2 = CSV [ "Month", "Days"]
> [ ["Jan", "31"]
> , ["Feb"] ]
RJ:BEGIN-CUT
Refined Type-Classes
--------------------
Perhaps there's a common interface that we want multiple data types to support,
e.g. random-access. Many such interfaces have protocols that define how to
*safely* use the interface, like "don't index out-of-bounds". We can describe
these protocols in LiquidHaskell by packaging the functions into a type-class
and giving it a refined definition.
> class Indexable f where
> size :: f a -> Int
> at :: f a -> Int -> a
>
> {-@
> class Indexable f where
> size :: forall a. xs:f a -> {v:Nat | v = sz xs}
> at :: forall a. xs:f a -> {v:Nat | v < sz xs} -> a
> @-}
This poses a bit of a problem though, how do we define the `sz` measure?
Measures have to be defined for a specific datatype so LiquidHaskell can refine
the constructors. We'll work around this issue by introducing *type-indexed*
measures.
> {-@ class measure sz :: forall a. a -> Int @-}
> {-@ instance measure sz :: [a] -> Int
> sz ([]) = 0
> sz (x:xs) = 1 + (sz xs)
> @-}
> {-@ invariant {v:[a] | sz v >= 0} @-}
Apart from allowing definitions for multiple types, class measures work just
like regular measures, i.e. they're translated into refined data constructor
types.
If we go ahead and define an instance for lists,
> instance Indexable [] where
> size [] = 0
> size (x:xs) = 1 + size xs
>
> (x:xs) `at` 0 = x
> (x:xs) `at` i = xs `at` (i-1)
LiquidHaskell will verify that our implementation matches the class
specification.
Clients of a type-class get to assume that the instances have been defined
correctly, i.e. LiquidHaskell will happily prove that
> sum :: (Indexable f) => f Int -> Int
> sum xs = go 0
> where
> go i | i < size xs = xs `at` i + go (i+1)
> | otherwise = 0
is safe for **all** instances of `Indexable`.
Abstract Refinements
--------------------
All of the examples so far have used *concrete* refinements, but sometimes
we just want to say that *some* property will be preserved by the function, e.g.
> max :: Int -> Int -> Int
> max x y = if x > y then x else y
>
> {-@ xPos :: {v: _ | v > 0} @-}
> xPos = max 10 13
>
> {-@ xNeg :: {v: _ | v < 0} @-}
> xNeg = max (0-5) (0-8)
>
> {-@ xEven :: {v: _ | v mod 2 == 0} @-}
> xEven = max 4 (0-6)
Since `max` returns one of it's arguments, we know that if *both* inputs share
some property, then *so will the output*. In LiquidHaskell we can express this
by abstracting over the refinements.
> {-@ max :: forall Prop>.
> Int
-> Int
-> Int
> @-}
RJ:END-CUT
Now that we've covered the basics of using LiquidHaskell, let's take a look at
our first experiment: proving functions total.