Samples of Verification by LiquidHaskell

Sample.hs

module Sample where

import Language.Haskell.Liquid.Prelude ( liquidError )

{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead []      = liquidError "empty list"
safeHead (x : _) = x

-- badUsage = safeHead [] -- => Liquid Type Mismatch

{-@ safeDiv :: Int -> { d:Int | d /= 0 } -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv n 0 = liquidError "zero divide"
safeDiv n d = n `div` d

{-@ safeAbs :: Int -> { n:Int | n >= 0} @-}
safeAbs :: Int -> Int
safeAbs n
    | n >= 0    = n
    | otherwise = 0 - n

{-@ safeIncr :: n:Int -> { v:Int | v > n } @-}
safeIncr :: Int -> Int
safeIncr n = n + 1

{-@ safeDouble :: n:{ v:Int | v > 2 } -> { w:Int | w > n + 2 } @-}
safeDouble :: Int -> Int
safeDouble n = 2 * n

{-@ vecZipWith :: (a -> b -> c) ->
    xs:[a] -> { ys:[b] | len ys = len xs } -> { zs:[c] | len zs = len xs } @-}
vecZipWith _ []       []       = []
vecZipWith f (x : xs) (y : ys) = f x y : vecZipWith f xs ys
vecZipWith _ _        _        = liquidError "dimension mismatch"

{-@ vecSum :: (Num a) =>
    xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-}
vecSum xs ys = vecZipWith (+) xs ys

-- badSum = vecSum [1, 2, 3] [4, 5] -- => Liquid Type Mismatch

{-@ vecSubtr :: (Num a) =>
   xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-}
vecSubtr xs ys = vecZipWith (-) xs ys

{-@ dot :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> a @-}
dot xs ys = sum $ vecZipWith (*) xs ys

{-@ vecMap :: (a -> b) -> xs:[a] -> { ys:[b] | len ys = len xs } @-}
vecMap f []       = []
vecMap f (x : xs) = f x : vecMap f xs

{-@  scalar :: (Num a) => a -> xs:[a] -> { ys:[a] | len ys = len xs } @-}
scalar c xs = vecMap (c *) xs