using types to prevent conflicting port numbers in a list

Question

Propellor represents a system it deploys as [Property], and for the sake of simplification, let's say that data Property = Property (Set Port) SatisfyProperty

So, there might be a apacheInstalled Property, which uses ports 80 and 443, and also a torBridge property, which uses port 443. It does not make sense for a system to have both properties at the same time, since they use the same port 443.

I wonder if there's a feasible way for the type checker to prevent a system from being assigned both? Then port conflicts could be caught at build time. I suppose that type level Ints would be the first step, but I haven't a clue as to the second one..

Answer 1

This is pretty tricky, but entirely possible with the an up to date ghc version (the latest haskell platform will work). There isn't many examples about this (as it is all pretty new), so I hope this helps you.

You are right that using type level naturals will work. You will need two modules - one to define the constructs and to provide a safe interface, and another to define the actual services.

This is the code in use:

{-# LANGUAGE TypeOperators, PolyKinds, RankNTypes #-}
{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, UndecidableInstances #-}
module DefinedServices where
import ServiceTypes
import Control.Monad

apacheInstalled :: Service '[443] ServiceDetails
apacheInstalled = makeService "apache" $ putStrLn "Apache service"

torBridge :: Service [80,443] ServiceDetails
torBridge = makeService "tor" $ putStrLn "Tor service"

httpService :: Service [80, 8080] ServiceDetails
httpService = makeService "http" $ putStrLn "Http service"

serviceList1 :: [ServiceDetails]
serviceList1 = getServices $
               noServices `addService` httpService `addService` apacheInstalled

-- serviceList2 :: [ServiceDetails]
-- serviceList2 = getServices $
--                noServices `addService` apacheInstalled `addService` torBridge


main = startServices serviceList1

Note how the ports for each service are defined in the type. serviceList1 makes use of the httpService and the apacheInstalled service. This compiles, as their ports don't conflict. serviceList2 is commented out, and causes this compile error if uncommented:

DefinedServices.hs:22:56:
    Couldn't match type 'False with 'True
    Expected type: 'True
      Actual type: ServiceTypes.UniquePorts '[443, 80, 443]
    In the second argument of `($)', namely
      `noServices `addService` apacheInstalled `addService` torBridge'
    In the expression:
      getServices
      $ noServices `addService` apacheInstalled `addService` torBridge
    In an equation for `serviceList2':
        serviceList2
          = getServices
            $ noServices `addService` apacheInstalled `addService` torBridge
Failed, modules loaded: ServiceTypes.

This describes pretty well the problem: UniquePorts ends up being false as 443 is used twice.

---

So here is how it is done in ServiceTypes.hs:

{-# LANGUAGE TypeOperators, PolyKinds, RankNTypes #-}
{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, UndecidableInstances #-}
module ServiceTypes (
  makeService, noServices, addService, Service, ServiceDetails(..) 
  , getServices, startServices) where
import GHC.TypeLits
import Control.Monad
import Data.Type.Equality
import Data.Type.Bool

We need a whole bunch of language extensions to get this to work. Also, the safe interface is defined.

First, a type level function is needed to check if a list is unique. This leverages the type family operators in Data.Type.Equality and Data.Type.Bool. Note that the following code is only ever executed by the typechecker.

type family UniquePorts (list1 :: [Nat]) :: Bool
type instance UniquePorts '[] = True
type instance UniquePorts (a ': '[]) = True
type instance UniquePorts (a ': b ': rest) = Not (a == b) && UniquePorts (a ': rest) && UniquePorts (b ': rest)

It is just a recursive definition of unique.

Next, as we will use multiple services at once, there will need to be a way to combine two lists into one:

type family Concat (list1 :: [a]) (list2 :: [a]) :: [a]
type instance Concat '[] list2 = list2
type instance Concat (a ': rest) list2 = a ': Concat rest list2

That is all the type level functions we require!

Next, I will define a Service type, that wraps another type with the ports needed:

data Service (ports :: [Nat]) service = Service service

Next, for the actual details of a single service. You should customize this to what you need:

data ServiceDetails = ServiceDetails {
  serviceName :: String
  , runService :: IO ()
  }

I also added a helper function to wrap a service in a Service type with defined ports:

makeService :: String -> IO () -> Service ports ServiceDetails
makeService name action = Service $ ServiceDetails name action

Now finally for the multiple services lists. `noServices just defines an empty list of services, which obviously uses no ports:

noServices :: Service '[] [ServiceDetails]
noServices = Service []

addService is where it all comes together:

addService :: (finalPorts ~ Concat ports newPorts, UniquePorts finalPorts ~ True)
  => Service ports [ServiceDetails]
  -> Service newPorts ServiceDetails
  -> Service finalPorts [ServiceDetails]
addService (Service serviceList) (Service newService) = 
  Service $ (newService : serviceList)

finalPorts ~ Concat ports newPorts just makes finalPorts the combination of the ports in the list of services and the new service. UniquePorts finalPorts ~ True ensures the final ports don't contain any duplicate ports. The rest of the function is completely trivial.

getServices unwraps the [ServiceDetails] from a Service ports [ServiceDetails]. As the Service constructor isn't made public, the only way to create a Service ports [ServiceDetails] type is through the noServices and addService functions, which are guaranteed to be safe.

getServices :: Service ports [ServiceDetails] -> [ServiceDetails]
getServices (Service details) = details

Finally a testing function to run the services:

startServices :: [ServiceDetails] -> IO ()
startServices services = forM_ services $ \service -> do
  putStrLn $ "Starting service " ++ (serviceName service)
  runService service
  putStrLn "------"

---

The possibilities for this new functionality are nearly endless, and is a huge improvement over previous ghc versions (it was still possible, but much more difficult). This code is pretty simple once you get your head around using values in types.