Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Samples of Verification by LiquidHaskell
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment