FAQ: best practices for records?

[andreasabel]

sbv defines a lot of instances for tuples, yet good programming practice suggests to use hand-rolled record types instead of tuple types. What are the best practices for working with records?

Records can be trivially converted to tuples and back (the latter is just uncurry<arity> <record-constructor>). Is there a systematic way to exploit this isomorphism?

E.g. I have a record Path with three fields and was prompted to define its Mergable instance. https://github.com/andreasabel/sbv-quarter-circle-puzzle/blob/fd7932a77300adfe6666ceb4c23b81a430468563/src/Board.hs#L57-L62

data Path = Path
  { distance :: SInteger  -- ^ ...
  , forward  :: SBool     -- ^ ...
  , vertical :: SBool     -- ^ ...
  }

So I went for this boilerplate: https://github.com/andreasabel/sbv-quarter-circle-puzzle/blob/fd7932a77300adfe6666ceb4c23b81a430468563/src/Board.hs#L278-L286

instance Mergeable Path where
  symbolicMerge f t p1 p2 = tupToPath $ symbolicMerge f t (pathToTup p1) (pathToTup p2)
  select ps p ind         = tupToPath $ select (map pathToTup ps) (pathToTup p) ind

pathToTup :: Path -> (SInteger, SBool, SBool)
pathToTup (Path x y z) = (x, y, z)

tupToPath :: (SInteger, SBool, SBool) -> Path
tupToPath (x, y, z) = Path x y z

At some other time I wanted a Symbolic instance of a record.

Are there quicker ways to get the boilerplate?

I tried deriving Mergeable via (SInteger, SBool, SBool) but to no avail:

Couldn't match representation of type ‘(SInteger, SBool, SBool)’
with that of ‘Path’

GHC's DerivingVia seems less clever than one would hope for...

[andreasabel]

I looked at https://www.tweag.io/blog/2020-04-23-deriving-isomorphically/ introducing iso-deriving.

{-# 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)

The instance Mergeable (As... could go into sbv or some add-on package sbv-iso-deriving, and then the user only has to do the easy boilerplate, the instance Isomorphic for their record type. So while this is less automatic than one could hope for, something like this could be a good practice.

[LeventErkok]

Hi Andreas,

I wasn't aware of the iso-deriving work; looks really interesting. If you find it useful, indeed I'd love to have it added to SBV. (I'm in general not in favor or add-on-packages. I think they make things more complicated than necessary, especially for a package like SBV where backwards compatibility isn't a big issue.)

For your example though, I think the generic way of deriving Mergeable might be the easiest? Something like:

{-# LANGUAGE DeriveAnyClass #-}

import Data.SBV
import GHC.Generics

data Path = Path { distance :: SInteger
                 , forward  :: SBool
                 , vertical :: SBool
                 }
                 deriving (Generic, Mergeable)

with the above, you can say:

newPath :: String -> Symbolic Path
newPath pre = Path <$> free (pre ++ "_distance")
                   <*> free (pre ++ "_forward")
                   <*> free (pre ++ "_vertical")

main :: IO ()
main = print =<< sat example
 where example = do p1 <- newPath "p1"
                    p2 <- newPath "p2"

                    constrain $ distance p1 .>= 5
                    constrain $ distance p2 .>= 12

                    pick <- sBool "pick"

                    let result = ite pick p1 p2
                    constrain $ distance result .< 12

Then you have:

*Main> main
Satisfiable. Model:
  p1_distance =     5 :: Integer
  p1_forward  = False :: Bool
  p1_vertical = False :: Bool
  p2_distance =    12 :: Integer
  p2_forward  = False :: Bool
  p2_vertical = False :: Bool
  pick        =  True :: Bool

Would this work for you? For a more "worked out example" of this, see Orangutans.hs

I've also used other encodings in the past, with varying degrees of ease-of-use, readability aspects. Another idea is to go more parametric, something like:

data SumS a = SumS { n :: a    -- ^ The input value
                   , i :: a    -- ^ Loop counter
                   , s :: a    -- ^ Running sum
                   }
                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)

Then you can have:

type S = SumS SInteger
type C = SumS Integer

and write converters between them. (See Sum.hs for a worked out example.)

I like the generic-derivable way since it's really easy to use. If that's not enough (with query mode they become clunky), I go for the more parameterized way. Neither is perfect but so far they handled my use cases.

Feel free to send a PR that adds the iso-deriving mechanism. If you can also add an example that demonstrates its use (under Documentation/SBV/Examples/Misc perhaps?), that'd be wonderful.

[andreasabel]

think the generic way of deriving Mergeable might be the easiest?

Excellent, indeed this works like a charm, no boilerplate!

[LeventErkok]

Great! I captured the iso-deriving idea in a separate ticket (#705). I think we can close this one; but feel free to file other issues if you run into further trouble.