Blog/Safely encoding flows

From foldr
Jump to: navigation, search

Information icon.svg This is a blog post. If you want to comment on this blog post, please mention me on Twitter @rightfold. I will set up proper comment functionality later.

WordPress blue logo.svg This blog post was migrated from my old WordPress blog. If you want to link to this blog post, please link to this page instead of to the WordPress blog.

Flow charts can be treated as sets of allowed flows. For example, the flow “A → C → B” is not allowed by the following flow chart.


If we want to describe this flow chart in our program, we can do this as follows:

data Node = A | B | C | D | E
type Flow = [Node]

While this works, it can encode flows not allowed by our flow chart. An example of a flow that is not allowed is [A, C, B], yet this type checks. It would be nice if we could use the type system to constrain the data type to only flows that are allowed by the flow chart. One way to do this is by listing all allows flows:

data Flow = ABDE | ACDE

While this works, it becomes a mess for flow charts with many branches, which is not atypical. By using a generalized abstract data type (GADTs) and datatype promotion (data kinds), we can construct a more scalable encoding, which composes flows into larger flows:

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

data Node = A | B | C | D | E

data Flow :: Node -> Node -> * where
  AB :: Flow A B
  AC :: Flow A C
  BD :: Flow B D
  CD :: Flow C D
  DE :: Flow D E
  (>~>) :: Flow a b -> Flow b c -> Flow a c

Now there is no way to construct the erroneous flow “A → C → B”, since there is no CB constructor. The two allowed flows are encoded as AB >~> BD >~> DE and AC >~> CD >~> DE. This encoding does, however, allow for incomplete flows. To fix that, you can add a begin and end node, and a simple type alias that enforces the flow to be complete:

data Node =  | Begin | End

data Flow :: Node -> Node -> * where
  BeginA :: Flow Begin A
  EEnd :: Flow E End

type FullFlow = Flow Begin End