## Smarter conditionals with dependent types: a quick case study

Find the type error in the following Haskell expression:

`if null xs then tail xs else xs`

You can’t, of course: this program is obviously nonsense unless you?re a typechecker. The trouble is that only certain computations make sense if the `null xs` test is `True`, whilst others make sense if it is `False`. However, as far as the type system is concerned, the type of the then branch is the type of the else branch is the type of the entire conditional. Statically, the test is irrelevant. Which is odd, because if the test really were irrelevant, we wouldn?t do it. Of course, `tail []` doesn?t go wrong – well-typed programs don?t go wrong – so we?d better pick a different word for the way they do go.

The above quote is an opening paragraph of Conor McBride’s “Epigram: Practical Programming with Dependent Types” paper. As always, Conor makes a good point – this test is completely irrelevant for the typechecker although it is very relevant at run time. Clearly the type system fails to accurately approximate runtime behaviour of our program. In this short post I will show how to fix this in Haskell using dependent types.

The problem is that the types used in this short program carry no information about the manipulated data. This is true both for `Bool` returned by `null xs`, which contains no evidence of the result, as well as lists, that store no information about their length. As some of you probably realize the latter is easily fixed by using vectors, ie. length-indexed lists:

```data N = Z | S N  -- natural numbers   data Vec a (n :: N) where Nil  :: Vec a Z Cons :: a -> Vec a n -> Vec a (S n)```

The type of vector encodes its length, which means that the type checker can now be aware whether it is dealing with an empty vector. Now let’s write `null` and `tail` functions that work on vectors:

```vecNull :: Vec a n -> Bool vecNull Nil        = True vecNull (Cons _ _) = False   vecTail :: Vec a (S n) -> Vec a n vecTail (Cons _ tl) = tl```

`vecNull` is nothing surprising – it returns `True` for empty vector and `False` for non-empty one. But the tail function for vectors differs from its implementation for lists. `tail` from Haskell’s standard prelude is not defined for an empty list so calling `tail []` results in an exception (that would be the case in Conor’s example). But the type signature of `vecTail` requires that input vector is non-empty. As a result we can rule out the `Nil` case. That also means that Conor’s example will no longer typecheck1. But how can we write a correct version of this example, one that removes first element of a vector only when it is non-empty? Here’s an attempt:

```shorten :: Vec a n -> Vec a m shorten xs = case vecNull xs of True -> xs False -> vecTail xs```

That however won’t compile: now that we written type-safe tail function typechecker requires a proof that vector passed to it as an argument is non empty. The weak link in this code is the `vecNull` function. It tests whether a vector is empty but delivers no type-level proof of the result. In other words we need:

`vecNull` :: Vec a n -> IsNull n`

ie. a function with result type carrying the information about the length of the list. This data type will have the runtime representation isomorphic to `Bool`, ie. it will be an enumeration with two constructors, and the type index will correspond to length of a vector:

```data IsNull (n :: N) where Null    :: IsNull Z NotNull :: IsNull (S n)```

`Null` represents empty vectors, `NotNull` represents non-empty ones. We can now implement a version of `vecNull` that carries proof of the result at the type level:

```vecNull` :: Vec a n -> IsNull n vecNull` Nil        = Null vecNull` (Cons _ _) = NotNull```

The type signature of `vecNull`` says that the return type must have the same index as the input vector. Pattern matching on the `Nil` case provides the type checker with the information that the `n` index of `Vec` is `Z`. This means that the return value in this case must be `Null` – the `NotNull` constructor is indexed with `S` and that obviously does not match `Z`. Similarly in the `Cons` case the return value must be `NotNull`. However, replacing `vecNull` in the definition of `shorten` with our new `vecNull`` will again result in a type error. The problem comes from the type signature of `shorten`:

`shorten :: Vec a n -> Vec a m`

By indexing input and output vectors with different length indices – `n` and `m` – we tell the typechecker that these are completely unrelated. But that is not true! Knowing the input length `n` we know exactly what the result should be: if the input vector is empty the result vector is also empty; if the input vector is not empty it should be shortened by one. Since we need to express this at the type level we will use a type family:

