How can I constrain a type (kind?) to product types only

Question

I'm looking into using monad comprehensions to represent SQL queries, and generate the appropriate SQL. At first glance, this is not a problem, it seems a good fit. But I have to restrict the types, which can form the monad to products only, no sums, and I can't think of a way to place such constraints.

I want to use the type checker to ensure that only types representable in SQL can be used.

I could, I suppose, use template haskell to derive the correct instances, and refuse to derive if the type does not fit, but I would prefer it done in the type level. Less chance for me introducing bugs due to my ignorance.

How could I do this? If yes, could you recommend some reading and/or code examples please.

Edit: Thanks, I've got some good paths to follow, which require more reading :) And here comes a long weekend.

Answer 1

Unfortunately, this isn't really possible: a Monad must be fully polymorphic. It's the same reason you can't make Set a monad (the Ord constraint).

If you can deal with only having the result type meet the constraint, then you could have have runSQL :: (Product a) => SQL a -> IO a, or similar. In that case, just deriving the appropriate instances with Template Haskell is the way to go, or alternately, using the new GHC Generics; plain Haskell has no way to determine whether a type is composed of only products.

But I suspect you need to access the entire structure of the monadic computation, to translate it to SQL. Unfortunately, monads aren't very well-equipped to this, since they are plugged together with arbitrary Haskell functions, which you can't "look inside". Arrows are closer, and let you do more static analysis, but still have that pesky arr that, again, lets you sneak in arbitrary Haskell functions.

The most viable option for doing something like this is probably to write a Template Haskell splicer to parse the syntax you want; you can say $(sql [| [ (a,b) | a <- table1, b <- table2 |]) and have sql translate the AST to the corresponding SQL at compile-time If that syntax is too ugly, you write use a quasiquoter with haskell-src-meta, which would look like [sql| (a, b) | a <- table1, b <- table2 |].

You might also be interested in the generalised arrows extension, although it's probably overkill (and too experimental) for your purposes.