average :: Foldable t => t Int -> Int
average ns = sum ns `div` length ns
                    

checkProtocol :: [IP] -> Bool
checkProtocol = isIPv4 . head
                    

getUserName :: Home -> Text
getUserName homeDir = parts !! 1
  where
    parts = splitOn "/" homeDir
                    

$ stack install liquidhaskell
                    

$ apt-get install z3
                    

$ stack exec -- liquid App.hs 
                    

module Liquid.Spec.Port where

{-@ type NotRootPort =
           {p:Int | 1024 <= p
                    && p <= 65535}
@-}
                    

import Liquid.Spec.Port ()

{-@ localPort :: NotRootPort @-}
localPort :: Int
localPort = 3010
                    

import Liquid.Spec.Port ()

{-@ localPort :: NotRootPort @-}
localPort :: Int
localPort = 22
                    

module Liquid.Spec.Number where

{-@ type NotZero = {n:Int | n != 0}
@-}
                    

{-@ okDiv :: Int -> NotZero -> Int @-}
okDiv :: Int -> Int -> Int
okDiv = div
                    

main :: IO ()
main = (readLn :: IO Int)
  >>= print . okDiv 512
                    

main :: IO ()
main = (readLn :: IO Int)
  >>= divideIt
 where
  divideIt 0 = putStrLn "Go away!"
  divideIt v = print $ 512 `okDiv` v
                    

servicePorts :: [Port]
servicePorts =
  [3000, 3001, 3010, 3011, 3012, 3013
   3013, 3014, 3020, 3030, 3040, 3050]
                    

module Liquid.Spec.List where

import Data.Set

{-@ type ListUnique a =
           {v:[a] | NoDups v}
@-}
                    

{-@ predicate NoDups L =
                Set_emp (dups L)
@-}
                    

{-@ measure dups :: [a] -> (Set a)
    dups ([])   = {v | Set_emp v}
    dups (x:xs) = {v | v =
      if (Set_mem x (listElts xs))
      then (Set_cup (Set_sng x) (dups xs))
      else (dups xs)}
@-}
                    

{-@ servicePorts ::
    ListUnique NotRootPort @-}
servicePorts :: [Port]
servicePorts =
  [3000, 3001, 3010, 3011, 3012, 3013
   3013, 3014, 3020, 3030, 3040, 3050]
                    

main :: IO ()
main = print . f $ "O RLY?"
                    

[1 of 1] Compiling Main ...

~/src/Main.hs:8:16: Not in scope: ‘f’
                    

 src/Main.hs:8:16: Error: GHC Error
  
   8 | main = print . f $ "O RLY?"
                      ^
                        
       Not in scope: ‘f’
                    

$ liquid --totality App.hs 
                    

data Currency = USD | RUB | GBP | EUR

display :: Currency -> Text
display USD = "United States Dollar"
display RUB = "Russia Ruble"
display GBP = "United Kingdom Pound"
                    

import Liquid.Spec.Port ()

{-@ localPort :: NotRootPort @-}
localPort :: Int
localPort = 22