A Route To Learning The Haskell Type System

TL;DR I start trying to write a library and get sidetracked into learning about Haskell’s type system.

So last time, I talked about Wai and how you could use it directly. However, if you’re going to do that, you’ll need a routing library. So, let’s talk about how we could build one up. One of the first things you’d need to do is to provide simple boolean conditions on the request object.

It turns out that this raises enough questions for someone at my level to fill more than one blog post.

{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}

import qualified Network.Wai as Wai
import qualified Network.HTTP.Types as H

So, how should we define conditions? Well, the Clojure model of keyword and string isn’t going to work here, because the Wai.Request object is heavily strongly typed. So how about instead we just use the expected values and deduce the key from the type?

So, we’re going to want to implement the same method for several different types. There’s several different ways of doing that: * Create a union/enum class. This is a good approach, but not extensible. * Create a typeclass, which is extensible. * Create a type family, which is also extensible, but I don’t really understand.

You Can’t Buy Class

With that in mind, let’s create our first typeclass!

class RequestCondition rc where
  isMatch :: Wai.Request -> rc -> Bool

So, in English this says “If the type rc is a RequestCondition then there is a method isMatch which takes a Wai.Request and an rc and returns a Bool.” This is pretty interesting from an OO standpoint. The OO representation would look like rc.isMatch(request). A Clojure protocol would change this to (isMatch rc request). In practice, it doesn’t matter: what’s happening is that there’s dynamic dispatch going on on the first parameter.

In the Haskell case, there’s no dynamic dispatch in sight and the first parameter isn’t special. isMatch on HTTPVersion and isMatch on Method are different functions.

We can now implement the RequestCondition for some obvious data types.

instance RequestCondition H.HttpVersion where
  isMatch = (>=) . W.httpVersion

So, here we’ve said “calling isMatch with a HttpVersion as a parameter calls (>=) . W.httpVersion i.e. checks the request is using the version specified. We’d probably need a more sophisticated way of dealing with this if we were writing a real system.

instance RequestCondition H.Method where
  isMatch = (==) . W.requestMethod

This is much the same, with one wrinkle: H.Method isn’t actually a type. It’s a type synonym. In C++ you’d introduce one with typedef, in C# with using. Haskell, because it likes to confuse you, introduces something that is not a type with the keyword type. If you look up method on Hackage you see:

type Method = ByteString

You might wonder why this matters. The answer is that the Haskell standard doesn’t allow you to declare instances of synonyms. You can understand why when you realize that you might have multiple synonyms for ByteString and shoot yourself in the foot. However, for now I’m going to assume we know what we’re doing and just switch on TypeSynonyms in the header.

Let’s do one more, because three’s a charm.

instance RequestCondition H.Header where
  isMatch = flip elem . W.requestHeaders

We’d need (a lot) more functionality regarding headers, but let’s not worry about that now. However, again this will fail to compile. This time H.Header is a type synonym, but a type synonym for a very specific tuple.

type Header = (CIByteString, ByteString)

Problem is, Haskell doesn’t like you declaring instances of specific tuples either. This time, you need FlexibleInstances to make the compiler error go away. To the best of my knowledge, FlexibleInstances is much less of a hefalump trap than TypeSynonyms could be.

For fun, let’s throw in a newtype

newtype IsSecure = IsSecure Bool

isSecure :: IsSecure
isSecure = IsSecure True

instance RequestCondition IsSecure where
  isMatch r (IsSecure isSecure) = W.isSecure r == isSecure

Under Construction

How about when we’ve got multiple conditions to apply? Well, if we were writing Java, we’d be calling for a composite pattern right now. Let’s declare some types for these.

newtype And rc = MkAnd [rc]
newtype Or rc = MkOr [rc]

I described newtypes back in Fox Goose Corn Haskell. Note that there’s no reference to RequestCondition in the declaration. By default, type variables in declarations are completely unbound.

Before we go any futher, let’s fire up a REPL (if you’re in a Haskell project right now you can type cabal repl) and take a look at what that does:

data And rc = MkAnd [rc]
:t MkAnd
MkAnd :: [rc] -> And rc

Yes, MkAnd is just a function. (Not exactly, it can also be used in destructuring, but there isn’t a type for that.) Let’s try expressing it a different way while we’re here:

:set -XGADTs
data And2 rc where MkAnd2 :: [rc] -> And2 rc

