Return multiple Vars from a single Command

[ChickenProp]

I have a state machine where one Command's output type is (FooId, BarId). That gets put into the model, so I have ids :: Var (FooId, BarId) v in my state. Then any time I want to pass either FooId or BarId into a commandExecute, it needs to get both of them and deconstruct.

I think it would be possible to change things so each Command can return multiple Vars at once. The state would get fooId :: Var FooId v, barId :: Var BarId v, the same as if they'd come from different Commands.

The sketch is that output would move from being kind Type to (Type -> Type) -> Type like input, parameterized by Symbolic or Concrete. commandExecute returns m (output Concrete). Update gets output v instead of Var output v, and Ensure gets output Concrete instead of just output. Where I currently return (fooId, barId), I'd instead return Tuple2B (Concrete fooId, Concrete barId), where

data Tuple2B a b f = Tuple2B (f a) (f b) -- feels like this should already exist somewhere?

Then we need some instances from barbies to generate the vars. From a bit of exploration, I think giving Tuple2B a b instances of ApplicativeB, TraversableB and ConstraintsB is enough. bpure lets us generate Tuple2B (Const ()) (Const ()) :: Tuple2B a b (Const ()), and then we can btraverseC to generate a Name for each of those Consts. (We need ConstraintsB because of the Typeable constraint in Symbolic.)

