We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies.

We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies. Less

We use cookies and other tracking technologies... More

# Login or registerto boost this post!

Show some love to the author of this blog by giving their post some rocket fuel ðŸš€.

# Login or register to start working on this issue!

Engineers who find a new job through JavaScript Works average a 15% increase in salary ðŸš€

# Become a Better Haskeller by Learning About Inductive Types

Marko DimjaÅ¡eviÄ‡ 15 April, 2019 | 2 min read

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.

Check out the Author's Github here

(C) Marko DimjaÅ¡eviÄ‡ 2019, licensed under the Creative Commons Attribution-ShareAlike 4.0 International license

Originally published on dimjasevic.net

Marko DimjaÅ¡eviÄ‡
A computer scientist with interests in correct software via advanced static type systems and functional programming
Idris
Agda

## Related Issues

WorksHub / client
• Started
• 0
• 18
• Intermediate
• Clojure
• \$150
viebel / klipse-clj
viebel / klipse-clj
• Started
• 0
• 1
• Intermediate
• Clojure
viebel / klipse
• Open
• 0
• 0
• Intermediate
• Clojure
viebel / klipse
• 1
• 0
• Intermediate
• Clojure
viebel / klipse
• Started
• 0
• 2
• Intermediate
• Clojure
• \$80
viebel / klipse
• Open
• 0
• 0
• Clojure
• \$80
viebel / klipse
• Started
• 0
• 2
• Clojure
• \$180
viebel / klipse
• Started
• 0
• 1
• Intermediate
• Clojure
viebel / klipse
• 1
• 1