When existentials aren't enough

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE RankNTypes #-}
> module Exists where

I've discovered a certain trick that seems to recur in my code. It might be a sign of me having too much time on my hands, which is commonly referred to as "perfectionism". Anyway, I thought I'd share it with the class. And forgive me if my exposition is overly generic; I do have real examples, but there is some extra stuff that obscures the general idea, which is what I want to present here.

Let's start with the simple example. Suppose we have some input, and want to generate some output from it (remember, I've told you it would be generic). Such "generator" is just a function of type

> type Gen1 m input output = input -> m output

Note that generation is done inside some arbitrary monad, so as to allow side effects.

How do we use such a function? Well, that's very simple, we just apply it and use it's result:

do output <- gen1 input
   process output

That's certainly good, but imagine that this generation has something existential about it. The output we generate has an additional argument — sometimes it would be a phony type intended to be a "marker" of this specific output (which is the case in my real-life code); sometimes it would read the type from external sources, etc.

Well, that's not a problem at all; existential types (superseded by GADTs) serve exactly that purpose. So, in this case we use an existential type

> data Exists output where Exists :: output phony -> Exists output

Then the generator would have a slightly different type

> type Gen2 m input output = input -> m (Exists output)

Using such a generator is almost as easy as the first one:

do e <- gen2 input
   case e of Exists output -> process output

In fact, we can easily convert the generator of the second type to the generator of the first type. The only thing we'd have to care about is adding this extra "phony" type to the output. We can do it like this:

> newtype WithPhony output phony = WithPhony output

Now, the actual conversion is done like this:

> withPhony :: Monad m => Gen2 m input (WithPhony output) -> Gen1 m input output
> withPhony gen2 = \input -> do {Exists (WithPhony output) <- gen2 input; return output}

Here comes the trick I've been talking about earlier. Assume that our generator is somewhat recursive, so that it's input depends on the output. What's worse, we need it to have this extra type as well. So the situation seems freaky: we have all the essential parts of input, then we need to generate output AND find out the "phony" type, so that we can amend our input. That's not usually a problem when there are no extra types; but with them in place things become interesting.

Let me give a (kinda real) example. Assume that you're creating a couple of tables in a database. You want to mark them with phony types, so that indices for one table are not accidentally used with another. Normally that would be like a situation described above, with existential types; but now you also want those two tables to reference one another. That mean that the specification (something like CREATE TABLE command) for each of them contains the phony type that marks another one. So we can't know the phony types beforehand; we can't define them externally, because then it would be possible to create two different table with the same marker type; and we need them as part of our input. Tricky.

So, returning to the general question, we have some function of type

> type ProduceInput m part input phony = part phony -> m (input phony)

Note that we don't use the full output; type safety aside, it's quite possible that we can't pass the full output "back in time", only the part of it.

Let's ask ourselves a question: suppose that we have the "generator" that produces our output, and it's type correct. When we use it — what would we have other than the generator itself?

Instead of input we would now have the function that produces the input from the part of output. Is that all?

No. We would also have the processing function, which takes the output and produces some result. It was present in the examples above, but it was not treated as part of the equation. But there is no reason why it shouldn't. And what's more exciting is that we don't really care about the extra types; we only care about the final outcome. So, we have this data:

> data Gen3Input m part input output phony result =
>     Gen3Input (part phony -> m (input phony)) (output phony -> m result)

And that's exactly what we need. Now our generator can be typed as this:

> type Gen3 m part input output =
>     forall result. (forall phony. Gen3Input m part input output phony result) -> m result

Using this generator is straightforward; in fact, it's even easier than using first two versions:

gen3 $ Gen3Input generateInput process

Writing this kind of generators is more challenging, but only because it does a more complicated job. Essentially the process is outlined above: we produce our input using the part of the output, not yet known; in the lazy world of Haskell this is completely normal, it's just that the input won't be generated fully until the next step. Then we compute the output from the input, using whatever techniques we need, and feed the required part of it back to the input producer.

For example, in case of two tables referencing each other, the only "part" we need is the markers themselves; so, this "part" would actually contain zero bits of real information. Therefore we can have our "input" (the specifications of tables) in full, and create tables from it.

We can, as before, convert this generator to the previous one. The part of the output we feed back would be void here.

> data Void phony = Void

We also add extra phony type parameter to input. The conversion itself is quite simple.

> withDep :: Monad m => Gen3 m Void (WithPhony input) output -> Gen2 m input output
> withDep gen3 = \input -> gen3 $ Gen3Input (\Void -> return (WithPhony input)) (return . Exists)

Note that here we don't use the full continuation as our processing function; we only need to advance it a bit farther than extra type goes. The existential type constructor gets rid of it, so we can stop there.

Well, class, that's it for today.