pwrt

Synopsis

Some notes, quotes & examples that I take while reading the Programming with Refinement Types book.

Setup

You need to install z3 4.7.1 for now (They just made some changes that makes 4.8 incompatible). Also, use liquidhaskell from the develop branch.

Here is my NixOS config for LH:

• https://github.com/vyorkin/nixos-config/blob/740e30defff098ef5deabcae9038ead4d967575d/cfgs/development/proof-assistants.nix#L14
• https://github.com/vyorkin/nixos-config/blob/740e30defff098ef5deabcae9038ead4d967575d/cfgs/development/haskell/packages/default.nix#L9

My Emacs config for LH:

https://github.com/vyorkin/emacs.d#liquid-types

Links

• the book
• the talk
• with Nix
• with Emacs

Notes

This is a Literal Haskell file! So feel free to play around with the examples!

There is a Liquid Haskell integration package for Cabal and Stack. See the liquidhaskell-cabal-demo for an example project setup. This project is another example of using liquidhaskell-cabal. Refinement Types = Types + Predicates.

Refinement types allows us to decorate types with logical predicates, that contrain the set of values described by the type.

module A1 where

{-@ LIQUID "--no-termination" @-}

Base types, type variables:

b := Int | Bool | ... | a, b, c

Refined base or refined function:

t := { x:b | p } | x:t -> t

Where p is a predicate in decidable logic:

p := e          -- atom
  | e1 == e2    -- equality
  | e1 <  e2    -- ordering
  | (p && p)    -- and
  | (p || p)    -- or
  | (not p)     -- negation

Where e is an expression:

e := x, y, z,...    -- variable
   | 0, 1, 2,...    -- constant
   | (e + e)        -- addition
   | (e - e)        -- subtraction
   | (c * e)        -- linear multiplication
   | (f e1 ... en)  -- uninterpreted function

Ok, lets try something!

We use {-@ ... @-} to add refinement type annotations:

{-@ type Zero = {v:Int | v = 0} @-}
{-@ zero :: Zero @-}
zero :: Int
zero = 0

Predicate Subtyping:

{-@ type Nat   = {v:Int | 0 <= v}        @-}
{-@ type Even  = {v:Int | v mod 2 == 0 } @-}
{-@ type Lt100 = {v:Int | v < 100}       @-}

Natural numbers:

{-@ nats :: [Nat] @-}
nats :: [Int]
nats = [0, 1, 2]

Positive integers:

{-@ type Pos = {v:Int | 1 <= v} @-}

{-@ pos :: [Pos] @-}
pos :: [Int]
pos = [1, 2, 3]

Zero:

{-@ z :: Zero @-}
z :: Int
z = 0

Because z :: Zero <: Nat:

