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 x
```

**FizzBuzzProofSimple** 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 x`

If 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.