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

You could always make chargeFee return a Maybe or Either for illegal actions:

chargeFee :: Customer a -> Maybe Int
chargeFee (Inactive _) = Nothing
chargeFee (Active cust) = ...

Answer 3

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

Answer 4

All that's required is to tag the type with the active status. I see no need for separate constructors. It's easy to do so like so:

{-# LANGUAGE GADTs #-}

data Active = Active
data Inactive = Inactive

data Customer a where
  Customer :: String -> Int -> Customer a

(p.s. I've added an Int to your data type to represent credit, so you can actually charge the customer in some way.)

So Customer Active represents and "active" customer, and likewise Customer Inactive represents an "inactive" customer.

We can then "create" customers like so:

create :: String -> Int -> Customer a
create = Customer

createByStatus :: a -> String -> Int -> Customer a
createByStatus _ = Customer

Creating convenience methods is easy:

createActive :: String -> Int -> Customer Active
createActive = create
createInactive :: String -> Int -> Customer Inactive
createInactive = create

Note that using create directly you can create silly types like Customer Int. You've got a few options to stop this,

1. Only expose the convenience methods to your users
2. Put a constraint on a in create type classes.

I'll go through option 2 later on.

Now we can write some methods to work on our type:

getName :: Customer a -> String
getName (Customer name _) = name

getCredit :: Customer a -> Int
getCredit (Customer _ credit) = credit

chargeCustomer :: Customer Active -> Int -> Customer Active
chargeCustomer (Customer name credit) charge = Customer name (credit - charge)

Note that chargeCustomer only works on active customers. You'l get a type error otherwise.

Now I'm going to write a utility function, castCustomer.

castCustomer :: Customer a -> Customer b
castCustomer (Customer name credit) = Customer name credit

What castCustomer does is just change any sort of customer into any sort of customer. Think of this as an unsafe cast in C, you shouldn't expose this to your users. But it's useful to write your other functions:

setActiveStatus :: statusToCheck -> Customer currentStatus -> Customer statusToCheck
setActiveStatus _ = castCustomer

So you can do setActiveStatus Inactive customer and you'll get back customer but inactive. It just uses castCustomer which works for all casts, but setActiveStatus's own type restricts castCustomer appropriately.

And there's also these simpler utility functions:

Of course one can now write convenience functions:

setActive :: (LegalStatus a) => Customer a -> Customer Active
setActive = castCustomer

setInactive :: (LegalStatus a) => Customer a -> Customer Inactive
setInactive = castCustomer

Finally, one might want a function like this:

getByStatus :: b -> Customer a -> Maybe (Customer b)

where we pass a status and a customer, and get that customer returned if they match the status, but otherwise returns Nothing.

We're going to need different implementations depending on the types, so we're going to need a class.

We could write a class like class GetByStatus a b but the problem is that any functions which use this class will have to have an ugly GetByStatus a b in their type signatures constraint clause.

So we're going to make a simpler class:

class LegalStatus a where ...

Which is going to have two instances:

instance LegalStatus Active where ...
instance LegalStatus Inactive where ...

Here's the definitions of the LegalStatus class:

class LegalStatus a where 
  get :: (LegalStatus b) => Customer b -> Maybe (Customer a)
  getActive :: Customer a -> Maybe (Customer Active)
  getInactive :: Customer a -> Maybe (Customer Inactive)

This may look confusing, but lets have a look at the instances:

instance LegalStatus Active where
  get = getActive
  getActive = Just . castCustomer
  getInactive _ = Nothing

instance LegalStatus Inactive where
  get = getInactive
  getActive _ = Nothing
  getInactive = Just . castCustomer 

What we're doing here is an object orientated technique called https://en.wikipedia.org/wiki/Double_dispatch. This means we don't complicate our signatures. We can now out function like:

getByStatus :: (LegalStatus a, LegalStatus b) => a -> Customer b -> Maybe (Customer a)
getByStatus _ = get

Using these functions and catMaybe, it's relatively easy to write functions that say, take a list of customers and return only the active ones:

getAll :: (LegalStatus a, LegalStatus b) => [Customer a] -> [Customer b]
getAll = catMaybes . map get

getAllByStatus :: (LegalStatus a, LegalStatus b) => a -> [Customer b] -> [Customer a]
getAllByStatus _ = getAll

getAllActive :: (LegalStatus a) => [Customer a] -> [Customer Active]
getAllActive = getAll

getAllInactive :: (LegalStatus a) => [Customer a] -> [Customer Inactive]
getAllInactive = getAll

It's worth pointing out how magic getAll is (and indeed, many other similar functions in Haskell). Do getAll list and if you put in into a list of active customers, you'll get only the active customers in the list, and similarly, if you put it into a list of inactive customers, you'll only get inactive customers in the list.

I'll illstrate this through the following function, which splits a list of customers who's status is unknown into a list of active customers and a list of inactive customers:

splitCustomers :: (LegalStatus a) => [Customer a] -> ([Customer Active], [Customer Inactive])
splitCustomers l = (getAll l, getAll l)

Looking at the implementation of splitCustomers, it looks like the first and second elements of the pair are the same. Indeed they look exactly the same. But they're not, they've got different types, and as a result end up calling different instances and can get totally different results.

There's one other thing to close up if you really want to. You'll probably want to expose the class LegalStatus, as users might want to use it as a constraint in their type signatures, but that means they can write instances of LegalStatus. Like

instance LegalStatus Int where ...

They'd be silly to do this but you can stop them if you like. The simplest approach is this:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}

type family RestrictLegalStatus a where
  RestrictLegalStatus Active = ()
  RestrictLegalStatus Inactive = ()

type IsLegalStatus a = (RestrictLegalStatus a ~ ())

class (IsLegalStatus a) => LegalStatus a where ...

Any attempt to make a new instance will now fail the IsLegalStatus constraint and fail.

This is probably overengineered at this point, and you won't need all this, but I've included it to show some points about type-inference:

So for your reference, here's all the code attached below:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}

module Main where

import Data.Maybe (catMaybes)

main = return ()

data Active = Active
data Inactive = Inactive

type family RestrictLegalStatus a where
  RestrictLegalStatus Active = ()
  RestrictLegalStatus Inactive = ()

type IsLegalStatus a = (RestrictLegalStatus a ~ ())

data Customer a where
  Customer :: String -> Int -> Customer a

class (IsLegalStatus a) => LegalStatus a where 
  get :: (LegalStatus b) => Customer b -> Maybe (Customer a)
  getActive :: Customer a -> Maybe (Customer Active)
  getInactive :: Customer a -> Maybe (Customer Inactive)

instance LegalStatus Active where
  get = getActive
  getActive = Just . castCustomer
  getInactive _ = Nothing

instance LegalStatus Inactive where
  get = getInactive
  getActive _ = Nothing
  getInactive = Just . castCustomer

getByStatus :: (LegalStatus a, LegalStatus b) => a -> Customer b -> Maybe (Customer a)
getByStatus _ = get

create :: String -> Int -> Customer a
create = Customer

createByStatus :: a -> String -> Int -> Customer a
createByStatus _ = Customer

createActive :: String -> Int -> Customer Active
createActive = Customer

createInactive :: String -> Int -> Customer Inactive
createInactive = Customer

getName :: Customer a -> String
getName (Customer name _) = name

getCredit :: Customer a -> Int
getCredit (Customer _ credit) = credit

chargeCustomer :: Customer Active -> Int -> Customer Active
chargeCustomer (Customer name credit) charge = Customer name (credit - charge)

castCustomer :: Customer a -> Customer b
castCustomer (Customer name credit) = Customer name credit

setActiveStatus :: (LegalStatus statusToCheck, LegalStatus currentStatus) => statusToCheck -> Customer currentStatus -> Customer statusToCheck
setActiveStatus _ = castCustomer

setActive :: (LegalStatus a) => Customer a -> Customer Active
setActive = castCustomer

setInactive :: (LegalStatus a) => Customer a -> Customer Inactive
setInactive = castCustomer

getAll :: (LegalStatus a, LegalStatus b) => [Customer a] -> [Customer b]
getAll = catMaybes . map get

getAllByStatus :: (LegalStatus a, LegalStatus b) => a -> [Customer b] -> [Customer a]
getAllByStatus _ = getAll

getAllActive :: (LegalStatus a) => [Customer a] -> [Customer Active]
getAllActive = getAll

getAllInactive :: (LegalStatus a) => [Customer a] -> [Customer Inactive]
getAllInactive = getAll

splitCustomers :: (LegalStatus a) => [Customer a] -> ([Customer Active], [Customer Inactive])
splitCustomers l = (getAll l, getAll l)

Edit:

Others have pointed out to restrict the statuses using DataKinds. Admittedly this is probably a cleaner approach than my "constraint on the class" approach. Note you have to change a few of the functions, because the parameter to the class is no longer an ordinary type but a kind, and only ordinary types can be parameters to functions, you have to wrap raw status functions in a Proxy constructor.

Note with the DataKind approach you can no longer call getByStatus Active... because Active is no longer a value, you need to do:

getByStatus (Proxy :: Proxy Active) ...

but feel free to define:

active :: Proxy Active
active = Proxy

so you can then call:

getByStatus active

The full code is below.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

module Main where

import Data.Maybe (catMaybes)
import Data.Proxy (Proxy)

main = return ()

data LegalStatusKind = Active | Inactive

data Customer (a :: LegalStatusKind) where
  Customer :: String -> Int -> Customer a

class LegalStatus (a :: LegalStatusKind) where 
  get :: (LegalStatus b) => Customer b -> Maybe (Customer a)
  getActive :: Customer a -> Maybe (Customer Active)
  getInactive :: Customer a -> Maybe (Customer Inactive)

instance LegalStatus Active where
  get = getActive
  getActive = Just . castCustomer
  getInactive _ = Nothing

instance LegalStatus Inactive where
  get = getInactive
  getActive _ = Nothing
  getInactive = Just . castCustomer

getByStatus :: (LegalStatus a, LegalStatus b) => Proxy a -> Customer b -> Maybe (Customer a)
getByStatus _ = get

create :: String -> Int -> Customer a
create = Customer

createByStatus :: Proxy a -> String -> Int -> Customer a
createByStatus _ = Customer

createActive :: String -> Int -> Customer Active
createActive = Customer

createInactive :: String -> Int -> Customer Inactive
createInactive = Customer

getName :: Customer a -> String
getName (Customer name _) = name

getCredit :: Customer a -> Int
getCredit (Customer _ credit) = credit

chargeCustomer :: Customer Active -> Int -> Customer Active
chargeCustomer (Customer name credit) charge = Customer name (credit - charge)

castCustomer :: Customer a -> Customer b
castCustomer (Customer name credit) = Customer name credit

setActiveStatus :: (LegalStatus statusToCheck, LegalStatus currentStatus) => Proxy statusToCheck -> Customer currentStatus -> Customer statusToCheck
setActiveStatus _ = castCustomer

setActive :: (LegalStatus a) => Customer a -> Customer Active
setActive = castCustomer

setInactive :: (LegalStatus a) => Customer a -> Customer Inactive
setInactive = castCustomer

getAll :: (LegalStatus a, LegalStatus b) => [Customer a] -> [Customer b]
getAll = catMaybes . map get

getAllByStatus :: (LegalStatus a, LegalStatus b) => Proxy a -> [Customer b] -> [Customer a]
getAllByStatus _ = getAll

getAllActive :: (LegalStatus a) => [Customer a] -> [Customer Active]
getAllActive = getAll

getAllInactive :: (LegalStatus a) => [Customer a] -> [Customer Inactive]
getAllInactive = getAll

splitCustomers :: (LegalStatus a) => [Customer a] -> ([Customer Active], [Customer Inactive])
splitCustomers l = (getAll l, getAll l)