What are some good examples of programs that are easy to specify as dependent types, but difficult to implement?

Question

Last year, I asked, “Dependent Types can prove that your code conforms to the specification. But how do you prove the specification is correct? ” The most voted answer presents the following reasoning:

We hope that your specification is simple and small enough to judge by the exam, while your implementation may be much larger.

This line of reasoning makes sense to me. Idris is the most accessible language for testing these concepts; however, since it can be used to a large extent as Haskell, it often leaves the programmer wandering around the old concepts, not knowing where to use the dependent types. Some real-world examples can help with this, therefore , what good, concrete examples of programs that occur in practice can simply be expressed as types, but difficult to implement?

Answer 1

This is strange for me, because my problem is that in all cases dependent types are needed. If you do not see this, look at programs this way.

Say we have f :: Ord a => [a] -> [a] (I will use the Haskell notation). What do we know about this function f ? In other words, what can you predict about applications like f [] , f [5,8,7] , f [1,1,2,2] ? Say you know fx = [4,6,8] , what can you say about x ? As you can see, we know little.

Then suppose I told you that the real name f is sort . What can you tell me then about the same examples? What can you say about ys with respect to xs in f xs = ys ? Now you know a lot, but where did this information come from? All I did was change the name of the function; it does not matter in the formal sense of the program.

All this new information comes from what you know about sorting. You know two defining characteristics:

• sort xs is a permutation of xs .
• sort xs monotonically increases.

We can use dependent typing to prove both of these properties for sort . Then it is not only about our external understanding of sorting; sorting value becomes an integral part of the program.

Catching bugs is a side effect. The real goal is to indicate and formalize what we need to know in our heads as part of the program.

Carefully review the programs you have already written. What are the facts that make your work in a program that is only known in your head? These are all examples of candidates.

Answer 2

I will answer this:

often he leaves a programmer wandering around old concepts, not knowing where to use dependent types

Of course, types can be used to eliminate some types of stupid errors, for example, when you apply a function to your arguments in the wrong order, but that’s not what types really need. Types structure your reasoning and allow you to scale the structure of your calculations.

Tell you the process lists and use head and tail lot, but these are partial functions, so you decide to switch to something more secure, and now you are processing NonEmpty a instead of [a] . Then you realize that you are also doing a lot of lookup (partial function again) and that it will not be too troublesome to maintain the duration of your lists statically in this particular case, so you switch to something like NonEmptyVec na , where n is the statically known length of the vector. Now you have eliminated many possible errors, but this is not the most important thing that has happened.

Most importantly, now you look at the type signatures and see what input functions are expected and what output they produce. The possible behavior of the function has been narrowed by its type signature, and now it is much easier to determine where the function belongs in the pipeline. But the more detailed types you have, the more your entity is encapsulated: a function of type NonEmpty a -> b no longer relies on the assumption that it will be passed a non-empty list, instead it explicitly requires that this invariant be preserved. You have turned the iron-like tightly coupled calculation into fine-grained.

Rich types are designed to guide people (before writing code, while writing code, after writing code) and reduce their ability to create errors in the first place, and not to determine their posteriori. Simple types I consider unavoidable, because even if you write code in a dynamically typed language, you still distinguish between a line and a picture.

---

Enough chit-chat, here is a real example of utility and, more importantly, the naturalness of dependent types. I focus on the API using the Servant library (which is an amazing piece of code and is also typed, so you can check it out):

 type API ar = ReqBody '[JSON] (Operation a) :> Post '[JSON] (Result r) 

So, we send a request of type Operation a (automatically encoded in JSON from Servant) and get a response Result r (automatically decoded from JSON by the Servant service). Operation and Result defined as follows:

 data Method = Add | Get data Operation a = Operation { method :: !Method , params :: !a } data Result a = Result { result :: !a } 

The task is to perform operations and receive responses from the server. However, the problem is that when we Add things, server responses with AddResults and when we Get things, the server’s response depends on what we passed along with the Get method. Therefore, we write a family of types:

 type family ResultOf ma where ResultOf Add a = AddResults ResultOf Get DictionaryNames = Dictionaries 

The code reads better than my description above. It remains only to raise Method to the level of the type, so we define the corresponding singleton (which is the way to emulate dependent types in Haskell at the moment):

 data SMethod m where SAdd :: SMethod Add SGet :: SMethod Get 

And here is the signature of the type of the main function (many unrelated things are omitted):

 perform :: SMethod m -> a -> ClientM (ResultOf ma) 

perform receives a method in a singleton form and some value and returns the calculation in the Servant ClientM monad. This calculation returns a result whose type depends on both the method and the type of value: if we are SAdd , we get AddResults ; if we are SGet DictionaryNames , we get Dictionaries . Very reasonable and very natural - there is no need to invent where to use dependent types: the task requires them aloud.