(You’ll need to hit return twice) Now we’re saying “And2 has one constructor, MkAnd2, which takes a list of m. The GADTs extension does way more than this, some of which I’ll cover later on, but even then I’m only really scratching the surface of what this does. For now I’ll just observe how the GADTs extension provides a syntax that is actually more regular than the standard syntax.

Incidentally, I could have called MkAnd just And, but I’ve avoided doing so for clarity.

Composing Ourselves

With the data types, we can easily write quick functions that implement the RequestCondition typeclass.

instance (RequestCondition rc) => RequestCondition (And rc) where
  isMatch r (MkAnd l) = all (isMatch r) l

instance (RequestCondition rc) => RequestCondition (Or rc) where
  isMatch r (MkOr l) = any (isMatch r) l

The most interesting thing here is that we haven’t said that And is an instance of RequestCondition, we’re say that it is if its type parameter is an instance of RequestCondition. Since data types normally don’t have type restrictions themselves, this is the standard mode of operation in Haskell.

So, now I can write

Or [H.methodGet, H.methodPost]

and it’ll behave. So we’re finished. Right? Not even close.

What if we wanted to write

And [H.methodGet, H.http10]

It’s going to throw a type error at you because HTTP methods aren’t HTTP versions. If you take a look at the declaration, it says “list of rcs that are instances of RequestCondition” not “list of arbitrary types that are instances of RequestCondition“. If you’re used to OO, (and I have some bad news for you if you’re a Clojure programmer, that means you) this makes no sense at all. If you’re a C++ programmer, this is going to make a lot more sense. You see, when you do that in Java you’re telling Java to call through a vtable to the correct method. Haskell doesn’t have pervasive vtables in the same way. If you want one, you’re going to have to ask nicely.

Pretty Please and Other Existential Questions

What we want, then, is a function that boxes up a RequestCondition and returns a type that isn’t parameterized by the original type of the RequestCondition. What would that function look like?

boxItUp :: (RequestCondition rc) => rc -> RequestConditionBox

Hang on, that looks like the type of a constructor! Except for one really annoying little detail: as I said before, you can’t put type restrictions in data declarations.

Except you can, if you enable GADTs.

data RequestConditionBox where
  RC :: (RequestCondition rc) => rc -> RequestConditionBox

RequestConditionBox is what’s known as an “existential type”. As I understand it that should be interpreted as “RequestConditionBox declares that it boxes a RequestCondition, but declares nothing else”. So its quite like declaring a variable to be an interface.

Since I wrote this, I’ve learned that existential types are indeed very like interfaces in C#/Java: they are bags of vtables for the relevant type classes. They don’t expose their parameterization externally, but destructuring them still gets the original type out. This is bonkers.

It just remains to actually implement the typeclass:

instance RequestCondition RequestConditionBox where
  isMatch r (RC m) = isMatch r m

And now we can finally write

And [RC H.methodPost, RC isSecure]

And the compiler will finally accept it. Not quite as pretty as in an OO language where polymorphism is baked into everything, but keeping the character count low isn’t everything. We’ve traded implicit polymorphism for explicit polymorphism.

So we’re done, right? Well, we could be, but I want to go further.

The Power of Equality

If you take a look, what we’ve built looks very much like a toy interpreter (because it is one). What if we wanted a toy compiler instead? In particular, imagine that we really were building a routing library and we had thousands of routes. We might want to only check any given condition once by grouping, for example, all of the GET routes togther.

Now, you could leave that to the user of the library, but let’s pose the question: given two RequestConditions, both of which may be composite, how do you determine what conditions are common between the two?

One route is to backtrack, and look at HLists. I think that’s probably an extremely strong approach, but I really haven’t got my head around the type equality proofs-as-types stuff. Another approach is add some stuff to RequestCondition to track the types in some way. It turns out there’s a way to get the compiler to do most of the work here, so I’ll talk about that next time.

FOOTNOTE: On the Reddit discussion it was pointed out that RequestConditionBox is an example of the existential type anti-pattern. To summarize: if all you’ve got is a bunch of methods, why not just have a record with those methods as properties? If all you’ve got is one method, why not just use a function.

This is a completely valid criticism of the code in this post as a practical approach. However, we wouldn’t have learned about existential types in the first place, and we couldn’t make functions implement Eq and Show. Implementing Eq is the subject of the next post.

The commenter also added an elegant implementation of the functionality given above in terms of pure functions.

EDIT: Lennart Augustsson clarified that existential types do indeed construct vtables. So “boxing” something in an existential type is very like casting a struct to an interface it implements in C#. I should also clarify that the word bonkers used in the above text was meant as a good thing. 🙂