Type-Driven Development

Kris Nuttycombe (@nuttycom) - January, 2018

Resources

TDD?

Test-Driven Development

  • Write down a failing test case for a specific feature. This test will be incomplete and wrong.
  • Write code until that test passes (solving the wrong problem).
  • Iterate

Type-Driven Development

  • Write down the problem as some types - both data and operations. Avoid implementation concerns.
  • Look at your type.
    • Does it represent all the states you need?
      • Write a proof.
    • Does it imply some states you don't want in your program?
      • Introduce types to eliminate those states (recurse.)

Chicken Sexing

-- anecdote via @garybernhardt

DAGs for Task Management

A simple task type

A simple task type

data Task = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [Task]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: Int
  }

Task Cost

Task Cost

data Task = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [Task]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: Int
  }
taskCost :: Task -> Int

Task Cost

data Task = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [Task]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: Int
  }
taskCost :: Task -> Int
taskCost task = 
  estimate task + sum (fmap taskCost (dependsOn task))
taskCost :: Task -> Int
taskCost task = length $ dependsOn task

Prune the space of possible implementations

data Task n = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [Task n]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n
  }
taskCost :: (Monoid n) => Task n -> n
taskCost task = 
  estimate task <> foldMap taskCost (dependsOn task)
taskCost :: (Monoid n) => Task -> n
taskCost = const mempty

Get rid of every operation you don't need

data Task n = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [Task n]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n
  }
taskCost :: (Semigroup n) => Task n -> n
taskCost task = 
  sconcat (estimate task :| fmap taskCost (dependsOn task))

Storage

Storage

data Task n = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [Task n]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n 
  } 
newtype TaskStore n = TaskStore { unTaskStore :: Map TaskRef (TaskF n) }

findTask :: TaskStore n 
         -> TaskRef 
         -> Maybe (Task n)

Storage

data Task n = Task 
  { title :: Text
  , description :: Text
  , dependsOn :: [TaskRef]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n 
  } 
newtype TaskStore n = TaskStore { unTaskStore :: Map TaskRef (TaskF n) }

findTask :: TaskStore n 
         -> TaskRef 
         -> Maybe (Task n)

Storage

data TaskF n a = TaskF 
  { title :: Text
  , description :: Text
  , dependsOn :: [a]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n 
  } 
newtype TaskStore n a = TaskStore { unTaskStore :: Map a (TaskF n a) }

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)

Storage

data TaskF n a = TaskF 
  { title :: Text
  , description :: Text
  , dependsOn :: [a]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n 
  } 
newtype TaskStore n a = TaskStore { unTaskStore :: Map a (TaskF n a) }

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
findTaskF = flip lookup . unTaskStore

Oops.

/Users/nuttycom/personal/lc_winter-2018-tdd/src/Task2.hs:29:44: error:
    • Couldn't match type ‘a’ with ‘TaskF n a0’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          taskCost :: forall n a. Semigroup n => TaskF n a -> n
        at src/Task2.hs:27:1-43
      Expected type: [TaskF n a0]
        Actual type: [a]
    • In the second argument of ‘fmap’, namely ‘(dependsOn task)’
      In the second argument of ‘(:|)’, namely
        ‘fmap taskCost (dependsOn task)’
      In the first argument of ‘sconcat’, namely
        ‘(estimate task :| fmap taskCost (dependsOn task))’
    • Relevant bindings include
        task :: TaskF n a (bound at src/Task2.hs:28:10)
        taskCost :: TaskF n a -> n (bound at src/Task2.hs:28:1)
   |
29 |   sconcat (estimate task :| fmap taskCost (dependsOn task))
   |                                            ^^^^^^^^^^^^^^

Oops.

Fixing taskCost

taskCost :: (Semigroup n) => Task n -> n
taskCost task = 
  sconcat (estimate task :| fmap taskCost (dependsOn task))
findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
taskCost :: (Semigroup n, Ord a) 
         => TaskStore n a 
         -> TaskF n a 
         -> n

Fixing taskCost

taskCost :: (Semigroup n) => Task n -> n
taskCost task = 
  sconcat (estimate task :| fmap taskCost (dependsOn task))
findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
taskCost :: (Semigroup n, Ord a) 
         => TaskStore n a 
         -> TaskF n a 
         -> n
taskCost s task = 
  let deps = catMaybes . fmap (findTaskF s) $ dependsOn task
  in  sconcat (estimate task :| fmap (taskCost s) deps)

Fixing taskCost

data TaskF n a = TaskF
  { title :: Text
  , description :: Text
  , dependsOn :: [a]
  , state :: TaskState
  , tags :: Set TaskTag
  , estimate :: n
  } deriving Functor
-- from Data.Functor.Foldable 
newtype Fix (f :: * -> *) = Fix { unfix :: f (Fix f) }
type Task n = Fix (TaskF n)
findTask :: (Ord a) 
         => TaskStore n a 
         -> a 
         -> Either (NonEmpty a) (Task n)

Fixing taskCost

type Task n = Fix (TaskF n)

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)



findTask :: (Ord a) 
         => TaskStore n a 
         -> a 
         -> Either (NonEmpty a) (Task n)
findTask store ref =

Fixing taskCost

type Task n = Fix (TaskF n)

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
import Data.Semigroup (:|)


