Haskell has a flexible type system. It actually is Turing complete given the right language extensions. This also means that we can do arbitrary computations, which we are going to exploit in this 10th day in my 100 days of Fibonacci challenge.

I already did look at Haskell. So strictly speaking I should choose another language. However, I find that programming in Haskell's type system is different enough that I will consider it a different language.

Day 9 - Haskell Types

Today I implemented Fibonacci in the Haskell type system. That means that I can get the Haskell compiler to generate a type for the n'th Fibonacci number.

I first created a datatype for representing naturals. The approach as in the last part of the Prolog implementation and use used in Coq was used. This representation builds on the Peano axioms and is straight forward to implement.

data Nat = Z | S Nat

This datatype is usable as a kind because we use the language extension DataKinds. A kind can be thought of as a type of a type.

In ghci we can inspect the kind of the type constructor Z by issuing :kind Z. The result returned is Z :: Nat.

Next I implemented addition. In Haskell we use the language extension TypeFamilies to have a mechanism for implementing type level functions.

type family Add (a :: Nat) (b :: Nat) :: Nattype instance Add  Z    b = btype instance Add (S a) b = S (Add a b)

Again we can try to inspect the kind of the type level function: :kind Add (S Z) (S Z) which yields Add (S Z) (S Z) :: Nat as expected.

To actually calculate the Fibonacci type we need Haskell to reduce the Add expression. This is done using the :kind! Add (S Z) (S Z) operation.

*FibType> :kind! Add (S Z) (S Z)Add (S Z) (S Z) :: Nat= 'S ('S 'Z)

We can now both define type level datatypes (kinds) and do operations on these. Along this line I implemented Fibonacci straight forward in direct recursion.

type family Fibonacci (n :: Nat) :: Nattype instance Fibonacci Z           = Ztype instance Fibonacci (S Z)       = (S Z)type instance Fibonacci (S (S n))   = Add (Fibonacci n) (Fibonacci (S n))

To implement above type family I had to add the language extension UndecidableInstances. This is because of the use of the Add type family in the Fibonacci type family.

In this example, however, it is easy to see that the type family will always converge. Add converges (and does not need UndecidableInstances) and Fibonacci converges as the arguments to the recursive applications are decreasing.

The last thing is to actually calculate Fibonacci. This can be done by issuing the :kind! as earlier on and read the result. The returned value is not easily readable but it is 13 as expected.

$ ghci FibType.hs -XDataKinds...*FibType> :kind! Fibonacci (S (S (S (S (S (S (S Z)))))))Fibonacci (S (S (S (S (S (S (S Z))))))) :: Nat= 'S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))

The code is as usual available on Github.

Types alone does, however, not make a program. We need some kind of value level implementation. In the next section I make a similar implementation of the type level functions on the value level. Coupling the type and the value in an one-to-one correspondence yields dependent programming

Dependent types are used to statically reason about programs and put up guarantees that can be checked on compile time. In this case we can set up the guarantee that the code actually calculates the n'th Fibonacci number.

Implementing Dependent Typing

With dependent typing the type of a term depends on its value. In Haskell we can benefit from making some parts of the types dependent. This could for example be statically sized lists to make matrix operations type-safe.

In this post I implement complete dependency between terms and their type. The type for the Fibonacci term was implemented above. Now we just need to write some code that couples it to the value level.

First we couple the datatype. I implemented a value level datatype, SNat, which embeds its size.

data SNat (a :: Nat) where    SZ   :: SNat Z    SS   :: SNat n -> SNat (S n)

In the above the value level constructor has the type SNat Z. From this type alone, we can read that it is the zero element.

The successor value constructor has the type SNat n -> SNat (S n). Here the type is constructed depending on which number element we construct.

An important property of above datatype is the bijection between a datatype and its type. This is what we use to statically reason about our programs and make sure certain guarantees are held.

After that we implement the addition function

add :: SNat m -> SNat n -> SNat (Add m n)add SZ      b = badd (SS a)  b = SS (add a b)

The value level add function stays completely true to the type-level add function and is together with the Fibonacci function below fairly self explanatory.

fibonacci :: SNat n -> SNat (Fibonacci n)fibonacci SZ            = SZfibonacci (SS SZ)       = (SS SZ)fibonacci (SS (SS n))   = add (fibonacci n) (fibonacci (SS n))

We now build a Fibonacci function where the returned value is bijective to its type. Hence we are sure that what is computed at runtime is something we can predict on compile time.

$ ghci -XDataKinds FibType.hs ...*FibType> let f = fibonacci $ SS $ SS $ SS $ SS $ SS $ SS $ SS $ SZ*FibType> :t ff :: SNat       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))*FibType> f13

As expected the type of the term fibonacci 7 has the type 13 (translated from the unary representation to decimal). After evaluating the term we also get the value 13.

Applications for Dependent Programming

All above is perfectly good. But why bother writing so much more code to just have a dependency between the value and its type? Well, for most applications this is not necessary, but the technique can be used to set strict guarantees in certain situations.

When you know the shape of the data-types on compile-time it can be advantageous to model this shape into the program. This could be some uses of matrices.

When implementing for example neural networks, the upper bound on the topology is usually known when writing the code. In this case one could use type safe matrix libraries to implement this functionality.

Conclusion

In this post I first implemented the Fibonacci function on the type level. I made a type for the n'th element in the Fibonacci series. This was done through data kinds and type families.

After this a value level implementation was implemented. It was implemented in such a way that its type was bijective to its return value.

The dependency between the terms and the types was carried out through GADTs which allows us to encode the type level natural in the types for the values.