Using types to force correctness

Question

Let's say that we have a store management application. It has Customers and can chargeFee(). It should do so only for active Customers however.

A common way I've seen this done (Java/pseudocode) is something like this:

class Customer {
    String name
    StatusEnum status  // 1=active, 2=inactive
}    

// and this is how the customers are charged
for (c:Customer.listByStatus(StatusEnum.1)) {
    c.chargeFee()
}

This is OK, but it doesn't stop someone from charging a fee from an inactive Customer. Even if chargeFee() checks the status of the Customer, that's a runtime error/event.

So, keeping the whole 'make illegal states unrepresentable' thing in mind, how would one approach design of this application (in Haskell for example)? I want a compile error if someone tries to charge an inactive customer.

---

I was thinking something like this, but I still doesn't allow me to restrict chargeFee so that an inactive Customer cannot be charged.

data CustomerDetails = CustomerDetails { name :: String }
data Customer a = Active a | Inactive a

chargeFee :: Active a -> Int -- this doesn't work, do I need DataKinds?

Answer 1

You can accomplish such a thing with phantom types:

module Customer 
   (CustomerKind(..), Customer, {- note: MkCustomer is not exported -}       
    makeCustomer, activate, chargeFee) where

data CustomerKind = Active | Inactive 
data Customer (x :: CustomerKind) = MkCustomer String 

mkCustomer :: String -> Customer Inactive 
mkCustomer = MkCustomer 

-- perhaps `IO (Customer Active)' or something else
activate :: Customer Inactive -> Maybe (Customer Active) 
activate = ...

chargeFee :: Customer Active -> Int
chargeFee = ... 

Here activate will somehow ensure that the given customer can be made active (and do so), producing said active customer. But trying to call chargeFee (mkCustomer ...) is a type error.

Note that DataKinds are not strictly required - the following is equivalent:

data Active 
data Inactive 
-- everything else unchanged 

The same can be accomplished without phantom types, by simply declaring two types - ActiveCustomer and InactiveCustomer - but the phantom types approach allows you to write functions which don't care about the type of customer:

customerName :: Customer a -> String 
customerName (MkCustomer a) = ...

Answer 2

A basic way is to use a separate type

data ActiveCustomer   = AC String -- etc.
data InactiveCustomer = IC String -- etc.
data Customer = Active ActiveCustomer | Inactive InactiveCustomer

-- only works on active
chargeFee :: ActiveCustomer -> IO ()
chargeFee (AC n) = putStrLn ("charged: " ++ n)

-- works on anyone
getName :: Customer -> String
getName (Active  (AC n)) = n
getName (Inctive (IC n)) = n

This can also be done, more or less, in OOP languages: just use a different class for active and inactive customers, possibly inheriting from a common Customer interface / superclass.

With algebraic types you get the benefits of the closed-world assumption, namely that there are no other subtypes of Customer, but often one can live without that.

---

A more advanced way is to use a GADT. DataKinds is optional but is nicer, IMHO. (Warning: untested)

{-# LANGUAGE GADTs, DataKinds #-}

data CustomerType = Active | Inactive
data Customer (t :: CustomerType) where
   AC :: String -> Customer Active
   IC :: String -> Customer Inactive

-- only works on active
chargeFee :: Customer Active -> IO ()
chargeFee (AC n) = putStrLn ("charged: " ++ n)

-- works on anyone
getName :: Customer any -> String
getName (AC n) = n
getName (IC n) = n

Alternatively, factor out the tag with a singleton:

data CustomerType = Active | Inactive
data CustomerTypeSing (t :: CustomerType) where
   AC :: CustomerTypeSing Active
   IC :: CustomerTypeSing Active
data Customer (t :: CustomerType) where
   C :: CustomerTypeSing t -> String -> Customer t

-- only works on active
chargeFee :: Customer Active -> IO ()
chargeFee (C _ n) = putStrLn ("charged: " ++ n)

-- works on anyone
getName :: Customer any -> String
getName (C _ n) = n

-- how to build a new customer
makeActive :: String -> Customer Active 
makeActive n = C AC n