A simple Agda-implementation.

Companies101.agda

module Companies101 where

open import Data.Bool
open import Data.Vec
open import Data.Nat
open import Data.String

Name = String
Salary = ℕ
Address = String

data Employee : Set where
  employee : (n : Name) -> (a : Address) -> (s : Salary) -> Employee

-- Note the use of sized vectors here. It allows us to enforce invariants
-- later on.
data Department : Set where
  dept : {n k : ℕ}
         -> (name : Name) -> (mgr : Employee)
         -> (emps : Vec Employee n)
         -> (subDepts : Vec Department k)
         -> Department

data Company : Set where
  company : {k : ℕ}
          -> (n : Name)
          -> (depts : Vec Department k) -> Company


totalEmployee : Employee -> ℕ
totalEmployee (employee n a s) = s

-- This mutual definition is needed to make Agdas termination checker happy
mutual
  sumDepts : {k : ℕ} -> Vec Department k -> ℕ
  sumDepts [] = 0
  sumDepts (x ∷ xs) = totalDepartment x + sumDepts xs

  totalDepartment : Department -> ℕ
  totalDepartment (dept n mgr emps subDepts) = mgrS + empS + sumDepts subDepts
    where mgrS = totalEmployee mgr
          empS = sum (map totalEmployee emps)

totalCompany : Company -> ℕ
totalCompany (company n depts) = sumDepts depts

cutEmployee : Employee -> Employee
cutEmployee (employee n a s) = employee n a ⌊ s /2⌋

-- Also a termination check hint for Agda
mutual
  cutDepts : {k : ℕ} -> Vec Department k -> Vec Department k
  cutDepts [] = []
  cutDepts (x ∷ xs) = cutDepartment x ∷ cutDepts xs

  cutDepartment : Department -> Department
  cutDepartment (dept name mgr emps subDepts) =
    dept name (cutEmployee mgr) (map cutEmployee emps) (cutDepts subDepts)

cutCompany : Company -> Company
cutCompany (company n depts) = company n (cutDepts depts)