Functional Doubly Linked Lists

It’s often been said that functional programming just isn’t cut out for certain tasks. File IO? Please… Databases? Forget about it!

I’ve always figured that the humble Doubly Linked list was on this list. After all, how do we implement these in C? An implementation would probably look something like this:

struct _DList
{
  struct DList * next;
  struct DList * prev;
  void * element;
} DList;

In this case, the element pointed to by prev and next have pointers to this element, if they aren’t NULL. The Doubly Linked list isn’t exactly a complicated structure, this is basically the way to do it. So, how would we do this in Haskell?

In the past, I’ve thought there were three answers to this question:

1) Use C pointers. This would involve use of unsafePerformIO, and you’d be a monster.

2) Use a singly linked list, and pretend it’s doubly linked. This would involve a “prev” function that just walks from the beginning of the list to the element before the current one. You’d be an even bigger monster than the guy who did option 1.

3) Don’t use a doubly linked list. To me, this is actually reasonable. In a world where arrays are basically always better, the only reason to use a list is because they’re very easy to deal with. If you need the level of complexity of a doubly linked list, you’re probably just better off with a different data structure.

But recently, I thought of a way to implement a doubly linked list in Haskell without being a bad person.

Preserved Here For Posterity

The implementation is actually quite simple. Here’s our type:

data DoublyLinkedList a =
   DList [a] [a] |
   Nil

Obviously, we have our Nil type for the empty list. We also have DList, which has two lists. Why two? On the left, we have the previous elements. This starts empty. On the right, we have our next elements. As we walk the list, we pop elements from the head of the right list to the head of the left list. The head of the right list is our current element. Let’s see some functions:

get :: DoublyLinkedList a -> a
get (DList _ (x:xs)) = x

This function returns the “current” element; the element at the current position in the list.

next :: DoublyLinkedList a -> DoublyLinkedList a
next (DList _ []) = undefined
next (DList prev (c:next)) = DList (c:prev) next

prev :: DoublyLinkedList a -> DoublyLinkedList a
prev (DList [] _) = undefined
prev (DList (c:prev) next) = DList prev (c:next)

These two functions move the cursor forward or backward. As you can see, when next is called, the current element is popped from the next list, and pushed onto the previous list. The opposite happens when prev is called. I’ve left the edge cases undefined, but a real implementation should do something sane here. (return a Maybe, throw an exception, etc…)

insert :: DoublyLinkedList a -> a -> DoublyLinkedList a
insert Nil e = DList [] [e]
insert (DList prev next) e = DList prev (e:next)

Elements are inserted in front of the current element.

makeDouble :: [a] -> DoublyLinkedList a
makeDouble [] = Nil
makeDouble l = DList [] l

…and it is trivial to convert a singly linked list into a doubly linked list. We can even add a pretty show instance!

instance (Show a) => Show (DoublyLinkedList a) where
   show Nil = "Nil"
   show (DList prev (c:next)) = (show $ reverse prev) ++
                              "*[" ++
                              (show c) ++
                              "]*" ++
                              show next

Obviously, we could go crazy and make a Monad instance and other things, but you get the idea. The final solution was very simple. One could even say simpler than the C version as you don’t have to worry about updating the next and prev pointers when adding elements. Sure, it took a bit of thought, but like many things in Haskell, the result was simple and elegant.

Checking Our Heads With Liquid Haskell

Consider this function:

headInTail :: [a] -> [a]
headInTail l = (tail l) ++ [head l]

Pretty straightforward, right? It takes a list, extracts the head and sticks it in the tail. Surely you’ve written something like this before. It should be fine, right?

*Main> headInTail [1,2,3]
[2,3,1]

…checks out. Let’s try a few more:

*Main> headInTail "hello"
"elloh"
*Main> headInTail ["cat"]
["cat"]

…good. And the moment we’ve all been waiting for:

*Main> headInTail []
*** Exception: Prelude.tail: empty list

Oh yeah, head and tail don’t work for empty lists… Normally, we have some choices on how to proceed here. We could wrap the function in a Maybe:

maybeHeadInTail :: [a] -> Maybe [a]
maybeHeadInTail [] = Nothing
maybeHeadInTail l = Just $ headInTail l

…which introduces an annoying Maybe to deal with just to stick our heads in our tails. Or, we could just do something with the empty list:

headInTail :: [a] -> [a]
headInTail [] = []
headInTail l = (tail l) ++ [head l]

…but what if returning the empty list isn’t the correct thing to do?

Another choice is to document this behavior (as head and tail do), and just never call headInTail []. But how can we guarantee that we never attempt to call this function on an empty list? Shouldn’t this be the type system’s problem?

Unfortunately, not all is roses and puppies. Sometimes the type system cannot help us. Sometimes somebody thought it’d be a good idea to use Haskell’s Evil exception system. Whatever the case, there are tools to help us.

Liquid Haskell

Liquid Haskell is a static code analysis tool that is used to catch just these sorts of problems. Liquid Haskell allows us to define invariants which will be enforced by the tool. Liquid Haskell is a research project that is still in development. As such, it has some rough spots, however it’s still very much capable of helping us with our problem here. But before we begin, we need to get the tool installed.

To install the tool, execute:

cabal install liquidhaskell