{-@ z' :: Nat @-}
z' :: Int
z' = z

Also:

{-@ z'' :: Even @-}
z'' :: Int
z'' = z

And this one as well:

{-@ z''' :: Lt100 @-}
z''' :: Int
z''' = z

When we erase the refinement we get the standart Haskell types. For example, the Int is equivalent to {v:Int | true} because any standart Haskell type has the trivial refinement true.

Writing specifications and typing dead code.

Contracts (function types):

If the program type checks it means that impossible is never called at runtime.

{-@ impossible :: {v:String | false} -> a @-}
impossible :: String -> a
impossible msg = error msg

{-@ die :: {v:String | false} -> a @-}
die :: String -> a
die msg = impossible msg

For example, LH will accept:

cannonDie :: ()
cannonDie =
  if 1 + 1 == 3
  then die "horrible death"
  else ()

But will reject:

canDie :: ()
canDie =
  if 1 + 1 == 2
  then die "horrible death"
  else ()

Pre-conditions:

The next example won’t typecheck:

{-@ safeDiv :: Int -> Int -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv _ 0 = impossible "divide-by-zero"
safeDiv x n = x `div` n

But this one will:

{-@ type NonZero = {v:Int | v /= 0} @-}
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x n = x `div` n

Verifying user input:

calc :: IO ()
calc = do
  putStrLn "Enter numerator"
  n <- readLn
  putStrLn "Enter denominator"
  d <- readLn
  if d == 0
    then putStrLn "Blya"
    else putStrLn ("Result = " ++ show (safeDiv n d))
  calc

Post-conditons.

We can specify a post-condition as output-type.

For example, lets refine the output type of the abs function to say that it returns only non-negative values:

{-@ abs :: Int -> Nat @-}
abs :: Int -> Int
abs n
  | 0 < n = n
  | otherwise = -n

Because SMT solver has built-in decision procedures for arithmetic.

Ex 3.1:

avg :: [Int] -> Int
avg xs = safeDiv total n
  where
    total = sum xs
    n = size xs

{-@ size :: [a] -> Pos @-}
size :: [a] -> Int
size []     = 1
size (_:xs) = 1 + size xs

Another way to solve the calc exercise is to define a function like:

{-@ nonZero :: Int -> Maybe {v:Int | v /= 0} @-}
nonZero :: Int -> Maybe Int
nonZero 0 = Nothing
nonZero n = Just n

...
case nonZero d of
  Nothing -> putStrLn "Blya"
  Just n  -> ...
...

Or

result :: Int -> Int -> String
result n d
  | isPositive d = "result = " ++ show (n `safeDiv` d)
  | otherwise    = "blya"

Ex 3.2:

{-@ isPositive :: x:_ -> {v:Bool | v <=> x > 0} @-}
isPositive :: (Ord a, Num a) => a -> Bool
isPositive = (> 0)

calc' :: IO ()
calc' = do
  putStrLn "n: "
  n <- readLn
  putStrLn "d: "
  d <- readLn
  putStrLn $ result n d
  calc

Ex 3.3: Assertions

{-@ lAssert :: {v:Bool | v} -> a -> a @-}
lAssert :: Bool -> a -> a
lAssert True x  = x
lAssert False _ = die "assertion failed!"

yes = lAssert (1 + 1 == 2) ()

no  = lAssert (1 + 1 == 3) ()

The next section is about data types.

{-# LANGUAGE ScopedTypeVariables #-}

module A2 where

import A1 (impossible)
import Prelude hiding (length, foldr1, foldr, map, init)

data List a
  = Emp
  | a ::: List a

Measures:

{-@ measure length @-}
length :: List a -> Int
length Emp = 0
length (_ ::: xs) = 1 + length xs

And now LH knows the following properties about our List a:

data List a where
  Emp   :: {v:List a | length v = 0}
  (:::) :: x:a -> xs:List a
        -> {v:List a | length v = 1 + length xs}

Lets make a type alias for a non-empty List:

{-@ type ListNE a = {v:List a | length v > 0} @-}

And now head and tail functions are not partial anymore:

{-@ head :: ListNE a -> a @-}
head (x ::: _) = x

{-@ tail :: ListNE a -> List a @-}
tail (_ ::: xs) = xs

Fold f over list initially using first element:

{-@ foldr1 :: (a -> a -> a) -> ListNE a -> a @-}
foldr1 :: (a -> a -> a) -> List a -> a
foldr1 f (x ::: xs) = foldr f x xs
foldr1 _ _          = impossible "foldr1"

foldr :: (a -> b -> b) -> b -> List a -> b
foldr _ acc Emp = acc
foldr f acc (x ::: xs) = f x (foldr f acc xs)

Another average:

{-@ average' :: ListNE Int -> Int @-}
average' :: List Int -> Int
average' xs = total `div` n
  where
    total = foldr1 (+) xs
    n = length xs

We can refine data types and make illegal states unrepresentable. For example, lets make sure that every year has exactly 12 months.

data Year a = Year (List a)

{-@ data Year a = Year (ListN a 12) @-}

We need a type for lists of a given size.

{-@ type ListN a N = {v: List a | length v == N } @-}

Now, this won’t typecheck:

badYear :: Year Int
badYear = Year (1 ::: Emp)

Mapping:

{-@ map :: (a -> b) -> xs:List a -> ys:ListN b {length xs} @-}
map :: (a -> b) -> List a -> List b
map _ Emp = Emp
map f (x ::: xs) = f x ::: map f xs

Lets write a function to calculate an average temperature of the year:

data Weather = W { temp :: Int, rain :: Int }

tempAverage :: Year Weather -> Int
tempAverage (Year ms) = average' months
  where
    months = map temp ms

Another example:

{-@ init :: (Int -> a) -> n:Nat -> ListN a n @-}
init :: (Int -> a) -> Int -> List a
init _ 0 = Emp
init f n = f n ::: init f (n - 1)

sanDiegoTemp :: Year Int
sanDiegoTemp = Year (init (const 72) 12)

It seems that the problem is in the following condition VV < i , but I don’t understand where this condition comes from. Asked in slack, waiting for reply.

{-@ init' :: (Int -> a) -> n:Nat -> ListN a n @-}
init' :: forall a. (Int -> a) -> Int -> List a
init' f n = go 0
  where
    {-@ go :: i:_ -> ListN a {n - i} @-}
    go :: Int -> List a
    go i | i < n     = f i ::: go (i + 1)
         | otherwise = Emp

sanDiegoTemp' :: Year Int
sanDiegoTemp' = Year (init' (const 72) 12)

Case study: Insertion Sort.

{-# LANGUAGE ScopedTypeVariables #-}
{-@ LIQUID "--no-termination" @-}

module A3 where

import A1 (impossible)
import A2 (List(..), length)
import Data.Set (Set)
import qualified Data.Set as Set

import Prelude hiding (length, foldr1, foldr, map, init)

We need to check 3 things:

• Lists have same size
• Lists have same elements
• Elements in the right order

Lets start with the same size constraint:

{-@ sort :: Ord a => xs:List a -> ListN a {length xs} @-}
sort Emp = Emp
sort (x ::: xs) = insert x (sort xs)

{-@ insert :: Ord a => a -> xs:List a -> ListN a {length xs + 1} @-}
insert :: Ord a => a -> List a -> List a
insert x Emp        = x ::: Emp
insert x (y ::: ys)
  | x <= y          = x ::: (y ::: ys)
  | otherwise       = y ::: insert x ys

Now, lets ensure that a sorted list have the same elements. SMT solvers reason about sets. Hence, we can write set-valued measures.

{-@ measure elems @-}
elems :: Ord a => List a -> Set a
elems Emp = Set.empty
elems (x ::: xs) = addElem x xs

{-@ inline addElem @-}
addElem :: Ord a => a -> List a -> Set a
addElem x xs = Set.union (Set.singleton x) (elems xs)

inline lets us reuse Haskell terms in refinements.

Implication and if-and-only-if operators.

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--higherorder" @-}

module B1 where

==> and <=> are special operators.

==> is the implication operator, equivalent the following Haskell function:

infixr 7 ==>
{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p ==> q)} @-}
(==>) :: Bool -> Bool -> Bool
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

<=> is the if-and-only-if operator, which is equivalent to the Haskell function:

infixr 7 <=>
{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p <=> q)} @-}
(<=>) :: Bool -> Bool -> Bool
False <=> False = True
False <=> True  = False
True  <=> True  = True
True  <=> False = False

An environment is a mapping from variables to their Haskell types. For example, let G be an environment:

x :: Int
y :: Int
z :: Int

Satisfaction:

A predicate is SATISFIABLE in a env G if there exists an assignment in G that makes the predicate evaluate to True.

x + y == z

Validity:

A predicate is VALID in an env G if every assignment make a predicate evalue to True.

x < 10 || x == 10 || x > 10

Verification conditions:

LH checks the program in roughly 2 steps:

1. Combines code and types down to a set of Verification Conditions (VC) which are predicates that are valid only if the program satisfies a given property which are predicates that are valid only if the program satisfies a given property.

2. Quries the SMT solver (e.g. Z3) to determine whether these VC’s are valid.

Examples (Prepositions).

Here TRUE is a refined type for Bool valued expressions that always evaluate to True:

{-@ type TRUE = {v:Bool | v} @-}

Same with FALSE:

{-@ type FALSE = {v:Bool | not v} @-}

Lets see some examples:

Valid:

{-@ ex0 :: TRUE @-}
ex0 :: Bool
ex0 = True

Invalid:

{-@ ex0' :: TRUE @-}
ex0' :: Bool
ex0' = False

Valid:

{-@ ex1 :: Bool -> TRUE @-}
ex1 :: Bool -> Bool
ex1 b = b || not b

Valid as well:

{-@ ex2 :: Bool -> FALSE @-}
ex2 :: Bool -> Bool
ex2 b = b && not b

Examples with ==> operator.

Read p ==> q as: _if p is true then q must also be true.

{-@ ex3 :: Bool -> Bool -> TRUE @-}
ex3 :: Bool -> Bool -> Bool
ex3 a b = (a && b) ==> a

{-@ ex4 :: Bool -> Bool -> TRUE @-}
ex4 :: Bool -> Bool -> Bool
ex4 a b = (a && b) ==> b

Ex 2.1:

{-@ ex3' :: Bool -> Bool -> TRUE @-}
ex3' :: Bool -> Bool -> Bool
ex3' a _ = (a || a) ==> a

Modus ponens:

{-@ ex6 :: Bool -> Bool -> TRUE @-}
ex6 :: Bool -> Bool -> Bool
ex6 a b = (a && (a ==> b)) ==> b

{-@ ex7 :: Bool -> Bool -> TRUE @-}
ex7 :: Bool -> Bool -> Bool
ex7 a b = a ==> (a ==> b) ==> b

De Morgan’s laws:

{-@ exDeMorgan1 :: Bool -> Bool -> TRUE @-}
exDeMorgan1 :: Bool -> Bool -> Bool
exDeMorgan1 a b = not (a || b) <=> (not a && not b)

{-@ exDeMorgan2 :: Bool -> Bool -> TRUE @-}
exDeMorgan2 :: Bool -> Bool -> Bool
exDeMorgan2 a b = not (a && b) <=> (not a || not b)

Examples: Arithmetic

Ok:

{-@ ax0 :: TRUE @-}
ax0 :: Bool
ax0 = 1 + 1 == 2

Not ok:

{-@ ax0' :: TRUE @-}
ax0' :: Bool
ax0' = 1 + 1 == 3

Via the laws of arithmetic, it is equivalent to 0 < 1, which is True independent of the value of x.

{-@ ax1 :: Int -> TRUE @-}
ax1 :: Int -> Bool
ax1 x = x < x + 1

We can combine arithmetic and prepositional operators:

{-@ ax2 :: Int -> TRUE @-}
ax2 :: Int -> Bool
ax2 x = (x < 0) ==> (0 <= 0 - x)

{-@ ax3 :: Int -> Int -> TRUE @-}
ax3 :: Int -> Int -> Bool
ax3 x y = (0 <= x) ==> (0 <= y) ==> (0 <= x + y)

{-@ ax4 :: Int -> Int -> TRUE @-}
ax4 :: Int -> Int -> Bool
ax4 x y = (x == y - 1) ==> (x + 2 == y + 1)

{-@ ax5 :: Int -> Int -> Int -> TRUE @-}
ax5 :: Int -> Int -> Int -> Bool
ax5 x y z =   (x <= 0 && x >= 0)
          ==> (y == x + z)
          ==> (y == z)

Ex 2.3:

{-@ ax6 :: Int -> Int -> TRUE @-}
ax6 :: Int -> Int -> Bool
ax6 x y = False ==> (x <= x + y)

Examples: Uninterpreted function

SMT solver doesn’t know how functions are defined. It only knows the axiom of conguence: any function f returns equal outputs when invoked on equal inputs.

Lets define an uninterpreted function from Int to Int:

{-@ measure f :: Int -> Int @-}

We test the axiom by checking the following predicate:

{-@ congruence :: (Int -> Int) -> Int -> Int -> TRUE @-}
congruence :: (Int -> Int) -> Int -> Int -> Bool
congruence f x y = (x == y) ==> (f x == f y)

I’m too stupid to figure out why this predicate is invalid.

{-@ fx1 :: (Int -> Int) -> Int -> TRUE @-}
fx1 :: (Int -> Int) -> Int -> Bool
fx1 f x =  (x == f (f (f x)))
       ==> (x == f (f (f (f x))))
       ==> (x == f x)

To get a taste:

{-@ measure size @-}
size :: [a] -> Int
size [] = 0
size (_:xs) = 1 + size xs

Now we can verify the following predicate. The SMT doesn’t need to evaluate the size function to proove it.

{-@ fx0 :: [a] -> [a] -> TRUE @-}
fx0 :: Eq a => [a] -> [a] -> Bool
fx0 xs ys = (xs == ys) ==> (size xs == size ys)

But

{-@ fx2 :: a -> [a] -> TRUE @-}
fx2 :: Eq a => a -> [a] -> Bool
fx2 x xs = 0 < size ys
  where
    ys = x : xs

But

{-@ fx2VC :: [a] -> [b] -> TRUE @-}
fx2VC :: [a] -> [b] -> Bool
fx2VC xs ys =   (0 <= size xs)
            ==> (size ys == 1 + size xs)
            ==> (0 < size ys)

Polymorphism.

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination"      @-}
{-@ LIQUID "--scrape-used-imports" @-}

module B2 where

import A1 (abs)
import Prelude hiding (length, abs)
import Data.Vector hiding (head, foldl')
import Data.List (foldl')

Array bounds verification:

twoLangs :: Vector String
twoLangs = fromList ["haskell", "javascript"]

We get a runtime exception with this:

eeks :: [String]
eeks = [ok, yup, nono]
  where
    ok   = twoLangs ! 0
    yup  = twoLangs ! 1
    nono = twoLangs ! 3

We can write specifications for imported modules – either in place or (better), in .spec files, which could be reused across multiple modules.

We can write specifications for external modules inside special include directories.

For example, for Data.Vector we’ll need include/Data/Vector.spec with the following contents:

-- | Define the size
measure vlen :: Vector a -> Int

-- | Compute the size
assume length :: x:Vector a -> {v:Int | v = vlen x}

-- | Lookup at an index
assume (!) :: x:Vector a -> {v:Nat | v < vlen x} -> a

To use this specification:

liquid -i include/ foo.hs

LiquidHaskell ships with specifications for Prelude, Data.List nad Data.Vector which it includes by default.

Measures - define properties of Haskell data values that are used for specification and verification.

Assumes - specify types describing semantics of functions that we cannot verify because we don’t have the code for them.

Alises - abbreviations for commonly occurring types, e.g.:

{-@ type VectorN a N = {v:Vector a | vlen v == N} @-}

{-@ twoLangs :: VectorN String 2 @-}

or

{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}

then we can

(!) :: x:Vector a -> Btwn 0 (vlen x) -> a

Lets try something.

What if vec had no elements? A formal verifier doesn’t make off by one errors:

head :: Vector a -> a
head vec = vec ! 0

Lets fix that:

{-@ type NEVector a = {v:Vector a | 0 < vlen v} @-}

We’ve specified NEVector is a non-empty vector, so now our new head' verifies:

{-@ head' :: NEVector a -> a @-}
head' :: Vector a -> a
head' vec = vec ! 0

Ex 4.1 (Vector head)

head'' :: Vector a -> Maybe a
head'' vec = vec !? 0

Ex 4.2 (Unsafe lookup)

{-@ type GTVector a N = {v:Vector a | N < vlen v} @-}

{-@ unsafeLookup :: ix:Nat -> GTVector a ix -> a @-}
unsafeLookup :: Int -> Vector a -> a
unsafeLookup ix vec = vec ! ix

Ex 4.3 (Safe lookup)

{-@ safeLookup :: Vector a -> Int -> Maybe a @-}
safeLookup :: Vector a -> Int -> Maybe a
safeLookup x i
  | ok = Just (x ! i)
  | otherwise = Nothing
  where
    ok = 0 < i && i < length x

Inference.

LH verifies the vectorSum function below (safety of vec ! i) because LH is able to automatically infer:

go :: Int -> {v:Int | 0 <= v && v <= sz} -> Int

vectorSum :: Vector Int -> Int
vectorSum vec = go 0 0
  where
    go :: Int -> Int -> Int
    go acc i
      | i < sz    = go (acc + (vec ! i)) (i + 1)
      | otherwise = acc
    sz = length vec

Ex 4.6 (Why v <= sz and not v < sz?)

Because when i < sz we call go acc (i + 1) and i + 1 <= sz in this case.

Ex 4.5 (Absolute sum)

{-@ absoluteSum :: Vector Int -> Nat @-}
absoluteSum :: Vector Int -> Int
absoluteSum vec = go 0 0
  where
    go acc i
      | i < length vec = go (acc + abs (vec ! i)) (i + 1)
      | otherwise      = acc

High-order functions.

{-@ loop :: lo:Nat -> hi:{Nat | lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a @-}
loop :: Int -> Int -> a -> (Int -> a -> a) -> a
loop lo hi base f = go base lo
 where
   go acc i
     | i < hi    = go (f i acc) (i + 1)
     | otherwise = acc

LH finds that:

loop
  :: lo:Nat
  -> hi:{Nat | lo <= hi}
  -> a
  -> (Btwn lo hi -> a -> a)
  -> a

TODO: Have no idea what’s wrong here

vectorSum' :: Vector Int -> Int
vectorSum' vec = loop 0 n 0 body
  where
    body i acc = acc + (vec ! i)
    n = length vec

Ex 4.7 (High-order loops)

{-@ absoluteSum' :: Vector Int -> Nat @-}
absoluteSum' :: Vector Int -> Int
absoluteSum' vec = loop 0 (length vec) 0 body
  where
    {-@ body :: Int -> _ -> Nat @-}
    body :: Int -> Int -> Int
    body i acc = acc + abs (vec ! i)

Ex 4.8

{-@
dotProduct
  :: x:Vector Int
  -> {y:Vector Int | vlen x == vlen y}
  -> Int
@-}
dotProduct :: Vector Int -> Vector Int -> Int
dotProduct x y = loop 0 (length x) 0 body
  where
    body :: Int -> Int -> Int
    body i acc = acc + (x ! i) * (y ! i)

Refinements and Polymorphism.

Lets make an alias for a sparse vectors and write a function to compute sparse product.

{-@ type SparseN a N = [(Btwn 0 N, a)] @-}

Since we know that all indexes are with the bounds of the source array the following function verifies:

{-@ sparseProduct :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct :: Num a => Vector a -> [(Int, a)] -> a
sparseProduct x y = go 0 y
  where
    go acc [] = acc
    go acc ((i, v):ys) = go (acc + (x ! i) * v) ys

Another way to represend the sparse product is using fold. For example:

foldl' :: (a -> b -> a) -> a -> [b] -> a

GHC infers that:

foldl' :: (a -> (Int, a)) -> a -> [(Int, a)] -> a

LH infers that:

b :: (Btwn 0 (vlen x), a)

{-@ sparseProduct' :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct' :: Num a => Vector a -> [(Int, a)] -> a
sparseProduct' x y = foldl' body 0 y
  where
    body sum (i, v) = sum + (x ! i) * v

Refined Datatypes.

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--no-total" @-}

module B3 where

import Prelude hiding (abs, length, min)
import Data.Vector hiding (singleton, foldl', foldr, fromList, (++), all)
import Data.Maybe (fromJust)

Sparse vectors revisited.

data Sparse a = SP
  { spDim :: Int
  , spElems :: [(Int, a)]
  }

• spDim should be positive number
• every index in spElems should be 0 <= i < spDim

{-@
data Sparse a = SP
  { spDim :: Nat
  , spElems :: [(Btwn 0 spDim, a)]
  }
@-}

{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}

Now SP works like a smart constructor!

okSP :: Sparse String
okSP = SP 5 [ (0, "cat")
            , (3, "dog")
            ]

badSP :: Sparse String
badSP = SP 5 [ (0, "cat")
             , (6, "dog")
             ]

Field measures.

Lets write an alias for sparse vectors of size N.

{-@ type SparseN a N = {v:Sparse a | spDim v == N} @-}

Now we can write our dotProd function like this:

{-@ dotProd :: x:Vector Int -> SparseN Int (vlen x) -> Int @-}
dotProd :: Vector Int -> Sparse Int -> Int
dotProd x (SP _ y) = go 0 y
  where
    go acc []          = acc
    go acc ((i, v):ys) = go (acc + (x ! i) * v) ys

And fold-based implementation:

Ex 5.1 (Sanitization)

{-@ fromList :: n:Nat -> [(Btwn 0 n, _)] -> Maybe (SparseN _ n) @-}
fromList :: Int -> [(Int, a)] -> Maybe (Sparse a)
fromList dim elems
  | all (< dim) (fst <$> elems) = Just $ SP dim elems
  | otherwise = Nothing

{-@ test1 :: SparseN String 3 @-}
test1 :: Sparse String
test1 = fromJust $ fromList 3 [(0, "cat"), (2, "mouse")]

Ex 5.2 (Addition)

{-@ plus :: SparseN a 3 -> SparseN a 3 -> SparseN a 3 @-}
plus :: Sparse a -> Sparse a -> Sparse a
plus v1 v2 = SP (spDim v1) (spElems v1 ++ spElems v2)

But I think the goal is to make a general function that can work for any dimension.

{-@ test2 :: SparseN Int 3 @-}
test2 :: Sparse Int
test2 = plus vec1 vec2
  where
    vec1 = SP 3 [(0, 12), (2, 9)]
    vec2 = SP 3 [(0, 8),  (1, 100)]

Ordered lists.

data IncList a
  = Emp
  | (:<) { hd :: a, tl :: IncList a }

infixr 9 :<

We can specify that the elements are in order by refining every element in tl to be greater than hd:

{-@
data IncList a =
    Emp
  | (:<) { hd :: a, tl :: IncList {v:a | hd <= v} }
@-}

okList :: IncList Int
okList = 1 :< 2 :< 3 :< Emp

badList :: IncList Int
badList = 2 :< 1 :< 3 :< Emp

Insertion sort.

insertSort :: Ord a => [a] -> IncList a
insertSort []     = Emp
insertSort (x:xs) = insert x (insertSort xs)

insert :: Ord a => a -> IncList a -> IncList a
insert y Emp = y :< Emp
insert y (x :< xs)
  | y <= x = y :< x :< xs
  | otherwise = x :< insert y xs

Ex 5.3

insertSort' :: Ord a => [a] -> IncList a
insertSort' = foldr insert Emp

Merge sort.

split :: [a] -> ([a], [a])
split (x:y:zs) =
  let (xs, ys) = split zs
  in (x:xs, y:ys)
split xs = (xs, [])

Sometimes I get errors like http://ix.io/1N99 which really confuse me.

This is a “totality” error — it means your function/case expression is missing a case and so LH cannot prove that case is dead code and hence gives that error (e.g. the head or tail function which is not defined on []). This feature was added after the tutorial and the LH authors made totality on by default. It can be switched off with {-@ LIQUID “—no-total” @-}. Or of course it is better to implement the missing case.

We should however add to the error the missing patterns…

One way to get them right now is load the file in ghci with the -fwarn-incomplete-patterns flag.

merge :: Ord a => IncList a -> IncList a -> IncList a
merge Emp ys = ys
merge xs Emp = xs
merge (x :< xs) (y :< ys)
  | x <= y    = x :< merge xs (y :< ys)
  | otherwise = y :< merge (x :< xs) ys

mergeSort :: Ord a => [a] -> IncList a
mergeSort []  = Emp
mergeSort [x] = x :< Emp
mergeSort xs  = merge (mergeSort ys) (mergeSort zs)
  where
    (ys, zs) = split xs

Ex 5.4 (QuickSort)

quickSort :: Ord a => [a] -> IncList a
quickSort [] = Emp
quickSort (x:xs) = append x lessers greaters
  where
    lessers  = quickSort [y | y <- xs, y < x]
    greaters = quickSort [z | z <- xs, z >= x]

We need to ensure that append has a valid specification:

{-@
append
  :: x:a
  -> IncList {v:a | v < x}
  -> IncList {v:a | v >= x}
  -> IncList a
@-}
append :: Ord a => a -> IncList a -> IncList a -> IncList a
append z Emp ys       = z :< ys
append z (x :< xs) ys = x :< (append z xs ys)

Ordered trees.

data BST a
  = Leaf
  | Node { root  :: a
         , left  :: BST a
         , right :: BST a
         }

okBST :: BST Int
okBST =
  Node 6
    ( Node 2
      (Node 1 Leaf Leaf)
      (Node 4 Leaf Leaf)
    )
    ( Node 9
      (Node 7 Leaf Leaf)
      Leaf
    )

okBST' :: BST Int
okBST' =
  Node 5
    ( Node 3
      (Node 1 Leaf Leaf)
      (Node 4 Leaf Leaf)
    )
    ( Node 8
      (Node 7 Leaf Leaf)
      Leaf
    )

{-@
data BST a =
    Leaf
  | Node { root  :: a
         , left  :: BSTL a root
         , right :: BSTR a root
         }
@-}

{-@ type BSTL a X = BST {v:a | v < X} @-}
{-@ type BSTR a X = BST {v:a | v > X} @-}

badBST :: BST Int
badBST =
  Node 66
    ( Node 4
      (Node 1 Leaf Leaf)
      (Node 69 Leaf Leaf)
    )
    ( Node 99
      (Node 77 Leaf Leaf)
      Leaf
    )

Ex 5.5 (Duplicates)

The answer is no. Each value is either > than other or <. But N > N is impossible and N < N doesn’t make any sense too.

Membership.

mem :: Ord a => a -> BST a -> Bool
mem _ Leaf = False
mem k (Node k' l r)
  | k == k'   = True
  | k <  k'   = mem k l
  | otherwise = mem k r

Singleton.

one :: a -> BST a
one x = Node x Leaf Leaf

Insertion.

add :: Ord a => a -> BST a -> BST a
add k' Leaf = one k'
add k' t@(Node k l r)
  | k' < k    = Node k (add k' l) r
  | k  < k'   = Node k l (add k' r)
  | otherwise = t

Minimum.

data MinPair a = MP
  { mEl :: a
  , mRest :: BST a
  }

{-@
data MinPair a = MP
  { mEl :: a
  , mRest :: BSTR a mEl
  }
@-}

Looks like the delMin example from page 55 needs an additional restriction (that BST a isn’t just a Leaf) + maybe something else.

As I can see right now, nothing prevents BST a from being a Leaf So delMin Leaf = die "impossible" branch is possible and verification fails for me with error http://ix.io/1O9r.

{-@ delMin :: BST a -> MinPair a @-}
delMin :: Ord a => BST a -> MinPair a
delMin (Node k Leaf r) = MP k r
delMin (Node k l r) =
  let MP k' l' = delMin l
  in MP k' (Node k l' r)
delMin Leaf = die "impossible"

Ex 5.6 (Delete)

Depends on delMin.

Ex 5.7. (Safely deleting minimum)

Depends on delMin.

Ex 5.8 (BST sort).

TODO!

Lifting functions to Measures.

{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--short-names"    @-}

module B4 where
import Prelude hiding (head, tail, null, sum, foldl1)
import qualified Prelude as P
import A1 (safeDiv, die)

notEmpty :: [a] -> Bool
notEmpty []    = False
notEmpty (_:_) = True

Measure is a total Haskell function:

• single equation per data constructor
• guaranteed to terminate

measure tells LiquidHaskell to lift a function into the refinement logic:

{-@ measure notEmpty @-}

Now we can use the notEmpty predicate to describe non-empty lists:

{-@ type NEList a = { v:[a] | notEmpty v } @-}

size returns a non-zero value if the input list is not-empty. We capture this condition with an implication in the output refinement.

{-@ size :: xs:[a] -> { v:Nat | notEmpty xs => v > 0 } @-}
size :: [a] -> Int
size []     = 0
size (_:xs) = 1 + size xs

{-@ average :: NEList Int -> Int @-}
average :: [Int] -> Int
average xs = total `safeDiv` elems
  where
    total = P.sum xs
    elems = size xs

Ex 6.1 (Average, Maybe)

average' :: [Int] -> Maybe Int
average' xs
  | elems > 0 = Just $ (P.sum xs) `safeDiv` elems
  | otherwise = Nothing
  where
    elems = size xs

Ex 6.2 (Debugging specificatins)

These two examples below are rejected because the xs in (_:xs) could be empty:

{-@ size1 :: xs:NEList a -> Pos @-}
size1 :: [a] -> Int
size1 [] = 0
size1 (_:xs) = 1 + size1 xs

{-@ size2 :: xs:[a] -> { v:Int | notEmpty xs => v > 0 } @-}
size2 :: [a] -> Int
size2 [] = 0
size2 (_:xs) = 1 + size2 xs

Since we have NEList we can use it to type the head and tail functions:

{-@ head :: NEList a -> a @-}
head :: [a] -> a
head (x:_) = x
head []    = die "fear not"

{-@ tail :: NEList a -> [a] @-}
tail :: [a] -> [a]
tail (_:xs) = xs
tail []    = die "fear not"

LH uses the precondition to deduce that the second equations are dead code.

Ex 6.3 (Safe head)

safeHead :: [a] -> Maybe a
safeHead xs
  | null xs   = Nothing
  | otherwise = Just $ head xs

{-@ null :: xs:[a] -> {v:Bool | v <=> not notEmpty xs } @-}
null :: [a] -> Bool
null []    = True
null (_:_) = False

Groups.

Lets write a function that chunks sequences into non-empty groups of equal elements:

{-@ groupEq :: Eq a => [a] -> [NEList a] @-}
groupEq :: Ord a => [a] -> [[a]]
groupEq []     = []
groupEq (x:xs) = (x:ys) : groupEq zs
  where
    (ys, zs) = span (x ==) xs

Eliminate stuttering:

eliminateStutter :: String -> String
eliminateStutter = map head . groupEq

λ> eliminateStutter "ssstringssss liiiiiike thisss"
"strings like this"

{-@ foldl1 :: (a -> a -> a) -> NEList a -> a @-}
foldl1 :: (a -> a -> a) -> [a] -> a
foldl1 f (x:xs) = foldl f x xs
foldl1 _ [] = die "foldl1"

Sum of a non-empty list of Num a:

{-@ sum :: Num a => NEList a -> a @-}
sum :: Num a => [a] -> a
sum [] = die "sum"
sum xs = foldl1 (+) xs

sumOk :: Int
sumOk = sum [1, 2, 3]

sumBad :: Int
sumBad = sum []

sumBad' :: Int
sumBad' = sum [1..3]

Ex 6.4 (Weighted average)

{-@ wtAverage :: NEList (Pos, Pos) -> Int @-}
wtAverage :: [(Int, Int)] -> Int
wtAverage wxs = totElems `safeDiv` totWeight
  where
    elems     = map' (uncurry (*)) wxs
    weights   = map' fst wxs
    totElems  = sum' elems
    totWeight = sum' weights

{-@ sum' :: NEList Pos -> Pos @-}
sum' :: [Int] -> Int
sum' [] = die "sum"
sum' xs = foldl1 (+) xs

{-@ map' :: (a -> b) -> NEList a -> NEList b @-}
map' :: (a -> b) -> [a] -> [b]
map' _ []     = die "impossible"
map' f (x:[]) = [f x]
map' f (x:xs) = (f x) : map' f xs

Ex 6.5 (Mitchell’s risers)

{-@ risers :: Ord a => NEList a -> NEList [a] @-}
risers :: (Ord a) => [a] -> [[a]]
risers []  = die "impossible"
risers [x] = [[x]]
risers (x:y:etc)
  | x <= y    = (x:s):ss
  | otherwise = [x]:(s:ss)
  where
    (s, ss) = safeSplit $ risers (y:etc)

{-@ safeSplit :: NEList a -> (a, [a]) @-}
safeSplit :: [a] -> (a, [a])
safeSplit (x:xs) = (x, xs)
safeSplit _ = die "go forth and die"

Numeric measures.

Wholemeal programming.

{-# LANGUAGE ScopedTypeVariables #-}
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--short-names"    @-}

module B5 where

import Prelude hiding (map, reverse, zipWith, zip)
import qualified Prelude as P
import A1 (die)

We’ll need some stuff from the previous chapters:

{-@ type TRUE = {v:Bool | v} @-}

We can use measures to specify dimensions and create a dimension-aware API for lists which can be used to implement wholemeal dimension-safe APIs.

data Vector a = V
  { vDim :: Int
  , vEls :: [a]
  }
  deriving (Eq)

data Matrix a = M
  { mRow :: Int
  , mCol :: Int
  , mEls :: Vector (Vector a)
  }
  deriving (Eq)

dotProd :: Num a => Vector a -> Vector a -> a
dotProd vx vy = sum (prod xs ys)
  where
    prod = P.zipWith (*)
    xs   = vEls vx
    ys   = vEls vy

matProd :: Num a => Matrix a -> Matrix a -> Matrix a
matProd (M rx _ xs) (M _ cy ys) = M rx cy els
  where
    els = for xs $ \xi ->
            for ys $ \yj ->
              dotProd xi yj

for :: Vector a -> (a -> b) -> Vector b
for (V n xs) f = V n (f <$> xs)

We need a way to represent the dimensions. Measures are ideal for this task, so lets write a measure to describe the length of a list:

{-@ measure size @-}
size :: [a] -> Int
size []     = 0
size (_:rs) = 1 + size rs

Just a reminder: a measure is an inductively defined function with a single equative per data-constructor.

As with refined data definitions, the measures are translated into smth like this:

data [a] where
  []  :: { v:[a] | size v = 0 }
  (:) :: a -> xs:[a] -> { v:[a] | size v = 1 + size xs }

Multiple measures may be defined for the same data type, for example:

{-@ measure notEmpty @-}
notEmpty :: [a] -> Bool
notEmpty []    = False
notEmpty (_:_) = True

Different measures can be composed by conjoining the refinements. For example, lets compose size and notEmpty measures:

data [a] where
  []  :: { v:[a] | not (notEmpty v) size v = 0 }
  (:) :: a
      -> xs:[a]
      -> { v:[a] | notEmpty v && size v = 1 + size xs }

Measure’s decouples property from structure, which enabled the use of the same structure for many different purposes.

To make signatures symmetric:

type List a = [a]

{-@ type ListN a N = { v:List a | size v == N } @-}
{-@ type ListX a X = ListN a { size X } @-}

Ex 7.1 (Map)

{-@ map :: (a -> b) -> xs:List a -> ListX b xs @-}
map :: (a -> b) -> List a -> List b
map f (x:xs) = f x : map f xs
map _ [] = []

{-@ prop_map :: forall a. xs:List a -> TRUE @-}
prop_map :: forall a. List a -> Bool
prop_map xs = size ys == size xs
  where
    {-@ ys :: ListX a xs @-}
    ys :: List a
    ys = map id xs

Ex 7.2 (Reverse)

{-@ reverse :: xs:List a -> ListX a xs @-}
reverse :: List a -> List a
reverse = go []
  where
    {-@ go :: ys:List a -> xs:List a -> ListN a {size xs + size ys} @-}
    go :: List a -> List a -> List a
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

{-@ invariant {v:[a] | 0 <= size v} @-}

{-@ zipWith :: (a -> b -> c) -> xs:List a -> ListX b xs -> ListX c xs @-}
zipWith :: (a -> b -> c) -> List a -> List b -> List c
zipWith f (a:as) (b:bs) = f a b : zipWith f as bs
zipWith _ [] []         = []
zipWith _ _ _           = die "impossible"

Unsafe zip:

{-@ zip :: as:[a] -> bs:[b] -> { v:[(a, b)] | Tinier v as bs } @-}
zip :: [a] -> [b] -> [(a, b)]
zip (a:as) (b:bs) = (a, b) : zip as bs
zip [] _ = []
zip _ [] = []

{-@ predicate Tinier V X Y = Min (size V) (size X) (size Y) @-}
{-@ predicate Min V X Y = (if X < Y then V == X else V == Y) @-}

Ex 7.3 (Zip unless empty)

TODO: How to draw an owl

{-@
zipOrNull
  :: xs:List a
  -> ys:List b
   -> ListX (a, b) xs @-}
zipOrNull :: [a] -> [b] -> [(a, b)]
zipOrNull [] _  = []
zipOrNull _ []  = []
zipOrNull xs ys = zipWith (,) xs ys

{-@ test1 :: { v:_ | size v = 2 } @-}
test1 :: [(Int, Bool)]
test1 = zipOrNull [0, 1] [True, False]