Last time we created a custom FizzBuzz data type and implemented the Show interface.
The problem with our previous code was that the compiler wasn’t enforcing any correctness, so today we’re going to do that.
Types are Proofs
Types are proofs, being able to create an instance of a type, tells you something about the value which has that type. This holds true even for basic type systems, a value with an Integer type tells you it isn’t a string. But Idris has a much more powerful type system.
Lots of languages have a concept of Generics, functions and data structures which are defined for arbitrary types. Idris takes this one step further and allows generics over runtime values.
data Divisibleby3 : Nat -> Type where
Three: Divisibleby3 3
ThreeMultiple: Divisibleby3 x -> Divisibleby3 (3+x)Divisibleby3 is a data structure which is generic over a natural number. It has two constructors, ways of making an instance of the type, Three and ThreeMultiple.
The Three constructor says that an instance of Divisibleby3 can be constructed from the value 3. i.e. three is divisible by 3.
The ThreeMultiple says, if you already have an instance of Divisibleby3 for a number x, then you can construct an instance of Divisibleby3 for the value (x+3). i.e. every number divisible by 3, is 3 more than another number divisible by 3.
You may have noticed that this sounds alot like recursion. Three is the base case and ThreeMultiple effectively ‘calls’ Divisibleby3 recursively. This is a very common pattern for constructing proofs.
Let’s construct a few instances of Divisibleby3
divBy3: Divisibleby3 3
divBy3 = Three
divBy6: Divisibleby3 6
divBy6 = ThreeMultiple Three
divBy9: Divisibleby3 9
divBy9 = ThreeMultiple (ThreeMultiple Three)divBy3 is straighforward, just a single use of the Three constructor. divBy6 starts with an instance of Three then passes that to ThreeMultiple to make a Divisibleby3 6 instance, and divBy9 continues the pattern.
It could get pretty tedious to write out divBy360, luckily Idris can do some of the leg work for you with its automated proof search feature.
If you can construct a instance of Divisibleby3 for a value you know it is divisible by 3. Instances of Divisibleby3 cannot be made for values not divisible by three using the two available constructors. As an example, let’s try to construct an instance of Divisibleby3 5.
divBy5: Divisibleby3 5
divBy5: ThreeMultiple (ThreeMultiple ?divByMinus3)We can’t directly use the Three constructor (5 isn’t 3), so we start with ThreeMultiple but that requires an instance of Divisibleby3 (5-3), so we go add another ThreeMultiple and now we need a Divisibleby3 (-3) and since Divisibleby3 takes a positive number we’re stuck.
DivisibleByX
FizzBuzz requires checking divisibility by three and five. Instead of constructing a separate data type for dividing by five, we’re going to make a generic proof type for being divisible by any number.
data DivisiblebyX : Nat -> Nat -> Type where
Base: DivisiblebyX x x
Multiple: DivisiblebyX x y -> DivisiblebyX x (x+y)DivisiblebyX has an identical structure to Divisibleby3 except now the type takes two numbers, the number to check divisiblilty against and the number we’re dividing.
As an example, proofs that 15 is divisible by 5 and 3 would look like:
divBy5_15: DivisiblebyX 5 15
divBy5_15 = Multiple (Multiple Base)
divBy3_15: DivisiblebyX 3 15
divBy3_15 = Multiple (Multiple (Multiple (Multiple Base)))Proving FizzBuzz (finally)
We now have a way of proving that a given value is divisible by three and/or five. We can use these types to constrain which variants of our FizzBuzz return type can be returned for a given value.
data FizzBuzzProofSimple: Nat -> Type where
Fizz: DivisiblebyX 3 x -> FizzBuzzProofSimple x
Buzz: DivisiblebyX 5 x -> FizzBuzzProofSimple x
FizzBuzz: DivisiblebyX 3 x -> DivisiblebyX 5 x -> FizzBuzzProofSimple x
Normal: FizzBuzzProofSimple xFizzBuzzProofSimple is a modification of FizzBuzzReturn from last time. Unlike FizzBuzzReturn, the Fizz, Buzz and FizzBuzz variants now need inputs in order to be instantiated.
To take the Fizz constructor as an example:
Fizz: DivisiblebyX 3 x -> FizzBuzzProofSimple xIf you want to construct a Fizz variant of FizzBuzzProofSimple x, then you need to have an instance of DivisiblebyX 3 x. The presence of x in both the input and output types ties them together.
There is now no way to return a Fizz, Buzz or FizzBuzz for a number without a proof that the number is divisible by everything it ought to be,
proof5: FizzBuzzProofSimple 5
proof5 = Buzz Base
proof3: FizzBuzzProofSimple 3
proof3 = Fizz Base
proof15: FizzBuzzProofSimple 15
proof15 = FizzBuzz (Multiple (Multiple (Multiple (Multiple Base)))) (Multiple (Multiple Base))Next time, we’ll look at how to construct FizzBuzzProofSimple instances programmatically.