…simple right? Unfortunately, we’re not quite done. We need to install an SMT solver. This tool is used by Liquid Haskell. Currently, the tool defaults to Z3. I’m not sure how to use a different solver (and Z3 works just fine), so I suggest you you Z3. You’ll have to build Z3, and place the binary somewhere on the PATH. After this is done, and assuming your .cabal/bin directory is also on the PATH, testing your source file is a simple as:

liquid [FILE].hs

Let’s Have A Look

Create a haskell source file that contains the following:

headInTail :: [a] -> [a]
headInTail l = (tail l) ++ [head l]

After that’s done, let Liquid Haskell analyze your file:

liquid [YOUR_FILE].hs

A bunch of stuff should scroll by, then in a second you’ll see something similar to the following:

**** UNSAFE *********************************************


 Doop.hs:5:22: Error: Liquid Type Mismatch
   Inferred type
     VV : [a] | VV == l && len VV >= 0

   not a subtype of Required type
     VV : [a] | len VV > 0

   In Context
     VV : [a] | VV == l && len VV >= 0
     l  : [a] | len l >= 0

If you go to the line and column indicated, you’ll find the argument to tail. Conveniently, it seems that Liquid Haskell comes pre-loaded with definitions for some library functions. Normally, you’ll have to define those yourself. In fact, let’s do just that.

The next logical step here is to write a specification for our function. This specification is a statement about what sorts of values the function can take. Add the following to your source file, in the line above the signature for headInTail:

{-@ headInTail :: {l:[a] | len l > 0} -> [a] @-}

If you re-run liquid on your source file, you’ll see that the warning went away, and the program now indicates that your source is “SAFE”. So, what does this refinement mean?

Basically, these refinements are machine-checked comments. They have no impact on the program, they exist for Liquid Haskell. Think of it as being like an enhanced type signature. Like a normal type signature, we start with the name of the function, then two colons. This part, however:

{l:[a] | len l > 0}

…should be new. Basically, this part says that the list should not be empty. You should read it as “l is a [a] such that len l is greater than zero.” A lot of the notation used by Liquid Haskell comes from formal logic. Let’s break this down some more:

l:[a]

Here we bind a symbol, l, to the first list argument. At any point to the right of this symbol until the end of the scope defined by {}, we can reference this symbol.

{... | ...}

The pipe symbol indicates that we are going to make some statement about the type on the left hand side.

len l > 0

Here we state that the length of l must be greater than 0. It looks like we are calling a function, and we sort of are; len is a measure which is a special function that is used in specifications. However, the subject of measures is a post for another day.

You may now be thinking: “Well this is all well and good, but what’s to stop me from calling this function on an empty list?” To answer that, let’s implement main:

main =
   do i <- getLine
      putStrLn $ headInTail i

Add this to your source file, and then run liquid [YOUR_FILE].hs and you’ll notice that Liquid Haskell has a problem with your attempt to call headInTail:

**** UNSAFE *********************************************


 Doop.hs:3:29: Error: Liquid Type Mismatch
   Inferred type
     VV : [Char] | VV == i && len VV >= 0

   not a subtype of Required type
     VV : [Char] | len VV > 0

   In Context
     VV : [Char] | VV == i && len VV >= 0
     i  : [Char] | len i >= 0

Liquid Haskell is telling you that it can’t prove that the length of i is greater than 0. If you execute your main function, you should see that it works as expected. Type in a string, and it’ll do the right thing. Push enter right away and you’ll get an exception.

*Main> main
hello
elloh
*Main> main

*** Exception: Prelude.tail: empty list

…ick… Let’s fix this:

main =
   do i <- getLine
      case i of
         [] -> putStrLn "Get your head checked."
         _ -> putStrLn $ headInTail i

Now if you analyze your file, Liquid Haskell should be happy. Honestly, you should be happy too: the tool caught this problem for you. It didn’t go to testing messed up, and the bug certainly didn’t escape testing unfound. Your program is now objectively better:

*Main> main
isn't that neat?
sn't that neat?i

*Main> main

Get your head checked.

Architecture of Evil: Writing C In Haskell

It’s been a long road, but today our hard work pays off. You can set globals in Haskell! No more fussing about with State monads, I’m talking big boy non-thread-safe globals. This glorious piece of functionality thanks to the Data.IORef package.

someGlobal = unsafePerformIO $ newIORef "foo"

This is how you set a global. We create a global called someGlobal, and give it the initial value of foo. You’ll notice I wrap that in unsafePerformIO. Like the name implies, it is perfectly ok* to do this, after all: the IO Monad exists only to annoy you, and serves no actual purpose.

_{* Seriously though, don’t ever do this; if I catch you doing this in real code, then we are no longer friends.}

This global can be used like so:

main = do g1 <- readIORef someGlobal
          putStrLn $ show $ g1
          writeIORef someGlobal "bar"
          g2 <- readIORef someGlobal
          putStrLn $ show $ g2
          return ()

Running this code produces the following output:

"foo"
"bar"

Rejoice!

On A Serious Note

Now that we’ve all had a good laugh; please don’t ever do this. I discovered this module while messing around with the haskell bindings to OpenGL. If you’ve ever used OpenGL for even a second, you surely noticed that there is crazy amounts of state being tracked. Given this, and the fact that nobody is just going to make a “Haskell replacement for OpenGL”, an IORef seems like a reasonable alternative to some monolithic State monad transformer stack.

However, aside from supporting legacy C libraries, I can see no good reason to ever use IORef instead of State