Type hackery for the practical programmer pt. II

This post is a long time coming, and sort of anti-climactic, but I wanted to just finish off what I’d begun describing in the previous post.

We have, if you will recall:

class MapFromTuple a b where
      mapFromTuple :: a -> [b]

This is our handy way to marshal a heterogenous tuple into a uniformly-typed list. Now, we can perform our operations on this uniform list. The next step, however, is to go back from our transformed list to a heterogenous tuple. Immediately an answer presents itself:

class MapToTuple a b where
    mapToTuple :: [b] -> a

The instance declarations are correspondingly the inverse of those for MapFromTuple:

instance (Sat (MapToTupleD a x), Sat (MapToTupleD b x))
    => MapToTuple (a,b) x where
    mapToTuple [a,b] = (fromGenD dict a, fromGenD dict b)
instance (Sat (MapToTupleD a x), Sat (MapToTupleD b x), Sat (MapToTupleD c x))
    => MapToTuple (a,b,c) x where
    mapToTuple [a,b,c] = (fromGenD dict a, fromGenD dict b, fromGenD dict c)

But there’s a problem here. While mapFromTuple was a total function, mapToTuple is not, because it is polymorphic on its return type, not its argument type. So if we use mapToTuple in a casual fashion, we introduce a great deal of extra partiality. What we need is a way to carry the type context of our original tuple over to the return argument of mapToTuple, and thus guarantee that it yields the correct types in a correctly-sized tuple. And thus, we have the complete type signature for withValidation’:

withValidation' :: (MapFromTuple a (String, ValidationFuncIntern s String Dynamic),
                    MapToTuple a1 Dynamic,
                    TupleMatchTwo a a1) =>
                   a -> (a1 -> HCGI r s t) -> HCGI r s t

The first restriction says that a is something which can be transformed into something of type (String, ValidationFunctionIntern s String Dynamic). The second restriction says that a1 is something which can be transformed *from* Dynamic. The trick here is the ridiculous TupleMatchTwo class, defined as such:

class TupleMatchTwo a b | a -> b where {}
instance TupleMatchTwo () ()
instance TupleMatchTwo (Box (foo, bar-> mk a)) (Box a)
instance TupleMatchTwo ((foo, bar -> mka a), (foo, bar -> mkb b)) (a,b)
instance TupleMatchTwo ((foo, bar -> mka a), (foo, bar -> mkb b), (foo, bar -> mkc c)) (a,b,c)

… and soforth. Lots of boilerplate, but luckily, as with the other boilerplate instances, this is write-once boilerplate that saves us lots of work elsewhere. Although I’m probably butchering the term, what TupleMatchTwo gives us is a very limited type-level logic-programming function that “extracts” the last bit of a rather complicated signature from each of a set of tupled values, and returns them alone. Unfortunately, as its not a real type-level function, it has to be unrolled by hand. The end result, however, is that now we can extract what we “know” our return type must be from our argument type, and by asserting that return type statically at compile time, we can guarantee what we sought to from the beginning — that withValidation’ can be passed an arbitrary tuple of validator functions and will produce only a well typed tuple of the corresponding validated inputs.

I might be asserting too much here, but it seems like this basic paradigm maps to 90% of the use cases for heterogeneous lists — we want to operate over them in a uniform way, and then we want to properly varigate our input again before exiting the library function.

This style of input is now in the current repo of hvac, for both validation and database functions. There are also a few other nice changes I plan to blog about soon, mainly along the lines of cleaning things up and reducing dependencies.

I’ve also run into a really nifty example of what can be done with this “tuple-level programming” in my current project — a little mini-dsl for SQL suitable for embedding into hvac, on which more later.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: