TLDR; Small types in type driven development facilitates composability much like small objects do in OO. By small types I mean few constructors and little data in each.
One of my first experiences in Idris was to try to implement a FizzBuzz where the types would be so strong that they'd ensure the code could only be correctly implemented.
FizzBuzz is a game where the input is a number between 1 and 100. The output is a string, "Fizz" if the number is divisible by 3. "Buzz" if the number is divisible by 5. "FizzBuzz" if it is both divisible by 3 and 5 and just the number otherwise. eg counting from 1
1, 2, fizz, 4, buzz, fizz, 7, 8, fizz, buzz, ...
My first implemention enforces the correctness by taking as arguments proofs that the given number is either divisible by 3 or a proof that it is not divisible. That way can call the constructor Fizz if and only if you can provide proof of division by 3 and a proof of non division by 5.
So just by defining a type FizzBuzz and the signatures of the constructors of this type we have no possibility of making a mistake in the implementation. Nice! Here's are the types and signature of methods.
IF you're curious about the implementation it's here
Besides being a major challenge, for me, in mastering dependent types and understanding that types can act as proofs, it actually worked out quite OK. Certainly it does not allow for incorrect code, so it was a successful experience. Sure it is a bit of verbose and contains a bit of pseudo-duplication.
But not extensible
Now there's an extension to FizzBuzz, namely Bang. Bang is the word for every multiple of 7, for instance given the number 21 we should return FizzBang. Now without Bang there are 4 possible results, Fizz, Buzz, FizzBuzz and the number. Now here's where things become interesting because with Bang there are 8, so the problem of verbosity and pseudo-duplication gets a lot worse. Clearly the first solution isn't very extensible
A better solution
A different approach is to decompose the type FizzBuzz into smaller orthogonal types. Lets consider the type Fizz (either a IsFizz or a Not IsFizz), the type Buzz, then FizzBuzz can be modeled as a tuple (pair) of Fizz an Buzz (the full code).
If we add the functionality of Bang then all we have to do is create a new type Bang, and a new composed type a 3-tuple of Fizz, Buzz and Bang. We don't have to break the existing type FizzBuzz nor the former function, we could possibly even keep the former method, a good example of the open-closed principle. Open-closed-principle with dependently typed code!
Possibly we'd fear that by making the types less closed we'd be able to code an incorrect solution to fizzbuzz. But that's still not possible.
Learnings
Keeping types small in the sense that they contain little data (few arguments) and have few constructors, favours reuse through composition. It might seem obvious in hindsight, but I discovered this much in the same way that I discovered the use of small objects in OO.
Some people say that strongly typed languages like Idris doesn't allow for extension, that they'd be closed by design. What I learned from this experience is that while that certainly applies to a type and functions on existing types, we can still compose types in new ways. Given of course that our types are small enough.
