Become a Better Haskeller by Learning About Inductive Types

In the functional programming world, we rely on languages with type systems that help us write, extend and maintain our software. These type systems, such as the one in Haskell, are based on solid type theory. While we usually and easily see the benefits of having a static type system on simple types such as integers, we might fail to see the benefits of applying the same principles to user-defined data types.

Haskell is a programming language with a decent type system. If one knows how to use it, the type system can be of immense help to them. One useful idea with types is to make states that make no sense in the domain we’re modeling irrepresentable in a type. In other words, the idea is to not be able to construct a domain-meaningless term in the type. If our domain model informs us that we should use integers to represent the state our system can be in, this implies not being able to put a term 3.14 into an integer type. The same principle applies to user-defined data types: relieve yourself of ways of putting a term into your state type that makes no sense in the domain. One way to achieve this in Haskell is via smart constructors. Below is a sketch of how to achieve this. Then we simply have to apply this idea from the lowest levels to the highest levels of abstraction. There are multiple benefits of such an approach, just to name a few: 1) aiding abstraction and separating unrelated concerns, 2) much easier testing, 3) improved maintainability.

Just like we perform checks when reading from the external world, e.g., with the readMaybe function that has a signature readMaybe :: Read a => String -> Maybe a:

import Text.Read

main :: IO ()
main = do
  xStr <- getLine
  let xMaybe = readMaybe xStr :: Maybe Word
  case xMaybe of
    Nothing -> putStrLn (xStr ++ " is not a positive integer!")
    Just x  -> putStrLn (show (x + 5))

so should we apply the same principle when constructing terms at higher levels of abstraction. For example, if we have a type Palindrome for palindrome integers and a type PalPrime for integers that are both palindrome and prime, our conversion of an input string to a prime palindrome integer would look like this:

f1 :: String     -> Maybe Word
f2 :: Word       -> Maybe Palindrome
f3 :: Palindrome -> Maybe PalPrime
 
readValidate :: String -> Maybe PalPrime
readValidate s = do
  i   <- f1 s
  pal <- f2 i
  f3 pal

By using coproducts (the Maybe types) we communicate the possibility of failure when climbing the ladder of abstraction. This is instead of not checking if validation passes at each abstraction level, but possibly only at the end:

f1' :: String     ->       Word
f2' :: Word       ->       Palindrome
f3' :: Palindrome -> Maybe PalPrime

readValidate' :: String -> Maybe PalPrime
readValidate' = f3' . f2' . f1'

Such an approach misses to throw away meaningless states early on, which inevitably complicates the whole program afterwards.

I encourage the reader to study the first half of a new book Programming Language Foundations in Agda by Wadler and Kokke. The book is freely available online. It comes with code in Agda, a dependently typed functional programming language. If you are interested in learning how to make meaningless states irrepresentable in your types in Haskell (or for that matter, in any other language), read the first half of the book where inductive types are lingua franca. Inductive types naturally make a meaningless state irrepresentable. Furthermore, inductive types teach you how to think inductively, i.e., how to have an initial state and make state transitions from one state into another. If your language of choice does not have dependent types like Agda does (dependent types are used throughout the book), I believe smart constructors are the most viable alternative you can use to substitute them; a sketch of smart constructors is given above.