Explore `Iso` instances

[LeventErkok]

Andreas Abel points out the "iso-deriving mechanism: https://www.tweag.io/blog/2020-04-23-deriving-isomorphically/ introducing iso-deriving.

This could be a useful addition to simplify Mergeable and SymVal classes, in particular getValue can be more easily defined for derived types. Example he gave:

{-# LANGUAGE TypeApplications #-}
import Iso.Deriving ( As(As), Isomorphic, Inject(inj), Project(prj) )

-- Missing from iso-deriving-0.0.8:
getAs :: As a b -> b
getAs (As x) = x
One has to define some boilerplate once for every class one once to use with DerivingVia, e.g. for Mergeable:

instance (Isomorphic a b, Mergeable a) => Mergeable (As a b) where
  symbolicMerge f t x1 x2 = As . inj @a $ symbolicMerge f t (prj @a . getAs $ x1) (prj @a . getAs $ x2)
  select xs x ind         = As . inj @a $ select (map (prj @a . getAs) xs) (prj @a . getAs $ x) ind

(Instead of getAs one can probably use coerce but I find the latter a bit ugly.)

Then one can use deriving via but has to define the iso for one's record type:

data Path = Path
  { distance :: SInteger  -- ^ ...
  , forward  :: SBool     -- ^ ...
  , vertical :: SBool     -- ^ ...
  }
  deriving Mergeable via ((SInteger, SBool, SBool) `As` Path)

instance Isomorphic (SInteger, SBool, SBool) Path where

instance Inject (SInteger, SBool, SBool) Path where
  inj (x, y, z) = Path x y z

instance Project (SInteger, SBool, SBool) Path where
  prj (Path x y z) = (x, y, z)

We should investigate how to integrate this idea into SBV.

[LeventErkok]

The idea here would be if we can simplify something like this:

{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Main(main) where

import Data.SBV
import Data.SBV.Either
import Data.SBV.Control

import Prelude hiding (either)
import qualified Prelude as P

data X = I Integer
       | F Float
       deriving Show

data SX = SX (SEither Integer Float)

instance Queriable IO SX where
  type QueryResult SX = X

  create = SX <$> freshVar_

  project (SX x) = getValue x >>= pure . P.either I F

  embed (I i) = pure $ SX $ sLeft  (literal i)
  embed (F f) = pure $ SX $ sRight (literal f)

main :: IO ()
main = print =<< runSMTWith z3{verbose=True} (query p)
 where p = do e@(SX ie) <- create
              constrain $ isLeft ie
              ensureSat
              project e

One can argue this is "simple" enough, but if there's a way to generate the SX (or obviate the need for it), it'd be nice.

Note that this is usually not a big deal for product-types, as we can simply use a record type and recurse down. But for sum-types, it might pay off. Of course, since these sum-types cannot be recursive, I'm not sure if there's enough ROI to introduce yet another mechanism. Something to think about.

[LeventErkok]

On second thought; Queriable is really what the iso-deriving is for SBV. I don't see any advantage of using that over the Queriable type, which is more custom-built for SBV.

The real issue here is support for algebraic-datatypes in general; but that's a whole another can of worms.

[LeventErkok]

Here's an example using a "list" like data-type:

{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Main(main) where

import Data.SBV
import Data.SBV.Control

import qualified Data.SBV.List as L

data L = E
       | C Integer L
       deriving Show

data SL = SL (SList Integer)

instance Queriable IO SL where
  type QueryResult SL = L

  create = SL <$> freshVar_

  project (SL x) = getValue x >>= pure . foldr C E

  embed = pure . SL . literal . collect
    where collect E       = []
          collect (C i l) = i : collect l

main :: IO ()
main = print =<< runSMTWith z3{verbose=True} (query p)
 where p = do e@(SL l) <- create
              constrain $ L.length l .== 5
              ensureSat
              project e

[LeventErkok]

And here's an example for a "tree." The mapping requires a "postfix" conversion, and should work in general for arbitrary trees. It works, but it is super "ugly.:

• Support at least binary-trees natively in SBV, so we can have an easier isomorphism
• Figure out a way to do the pattern matching a bit better?

{-# LANGUAGE TypeFamilies     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Main(main) where

import Data.SBV
import Data.SBV.Either
import Data.SBV.Control

import qualified Data.SBV.List as L

data E = Lit Integer
       | Add E E
       | Mul E E
       deriving Show

data SE = SE (SList (Either Integer (Either () ())))

validSE :: SList (Either Integer (Either () ())) -> SBool
validSE = go 0
  where go = smtFunction "validExpr" $ \(len :: SInteger) l ->
                  ite (              L.length l .>= 1 .&& isLeft  (L.head l))                                    (go (len+1) (L.tail l))
                $ ite (len .>= 2 .&& L.length l .>= 1 .&& isRight (L.head l) .&& isLeft  (fromRight (L.head l))) (go (len-1) (L.tail l))
                $ ite (len .>= 2 .&& L.length l .>= 1 .&& isRight (L.head l) .&& isRight (fromRight (L.head l))) (go (len-1) (L.tail l))
                      (len .== 1 .&& L.null l)

eval :: SE -> SInteger
eval (SE lst) = go L.nil lst
  where go = smtFunction "eval" $ \(stk :: SList Integer) l ->
                 ite (                       L.length l .>= 1 .&& isLeft  (L.head l))                                    (go (fromLeft (l   L.!! 0)   L..:                stk ) (L.tail l))
               $ ite (L.length stk .>= 2 .&& L.length l .>= 1 .&& isRight (L.head l) .&& isLeft  (fromRight (L.head l))) (go (stk L.!! 1 + stk L.!! 0 L..: L.tail (L.tail stk)) (L.tail l))
               $ ite (L.length stk .>= 2 .&& L.length l .>= 1 .&& isRight (L.head l) .&& isRight (fromRight (L.head l))) (go (stk L.!! 1 * stk L.!! 0 L..: L.tail (L.tail stk)) (L.tail l))
                     (L.head stk)

instance Queriable IO SE where
  type QueryResult SE = E

  create = do lst <- freshVar_
              constrain $ validSE lst
              pure $ SE lst

  project (SE x) = getValue x >>= pure  . se2e
    where se2e :: [Either Integer (Either () ())] -> E
          se2e = go []
            where go stk             (Left i           : rest) = go (Lit i     : stk) rest
                  go (a1 : a2 : stk) (Right (Left  ()) : rest) = go (Add a1 a2 : stk) rest
                  go (a1 : a2 : stk) (Right (Right ()) : rest) = go (Mul a1 a2 : stk) rest
                  go [tos]           []                        = tos

                  -- Shouldn't happen, unless we screw something up
                  go stk xs = error $ unlines [ "se2e, junk: " ++ show xs
                                              , "stack     : " ++ show stk
                                              ]

  embed e = pure $ SE $ literal (e2se e)
    where e2se :: E -> [Either Integer (Either () ())]
          e2se (Lit i)   = [Left i]
          e2se (Add a b) = e2se a ++ e2se b ++ [Right (Left  ())]
          e2se (Mul a b) = e2se a ++ e2se b ++ [Right (Right ())]

main :: IO ()
main = print =<< runSMTWith z3{verbose=False} p
 where p = do e@(SE l) <- SE <$> free_
              constrain $ validSE l
              constrain $ L.length l .== 5
              constrain $ eval e .== 17
              query $ do ensureSat
                         project e