Choosing object definitions in categories

[jwiegley]

I'm trying to represent the Z3 Monad as a Kleisli category, because I'd love to write solver equations using simple, boolean+numeric Haskell functions. However, booleans and other types in Z3 are not distinguished objects in that category: There is only one object, AST, with all morphisms being endomorphisms on that object.

[conal]

Sounds like a wonderful application of compiling to categories! I'd try using a phantomly typed wrapper. As an example, see the phantom Syn category in ConCat.Syntactic.

[jwiegley]

One place where I'm having difficulties with the phantom approach is defining IfCat:

newtype Z3Cat a b = Z3Cat { runZ3Cat :: Kleisli Z3 AST AST }

instance Category Z3Cat where
    id  = Z3Cat id
    Z3Cat f . Z3Cat g = Z3Cat (f . g)

instance IfCat Z3Cat a where
    ifC = Z3Cat $ Kleisli $ ???

The function I want to use is mkIte:

mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST

However, because my phantom types are not communicating the fact that a product is being used for the argument, I have no way of getting the separate arguments to mkIte.

[conal]

I see. I had a similar challenge with generating circuits. My solution there was to define a GADT that contains a type-based structure that I can manipulate and then later flatten. Something like the following:

data E :: * -> * where
  PrimE :: AST -> E a
  PairE :: E a -> E b -> E (a,b)

newtype Z3Cat a b = Z3Cat { runZ3Cat :: Kleisli Z3 (E a) (E b) }

instance IfCat Z3Cat a where
  ifC = Z3Cat $ Kleisli $ \ (PairE (PrimE c) (PairE (PrimE t) (PrimE e))) ->
          PrimE <$> mkIte c t e

You'll probably really want to allow non-prim Es for t and e (the then and else arguments). See prodIf in ConCat.Category and its use in ConCat.Circuit.

In this style, Z3Cat is no longer a phantom type directly. Instead, E is the phantom type in a more structured way.

[jwiegley]

Ok, here's my equation for the solver, written in plain Haskell:

equation :: (Num a, Ord a) => a -> a -> Bool
equation x y =
    x < y &&
    y < 100 &&
    0 <= x - 3 + 7 * y &&
    (x == y || y + 20 == x + 30)

Here's how I run the solver:

    res <- evalZ3With Nothing opts $ do
        x <- mkFreshIntVar "x"
        y <- mkFreshIntVar "y"
        PrimE ast <-
            runKleisli (runZ3Cat (ccc @Z3Cat (uncurry (equation @Int))))
                       (PairE (PrimE x) (PrimE y))
        assertShow ast
        -- check and get solution
        fmap snd $ withModel $ \m ->
            catMaybes <$> mapM (evalInt m) [x, y]
    case res of
        Nothing  -> error "No solution found."
        Just sol -> do
            putStrLn $ "Solution: " ++ show sol

And here's the result, which also show you the equation we submitted to Z3:

(let ((a!1 (ite (<= 0 (+ (- x!0 3) (* 7 y!1)))
                (ite (= x!0 y!1) true (= (+ y!1 20) (+ x!0 30)))
                false)))
  (ite (< x!0 y!1) (ite (< y!1 100) a!1 false) false))
Solution: [-8,2]

Now with one function, I have either a predicate that I can use in Haskell code, or an input to Z3 for finding possible arguments for which it is true!

[conal]

Nice!

Next, how about an easy-to-use "run" function, say

runZ3 :: Z3able a => Z3Cat a Bool -> IO (Maybe a)

This is a great example of compiling to categories. If it's okay with you, I'd love to show it off at work and in my keynote at Lambda Jam in Sydney next month.

[jwiegley]

Funny, I was just thinking about an easier run function during dinner now. :) And yes! The example is yours to use as you see fit. I think I'll package it up and put it on Hackage, once I've done a bit more testing. I'd also like to add support for internal homs, since Z3 allows registering "functions" by specifying the sorts and arity.

[jwiegley]

I've created a project for this example: https://github.com/jwiegley/z3cat

[conal]

Cool. How do you build & run the tests? After cabal-installing, I tried the following:

bash-3.2$ cabal test
cabal: Ambiguous build target 'z3cat'. It could be:
lib:z3cat (component)
test:z3cat (component)

[jwiegley]

Let me rename the test.

[conal]

Thanks. The test works for me now.