LiquidHaskell Company and Groups

Main.hs

module Main where

import Data.Set (Set)
import qualified Data.Set as S

main :: IO ()
main
  = print
  . removePerson (Person 1)
  . addPerson (Person 1)
  $ emptyCompany

newtype Person = Person { personId :: Int }
  deriving (Show, Eq, Ord)

{-@
emptyCompany :: { c : Company | people c == S.empty }
@-}
emptyCompany :: Company
emptyCompany = Company S.empty S.empty

{-@
data Company = Company
    { people :: Set Person
    , groups :: Set (Set { p : Person | S.member p people })
    }
@-}
data Company
  = Company
    { people :: Set Person
    , groups :: Set (Set Person)
    } deriving (Show)

memberOfCompany :: Person -> Company -> Bool
memberOfCompany person company = person `S.member` (people company)

{-@ addPerson
  :: person : Person
  -> company : { c : Company | not S.member person (people c) }
  -> { c' : Company | people c' == S.union (S.singleton person) (people company) }
@-}
addPerson :: Person -> Company -> Company
addPerson person company = company { people = S.insert person (people company) }

removePerson :: Person -> Company -> Company
removePerson person company = company
  { people = S.delete person (people company)
  , groups = S.map (S.delete person) (groups company)
  }