(I think that would need us to require barbies >= 2.0.0.0, but my guess is that wouldn't cause problems? It only has two dependencies itself, base >= 4.11 and transformers, and it was released in Jan 2020.)

This does make single-var Commands a bit more complicated, they now return Var (Concrete x) instead of just x. (Or I think we'd want a new newtype SoloB a f = SoloB (f a) on the grounds that Var feels like it only works here "by coincidence". I'm a bit surprised there's nothing like SoloB in the barbies package.) Commands currently returning () can just return barbies' Unit. I think it would be possible to do this mostly backwards-compatible, similar to how #456 does it, though perhaps more awkward.

I've made a bit of progress on this that makes me think it works, but not yet in a sharable state. If it's wanted I can finish it off.

[ocharles]

This is an interesting idea. My usually approach for returning multiple values is to work within the framework that Hedgehog gives us, but to then essentially store defunctionalized functions to extract elements where I need them.

So let's say you have something that outputs (FooId, BarId), and something later needs just a FooId. First, for my state type I would store:

data State f = State
  { foos :: [Expr FooId f]
  , bars :: [Expr BarId f]
  }

And I then create a command type like:

data CallBar f = CallBar
  { fooId :: Expr FooId }

The trick here is the Expr type, which might be something like:

data Expr a f where
  V :: Var a f -> Expr a f
  Fst :: Expr (a, b) f -> Expr a f
  Snd :: Expr (a, b) f -> Expr b f

You would also write an evaluator for this, when you have Concrete Exprs:

eval :: Expr a Concrete -> a
eval = \case
  V v -> concrete v
  Fst e -> fst $ eval e
  Snd e -> snd $ eval e

So now when my first command completes, I can provide a Update like:

Update $ \s input outputV -> s
  { foos = Fst (V outputV) : foos s
  , bars = Snd (V outputV) : bars s
  }

I haven't done a huge amount with this, but I thought it was worth sharing an alternative approach.

[ChickenProp]

From a bit of exploration, I think giving Tuple2B a b instances of ApplicativeB, TraversableB and ConstraintsB is enough.

Oh, I now think these constraints are too weak if we want to avoid runtime crashes.

The problem is that we need to be able to pair off the vars created during the symbolic run with those created during the concrete run. That's fine with something like Tuple2B, because Tuple2B a b Symbolic always has two Names and Tuple2B a b Concrete always has two concrete values.

But it doesn't work with something like

newtype ListB a f = ListB [f a]

which I think (haven't fully checked) can have all the relevant instances. One could define bpure for that as any of

bpure _ = ListB []
bpure x = ListB [x]
bpure x = ListB $ replicate n x -- for any `n`
bpure x = ListB (repeat x)

and the execute function can return any number of Concretes.

From the class documentation, it sounds like DistributiveB gives the constraints we want? But I haven't taken the time to understand it properly. I don't even have a good handle on regular Distributive.

I'm also less confident than I used to be that it would work for things like Tuple2B. I've only done a partial implementation so far and just assumed the bits I didn't do would be easy, and I'm realizing there are bits I'd forgotten to think about. I still guess they'd be fine, but yeah, less confident.

So probably this needs more exploration, which I'm unlikely to get to in the immediate future. In the meantime @ocharles' suggestion is a neat trick.

[spacekitteh]

@ocharles that's a huge help, thanks!

[endgame]

The documentation for distributive:Data.Distributive.Distributive says:

To be distributable a container will need to have a way to consistently zip a potentially infinite number of copies of itself. This effectively means that the holes in all values of that type, must have the same cardinality, fixed sized vectors, infinite streams, functions, etc. and no extra information to try to merge together.

This is probably why your ListB example fell down.

I think DistributiveB is the ticket: things look awkward but doable if you have it. bdistribute requires a Functor on the outside, and Symbolic is not a Functor. We can make it one by cribbing off of Coyoneda but we don't carry a b. Instead, we carry around a TypeRep b so we know what type we "came from" when we replace Symbolic values by Concrete ones:

data Symbolic a where
  Symbolic :: TypeRep b -> Name -> (b -> a) -> Symbolic a

instance Functor Symbolic where
  fmap f (Symbolic rep n g) = Symbolic rep n $ f . g

Then you can do something like this:

data Record f = Record
  { foo :: f Int,
    bar :: f Char
  }
  deriving stock (Generic)
  deriving anyclass (FunctorB, DistributiveB)

deriving instance (forall a. Show (f a)) => Show (Record f)

-- Assume this is passed into an Update hook; we wouldn't really make one by hand
rSym :: Symbolic (Record Identity)
rSym = symbol (Name 0)

rSymParts :: Record Symbolic
rSymParts = bdistribute' rSym

And then I think you're basically there, modulo writing some slightly-gnarly library code. I think you have to make the commandExecute have the new type commandExecute :: input Concrete -> m (output Concrete) and change Update to Update :: forall v. Ord1 v => state v -> input v -> output v -> state v. The increased symmetry makes me think this is going the right way, though now I really want to rearrange the arguments into Update :: forall v. Ord1 v => input v -> output v -> state v -> state v.

[endgame]

I just noticed how similar this is to what @ocharles is doing, but it's able to hold arbitrary functions next to a Symbolic. This makes me think there's probably a version of his trick which uses Coyoneda v a instead of a defunctionalised syntax tree. This seems usable today without having to rework the guts of hedgehog:

data Record v = Record
  { foo :: Coyoneda v Int,
    bar :: Coyoneda v Char,
    baz :: String
  }

-- Imagine this is in an 'Update' callback.
-- When you are in an 'Ensure' callback, you'll have `Coyoneda Concrete a` everywhere;
-- `Concrete` is a functor so you can `lowerCoyoneda` to get your specific `a`.
update :: Ord1 v => Record v -> Var (Int, Char) v -> Record v
update r (Var v) = r
  { foo = fst <$> liftCoyoneda v,
    bar = snd <$> liftCoyoneda v
  }

But I think passing around an output v instead of a Var output v would make things a lot more regular, and then users can use DistributiveB if and when it's appropriate.

[ChickenProp]

@endgame thanks for looking into this! Coyoneda seems neat.

Note that your proposed definition of Symbolic means we no longer get Eq or Ord instances for it. I'm not sure how big a deal that is. I can imagine there are people using symbolic vars as map keys who'd be annoyed if they had to stop. (Though it seems risky because when you reify that map, different symbolic vars might become equal concrete vars and then what? But it still feels like a useful thing to sometimes do.)

But I'm not sure we need the Functor instance? I don't remember very well what I was thinking when I wrote the previous comments, but I don't think we'd need the Symbolic (Record Identity) in your example. Rereading and looking back at State.hs, what I think we need is

1. m (Record Symbolic) for some monad m, to replace contextNewVar. This is what I was doing with bpure and bTraverseC.
2. Given a Record Symbolic and a Record Concrete, pair off the symbolic names with the actual values and insert all these into an environment. This feels like it should be possible, and the description of DistributiveB feels like it fits. But I haven't figured out details. It looks like bprod from ApplicativeB, but we absolutely need the two things we're producting to have the same number of fields. I guess I'm kinda thinking "it looks like it should work if we use ApplicativeB and TraversableB to do the work, and also require a DistributiveB constraint just to ensure the shapes are right". But that feels super inelegant.

[endgame]

Ah yes. It's probably important to preserve Eq and Ord, because I can see people wanting to maintain Sets of Symbolic values etc. And since it's easy to wrap current Symbolic to get free Functor (Coyoneda) and Applicative (free:Control.Applicative.Free.Ap) instances but the reverse is not true (i.e., it's hard to come up with Eq/Ord for this alternate Symbolic, I think we leave them the way they are.

Why am I interested in something with a Functor instance? Because it is required to do anything interesting with a DistributiveB. Examples:

bdistribute :: (DistributiveB b, Functor f) => f (b g) -> b (Compose f g)
bdistribute' :: (DistributiveB b, Functor f) => b f -> f (b Identity)

Any HKD record type where every field is wrapped by the v parameter can have a DistributiveB instance, and is anyclass-derivable. This is where I was getting the Symbolic (Record Identity) from — you can do this with Hedgehog as it exists today, and then use liftCoyoneda and bdistribute' to get a Record (Coyoneda Symbolic) (which you can lowerCoyoneda out of when everything's Concrete).

---

I think that if we want to change hedgehog, the next question is: in what way? I think the objective should be to use output v in the definition of Command and Callback for consistency with input v, and documenting Var as merely a convenient type constructor for when you want to wrap a single value and make the types line up.

There are two ways to do this that I can see:

1. Make output a DistributiveB and find a way to make Symbolic a Functor without sacrificing Ord and Eq on Symbolic a. Then you have a really nice symmetry between TraversableB input and DistributiveB output and you don't really have to change how Symbolic values are substituted: you can generate a Symbolic (output Identity) and bdistribute' it to make an output Symbolic and keep most of the other hedgehog machinery the same.

2. Attempt to generate an output Symbolic directly. As you observe, this requires bpure to make an output Proxy followed by a btraverseC to turn it into an m (output Symbolic). So then you require at least ApplicativeB output and TraversableB output. I'm not sure you need DistributiveB then, because you should be able to do the necessary zipping with bprod.

I think having the output v is really appealing independent of which option we choose, but I think option 1 is much more elegant. But I don't like giving up Eq and Ord on Symbolic a values — is there a trick that I've missed?

[endgame]

(Aside: It would also be nice to have instance Applicative Concrete, so that you don't have to go Concrete ~> Identity before you lower out of a free Applicative.)

[ChickenProp]

I think that if we want to change hedgehog, the next question is: in what way? I think the objective should be to use output v in the definition of Command and Callback for consistency with input v, and documenting Var as merely a convenient type constructor for when you want to wrap a single value and make the types line up.

I think I agree with this, though in my case it's mostly for the specific reason of "I want to return multiple vars at once" rather than consistency.

(I'm trying out the Coyoneda thing now, the type parameters are the wrong way around to do deriving anyclass (FunctorB, TraversableB). Looks like I can make it work anyway, will report back next week how ergonomic it is when it's all plumbed together.)

I'm not sure you need DistributiveB then, because you should be able to do the necessary zipping with bprod.

So the reason I thought bprod doesn't work by itself is because if you have

newtype ListB a f = ListB [f a]

then you might end up with bprod (ListB [Symbolic $ Name 1]) (ListB [Concrete "foo", Concrete "bar"]). Then we'd be dropping one of the Concretes. Or vice versa, drop one of the Symbolics if there are more of those.

But I'm actually not entirely sure ListB can have a lawful instance of TraversableB. I said before that I think you could write the instance, but I didn't mention lawfulness. If it wouldn't be lawful then maybe there's no problem.

[endgame]

I think I agree with this, though in my case it's mostly for the specific reason of "I want to return multiple vars at once" rather than consistency.

Sure. I take consistency and symmetry as a smell that the design is pointing the right way, and the current way output is used in Command and Update closes off ergonomic ways of doing multiple values, which is what we all actually want.

(I'm trying out the Coyoneda thing now, the type parameters are the wrong way around to do deriving anyclass (FunctorB, TraversableB). Looks like I can make it work anyway, will report back next week how ergonomic it is when it's all plumbed together.)

I believe this is just a limitation in the generics-based deriving code, but nothing fundamental:

-- Dunno if this is the best name
traverseCoyoneda :: Functor e => (forall x. f x -> e (g x)) -> Coyoneda f a -> e (Coyoneda g a)
traverseCoyoneda f (Coyoneda g fb) = Coyoneda g <$> f fb

data X f = X
  { x1 :: f Int,
    x2 :: Coyoneda f Char,
    x3 :: Bool
  }

instance FunctorB X where
  bmap :: (forall a. f a -> g a) -> X f -> X g
  bmap f x = X {x1 = f $ x1 x, x2 = hoistCoyoneda f $ x2 x, x3 = x3 x}

instance TraversableB X where
  btraverse :: Applicative e => (forall a. f a -> e (g a)) -> X f -> e (X g)
  btraverse f x = do
    x1' <- f $ x1 x
    x2' <- traverseCoyoneda f $ x2 x
    pure X {x1 = x1', x2 = x2', x3 = x3 x}

Re: bprod truncating the longer list with your ListB type: this seems lawful to me, like how the ZipList Applicative and zipWith functions do this. Is it actually the case that we need to pair off a ListB a Symbolic with a ListB a Concrete, or would this transformation actually be done via btraverse?

Re: Can ListB have a lawful instance of TraversableB? I sat down and thought about the laws for TraversableB and while I didn't formally prove them it seems to me that instance TraversableB (ListB a) will obey the laws unless one specifically sets out to permute/drop list elements or do other silly things. btraverse f (ListB fas) = ListB <$> traverse f fas falls out of the type tetris and I assume that's what the anyclass-derived instance would be doing too.

[ChickenProp]

Looks like it wasn't just about automatic deriving, there are also issues with Show. (We need Show (input Symbolic), but there's no instance Show (Coyoneda Symbolic a) because Symbolic isn't a Functor. But nothing unworkable. I ended up just defining my own version of it with flipped type vars.

-- | This allows us to deconstruct the return value from an @exec@ function and
-- store it in state.
--
-- If an @exec@ function returns @(a, b)@, we might want to put the @a@ and @b@
-- in state separately. But we also need to put them in `Symbolic` state, where
-- what we have is @val :: `Symbolic` (a, b)@. Since `Symbolic` isn't a functor,
-- we can't really do that. What we can do is store @(fst, val)@ and
-- @(snd, val)@, and this is essentially that.
--
-- This is a flipped version of @Coyoneda@ from
-- https://hackage.haskell.org/package/kan-extensions-5.2.5/docs/Data-Functor-Coyoneda.html.
-- Flipping the type variables makes it suitable for things using it to
-- auto-derive `FunctorB` and `TraversableB`. We also add a @Show b@ constraint,
-- because the `Show` instance for @Coyoneda f a@ requires @Functor f@, which
-- we still don't have for `Symbolic`.
data FVar a v where
  FVar :: Show b => (b -> a) -> v b -> FVar a v

instance (Eq1 v, Eq a) => Eq (FVar a v) where
  (FVar f1 a1) == (FVar f2 a2) = liftEq (\x y -> f1 x == f2 y) a1 a2

instance (Show1 v, Show a) => Show (FVar a v) where
  showsPrec prec (FVar _ x) =
    showParen (prec > 10) $ showString "FVar _ " . showsPrec1 11 x

instance FunctorB (FVar a) where
  bmap f (FVar g x) = FVar g (f x)

instance TraversableB (FVar a) where
  btraverse f (FVar g x) = FVar g <$> f x

-- | Turn a `Var` into an `FVar`.
fvar :: Show b => (b -> a) -> Var b v -> FVar a v
fvar f (Var x) = FVar f x

-- | Pull a `Concrete` value out of an `FVar`.
--
-- There's a more general but less convenient form of this, which has type
-- @`Functor` v => `FVar` a v -> v a@.
fconcrete :: FVar a Concrete -> a
fconcrete (FVar f (Concrete x)) = f x

I still think that actually returning multiple Vars would be nicer, in particular it would improve the show instance. (Right now we'll see something like theA :: FVar _ (someA, someB), theB :: FVar _ (someA, someB), where theA :: Var someA, theB :: Var someB would be better.) But I think this does get a lot of the value.

Is it actually the case that we need to pair off a ListB a Symbolic with a ListB a Concrete, or would this transformation actually be done via btraverse?

I think we do need to pair them off. Right now we have function

insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment

and we need some analog of that with multiple vars.

[endgame]

Good digging. I made a new issue to discuss free wrappers, so we can focus on the "multiple return values" problem here. Actually generating an output v seems pretty hard. I was able to write this variant of brecompose, but I don't know how you'd know which a to use for your function argument, or how to assemble the b (Compose ((->) a) f):

brecompose' :: FunctorB b => b (Compose ((->) a) f) -> a -> b f
brecompose' b a = bmap (($ a) . getCompose) b

Perhaps it is a red herring? Generating a v (output identity) and using bdistribute also seems like a dead end, because v is not necessarily a Functor and we can't force people into FVar-land, and baking the free Functor/Applicative machinery into Symbolic would make us give up Eq and Ord instances...

Trade-offs, trade-offs. Which ones to pick?