findTask :: (Ord a) 
         => TaskStore n a 
         -> a 
         -> Either (NonEmpty a) (Task n)
findTask s ref = do
  root  <- maybe (Left $ ref :| []) Right (findTaskF store ref)

Fixing taskCost

type Task n = Fix (TaskF n)

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
import Data.Semigroup (:|)
import Data.Validation as V

findTask :: (Ord a) 
         => TaskStore n a 
         -> a 
         -> Either (NonEmpty a) (Task n)
findTask s ref = do
  root  <- maybe (Left $ ref :| []) Right (findTaskF s ref)
  root' <- V.toEither $ traverse (V.fromEither . findTask s) root

Fixing taskCost

type Task n = Fix (TaskF n)

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
import Data.Semigroup (:|)
import Data.Validation as V

findTask :: (Ord a) 
         => TaskStore n a 
         -> a 
         -> Either (NonEmpty a) (Task n)
findTask s ref = do
  root  <- maybe (Left $ ref :| []) Right (findTaskF s ref)
  root' <- V.toEither $ traverse (V.fromEither . findTask s) root
  pure $ embed root

Fixing taskCost

type Task n = Fix (TaskF n)

findTaskF :: (Ord a) 
          => TaskStore n a 
          -> a 
          -> Maybe (TaskF n a)
taskCost :: (Semigroup n) => Task n -> n
taskCost = cata (\t -> sconcat (estimate t :| dependsOn t))

Graphing!

Graphing!

graph :: (Ord a, Show a) => TaskStore n a -> a -> DotGraph a
graph s a = 
  let nodes = a : transitiveDeps s a
      edges' (a, tf) = (a,,()) <$> dependsOn tf
      edges = edges' =<< (\a' -> fmap (a',) . F.toList $ findTaskF s a') =<< nodes
  in  graphElemsToDot (graphParams s) ((,()) <$> nodes) (L.nub edges)

graphParams :: (Ord a) => TaskStore n a -> GraphvizParams a al el () al
graphParams s = nonClusteredParams 
  { isDirected = True
  , globalAttributes = 
      [ GraphAttrs [RankDir FromLeft] 
      , NodeAttrs  [shape DoubleCircle]
      ]
  , fmtNode = \(a, _) -> 
      let attrs t = toLabel (title t) : taskStyle (taskState t) 
      in  maybe [] attrs $ findTaskF s a 
  }

taskStyle :: TaskState -> [Attribute]
taskStyle (Created Task) = []
taskStyle (Created Bug) = [style filled, fillColor Tomato] 
taskStyle Completed = [style filled, fillColor LawnGreen]

Graphing!

Graphing!

To Be Embellished

The Vampire Policy

"Bug fixing strategy: forbid yourself to fix the bug. Instead, render the bug impossible by construction." --Paul Phillips

Know the size of your state space

How many different values can this function possibly return?

f :: () -> Bool

Know the size of your state space

How many different values can this function possibly return?

f :: () -> Bool -- 2 possible values
g :: () -> Int32

Know the size of your state space

How many different values can this function possibly return?

f :: () -> Bool -- 2 possible values
g :: () -> Int32 -- 2^32 possible values
k :: () -> Either Bool Int32

Know the size of your state space

How many different values can this function possibly return?

f :: () -> Bool -- 2 possible values
g :: () -> Int32 -- 2^32 possible values
k :: () -> Either Bool Int32 -- 2 + 2^32 possible values
h :: () -> (Bool, Int32)

Know the size of your state space

How many different values can this function possibly return?

f :: () -> Bool -- 2 possible values
g :: () -> Int32 -- 2^32 possible values
k :: () -> Either Bool Int32 -- 2 + 2^32 possible values
h :: () -> (Bool, Int32) -- 2 * 2^32 = 2^33 possible values
h :: () -> Either Int32 Int32 -- 2^32 + 2^32 = 2^33 possible values
k :: () -> Text

Know the size of your state space

How many different values can this function possibly return?

f :: () -> Bool -- 2 possible values
g :: () -> Int32 -- 2^32 possible values
k :: () -> Either Bool Int32 -- 2 + 2^32 possible values
h :: () -> (Bool, Int32) -- 2 * 2^32 = 2^33 possible values
h :: () -> Either Int32 Int32 -- 2^32 + 2^32 = 2^33 possible values
k :: () -> Text -- 😬😖😩😷

Use smart constructors (aka parsers) wherever errors can occur

insertTaskF :: (Ord a)
           => TaskStore n a
           -> a 
           -> TaskF n a 
           -> Either (NonEmpty a) (TaskStore n a)

Final principles to code by

Extra bonus quiz!

type T a b = forall c. (a -> b -> c) -> c

type E a b = forall c. (a -> c) -> (b -> c) -> c

How many different values can these functions possibly return?

f :: () -> T Bool Int32

g :: () -> E Bool Int32

Extra bonus quiz!

type T a b = forall c. (a -> b -> c) -> c

type E a b = forall c. (a -> c) -> (b -> c) -> c

How many different values can these functions possibly return?

f :: () -> T Bool Int32 -- 2 * 2^32 = 2^33 possible values!

g :: () -> E Bool Int32 -- 2 + 2^32 possible values!