```type family Pred (n :: N) :: N where Pred Z = Z Pred (S n) = n```

(In a fully-fledged dependently-typed language we would write normal function and then apply it at the type level.) Now we can finally write:

```shorten :: Vec a n -> Vec a (Pred n) shorten xs = case vecNull` xs of Null -> xs NotNull -> vecTail xs```

This definition should not go wrong. Trying to swap expression in the branches will result in a type error.

1. Assuming we don’t abuse Haskell’s unsoundness as logic, eg. by using `undefined`. []

## Why dependent types matter (in Haskell)

A year ago I published Agda code for “Why dependent types matter” paper by Thorsten Altenkirch, Conor McBride and James McKinna. Now I rewrote that code in Haskell. This work is similar to my recent conversion of weight-biased leftist heaps from Agda to Haskell so I won’t go into technical details. As usual you can view the code on Github.

## Weight-biased leftist heaps verified in Haskell using dependent types

In January I announced my implementation of weight-biased leftist heaps verified with dependent types in Agda. This was part of my work on a paper submitted to CAV’14 conference. The paper got rejected and I decided not to resubmit it anywhere else. At this year’s ICFP listening to Stephanie Weirich’s keynote speech motivated me to finally port that implementation to Haskell, something that I had planned for a couple of months now. You can take a look at the result on github. Here I want to share some of my experiences and insights.

My overall impression is that porting from Agda to Haskell turned out to be fairly straightforward. It was definitely not a complete rewrite. More like syntax adjustments here and there. There were of course some surprises and bumps along the way but nothing too problematic. More precise details are given in the code comments.

When it comes to programming with dependent types Agda, being a fully-fledged dependently-typed language, beats Haskell in many aspects:

• Agda has the same language for terms and types. Haskell separates these languages, which means that if I want to have addition for natural numbers then I need to have two separate definitions for terms and types. Moreover, to tie types and terms together I need singleton types. And once I have singleton types then I need to write third definition of addition that works on singletons. All of this is troublesome to write and use. (This tedious process can be automated by  using singletons package.)
• interactive agda-mode for Emacs makes writing code much simpler in Agda. Here I was porting code that was already written so having an interactive Emacs mode for Haskell was not at all important. But if I were to write all that dependently-typed code from scratch in Haskell this would be painful. We definitely need better tools for dependently-typed programming in Haskell.
• Agda admits Unicode identifiers. This allows me to have type constructors like `?` or variables like `p?b`. In Haskell I have `GEq` and `pgeb`, respectively. I find that less readable. (This is very subjective.)
• Agda has implicit arguments that can be deduced from types. Haskell does not, which makes some function calls more difficult. Surprisingly that was not as huge problem as I initially thought it will be.
• Agda is total, while Haskell is not. Since there are bottoms in Haskell it is not sound as a logic. In other words we can prove false eg. by using undefined.

The list is noticeably shorter:

• Haskell has much better term-level syntax. In many places this resulted in significantly shorter code than in Agda.
• Haskell is not total. As stated earlier this has its drawbacks but it also has a good side: we don’t need to struggle with convincing the termination checker that our code does actually terminate. This was painful in Agda since it required using sized types.
• Haskell’s `gcastWith` function is much better than Agda’s `subst`. Both these functions allow type-safe casts given the proof that the cast is safe. The difference is that Agda’s `subst` requires more explicit arguments (as I noted earlier the opposite is usually the case) and restricts the cast to the last type parameter (Haskell allows cast for any type parameter).

# Summary

While the list of wins is longer for Agda than it is for Haskell I’m actually very happy with Haskell’s performance in this task. The verification in Haskell is as powerful as it is in Agda. No compromises required.

It’s worth remarking that my implementation works with GHC 7.6, so you don’t need the latest fancy type-level features like closed type families. The really essential part are the promoted data types.

Staypressed theme by Themocracy