Pushing applicative effects in?

[gergoerdi]

It seems pulling effects out in Barbies is a trivial matter of btraverse and related functions. But how do I do the opposite, and push effects inwards?

My full question is at https://stackoverflow.com/questions/60900998/pushing-applicative-effects-into-hkd-fields-with-barbies-or-higgledy but basically I am looking for the dual of Higgledy's construct function; Higgledy has these:

construct :: HKD structure f -> f structure
deconstruct :: structure -> HKD structure f

What I'm looking for is:

nstruct :: (Applicative f, _) => f structure -> HKD structure f

or, in Barbies parlance,

bdistribute :: (ApplicativeB b, Applicative f, _) => f (b g) -> b (Compose f g)

(yes, I am leaving the door open that bdistribute and nstruct might have more constraints)

[gergoerdi]

Here's how to implement bdistribute if we only had shape:

shape :: (ApplicativeB b) => b ((->) (b Identity))
shape = _

bdistribute :: (Functor f, Applicative g, ApplicativeB b, TraversableB b) => f (b g) -> b (Compose f g)
bdistribute x = bmap (\f -> Compose $ fmap f . bsequence' <$> x) shape

[jcpetruzza]

Interesting question! I suspect you can't define a function such as shape, requiring only ApplicativeB. Intuitively, the problem is sum-types. E.g.:

data MT f = NoT | SomeT (f Int)

You can define an ApplicativeB MT, but assuming shape @MT was defined, what should the behaviour be if you passed a NoT to the function in the SomeT? (hope this makes sense)

What we could do here instead is try to define a notion analogous to that of distributive functors. Something like:

class DistributiveB b where
  bdistribute :: Distributive f => f (b g) -> b (Compose f g)

I don't currently have good intuitions about what things are DistributiveB, but the docs of Distributive say:

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.

So let's go with that! This looks very similar to what we were calling ProductB in version 1.x and that later got replaced by ApplicativeB: things that are essentially records with all their fields covered by an f. Let's try this out:

data Person f
  = Person
       { name :: f Text
       , age:: f Int
       }

instance DistributiveB Person where
  bdistribute fbg
    = Person {
        name = Compose $ fmap name fbg
      , age = Compose $ fmap age fbg
      }

aging n = [Person (pure n) (pure i) | i <- [0..]]

> take 10 $ map runIdentity $ getCompose $ age $ bdistribute $ aging "Daniel"                                
> [0,1,2,3,4,5,6,7,8,9]

What do you think?

[gergoerdi]

Should bdistribute be the primitive in the typeclass, or shape? shape comes with a nice law which doesn't even need an ApplicativeB instance on b:

forall (x :: b Identity). x = bmap (\f -> Identity (f x)) shape

[gergoerdi]

One argument for shape: I think the above law succeeds in ruling out shape @MT, since whichever constructor you pick in shape, that is what you will get out of bmap _ shape, so the above law can easily be disproven by picking the other constructor for x.

[jcpetruzza]

I think you can have valid instances of DistributiveB where you wouldn't be able to implement shape. Consider this example:

data T k f
  = T { unT :: k -> f Int }

instance DistributiveB (T k) where
  bdistribute fbg
    = T (Compose <$> distribute (fmap unT fbg))

Here we are using the instance Distributive ((->) e). Any implementation of shape @(T k) would be unlawful, right?

Unrelated, if one were to write a class that provides something similar to shape, maybe returning a lens for each field, instead of a getter, could be desirable?

Edit: midair-collission, just saw your PR :slightly_smiling_face:

[gergoerdi]

I like your example! If more types can be DistributiveB than Shape, then I guess we should go with the former after all (and my real use case only requires bdistribute not shape, so there's no loss). So what would be the defining law of DistributiveB?

Good point about putting lenses instead of getters into shape, but I guess that doesn't matter if we're going to go with DistributiveB after all.

[gergoerdi]

But wait, why couldn't T k have a shape?

data T k f
  = T { unT :: k -> f Int }

instance Shape (T k) where
  shape = T{ unT = \k -> \b -> Identity $ unT b k }

[jcpetruzza]

Oh, you are completely right! And it turns out that one can show bdistribute and shape to be equivalent after all. You've already given one direction. For the other, let's define shape using bdistribute:

-- Analogous to `bsequence'`
bdistribute' :: (DistributiveB b, Functor f) => f (b Identity) -> b f
bdistribute' = bmap (fmap runIdentity . getCompose) . bdistribute

shape :: DistributiveB b => b ((->) (b Identity))
shape = bdistribute' id

[gergoerdi]

I've gone deeper into "I have no idea what I'm doing" territory and pushed a version that works for deriving Shape for your T example.

However, it is very ad-hoc, I am basically playing generic instance whack-a-mole. Ideally someone who has experience with the generics machinery should look at it.

[gergoerdi]

In particular, Shape for InfRec, CompositeRecord and ParB should be derivable but isn't yet.

[gergoerdi]

I've rewritten all of it to DistributiveB and oh my god it is so much cleaner. I think #27 is now good for merging.

[gergoerdi]

Unrelated, if one were to write a class that provides something similar to shape, maybe returning a lens for each field, instead of a getter, could be desirable?

I am now less sure this is possible. Is Lens' s (for some fixed s) a distributive functor? I don't think it's even a functor, since you can only map isomorphisms, not unidirectional functions over it.

[gergoerdi]

Let's go back to the example of T:

data T k f
  = T { unT :: k -> f Int }

If we wanted bshape to return a skeleton of lenses, not getters, it would need to look like this:

-- Otherwise we can't partially apply the type synonym `Lens'`
newtype LensFrom s a = MkLensFrom{ getLensFrom :: Lens' s a }

bshapeOfT :: T k (LensFrom (T k Identity))
bshapeOfT = T{ unT = \k -> MkLensFrom $ lens (runIdentity . ($k) . unT) (\t x -> t{ unT = _ }) }

But here, what exactly should be the new value of unT? The best we can do is const (Identity x), but that doesn't really expose all possible degrees of freedom (unlike the getter, which really will give you the right Int for your choice of k). It also restricts the universe of functors you can use in fields to distributive applicative functors (note that the const we use here is the pure of (k ->)).

I think fundamentally what's going on here is that what we want to put in unT is a getter and a setter both indexed by k. For a pure getter, since k -> Identity Int is isomorphic with Identity (k -> Int) it doesn't matter that we end up with the former. But for a full lens, there's a difference between k -> Lens s a (which we'd get with this approach) and Lens s (k -> a) (which we would want).

[jcpetruzza]

Sorry for the delay in coming back to you and thanks for the effort you've put so far in the PR, it's looking very good!

Should bdistribute be the primitive in the typeclass, or shape? shape comes with a nice law which doesn't even need an ApplicativeB instance on b:

forall (x :: b Identity). x = bmap (\f -> Identity (f x)) shape

This question sent me through a bit of rabbit-hole (of which I haven't yet fully climbed out, as I'm still trying to understand all this better), but my current thinking is that this law may not enough be enough to prove the "Distributive laws" that come from "flipping the arrows" in the Traversable laws.

Let's consider the "first-order" Distributive class. One could make the following method the primitive of the class:

decompose :: Distributive g => (a -> g b) -> g (a -> b)

  -- intuition: decompose = distribute @((->) a)

And then, the Distributive laws can be proven, I think, from these two laws:

recompose . decompose = id
decompose . recompose = id

where

recompose :: Functor f => f (a -> b) -> (a -> f b)
recompose fab = \a -> fmap ($ a) fab

In the PR you propose as class law:

bmap (Identity . ($ b)) bshape = b

But if I'm reading this correctly, it is a specialization of the first of the two laws above. I expect without the other one, it should be possible to have an instance whose bdistribute violates the composition law, which for Distribute is:

  fmap Compose . distribute . fmap distribute  =  distribute . Compose

If what I'm saying is correct, It should be possible to come with an example of this, but I haven't tried it so far.

[gergoerdi]

FWIW I'd call decompose tabulate instead because that gives me some intuition for what it does. Alas, tabulate seems to be already taken.

(I am not going to repeat my joke from the original bug report about how it shoudl be called compose and mpose...)

[gergoerdi]

Is it possible that the second law, that is:

decompose . recompose = id

is not really adding any new constraints? recompose on its own is a very weak operation (it's no coincidence it only needs Functor f).

[gergoerdi]

So the conclusion so far is that you're fine with the code of the patch, but the documentation should be changed to contain the decompose . recompose and recompose . decompose laws? Do you want to make this change or should i?

[jcpetruzza]

Is it possible that the second law [...] is not really adding any new constraints?

Good question! So, the problem is whether one can write a Distributive instance such that

recompose . decompose = id
decompose . recompose /= id

It turns out one such example would be:

newtype Sel r a = Sel { runSel :: (a -> r) -> a }

instance Functor (Sel r) where
  fmap h s = Sel (\br -> h (runSel s (br . h)))

instance Distributive (Sel r) where
  decompose h = Sel (\abr -> (\a -> runSel (h a) (\b -> abr (const b))))

This wasn't obvious to me at all. I found the example on this stackoverflow discussion, which actually discusses the same things we are discussings here.

Btw, I started writing some notes with all the details about the things I'm claiming in this thread, because future me will most likely forget them all :slightly_smiling_face:

[jcpetruzza]

So, yeah, I think we should probably state the laws in terms of decompose. I'm not particularly attached to the name, I've just been using it in my notes so far and got used to it, I guess. tabulate would be fine as well, it's a pity that it's taken (also not sure how to call it's inverse).

[gergoerdi]

So, it seems the only missing piece is documenting the laws, and you are on top of it; do you need anything more from me for #27?

[gergoerdi]

That Stack Overflow question is a really good find!

[jcpetruzza]

Sorry, was a little busy during the week and couldn't look into this earlier. I'll check the docs of the laws of DistributiveB, so we can get #27 merged

[gergoerdi]

I wonder if it would make sense to give a name specifically for bdistribute' . fmap bcover, because I foresee that being 95% of my use cases for DistributiveB.

[gergoerdi]

FYI I have made a pull request for barbies-th to generate DistributiveB instances.

[jcpetruzza]

I wonder if it would make sense to give a name specifically for bdistribute' . fmap bcover, because I foresee that being 95% of my use cases for DistributiveB.

Do you have a name in mind? I can only think of bdiscover, which is not intuitive but at least is mnemonic :slightly_smiling_face:

Out of curiosity, what's your use case?

[gergoerdi]

My use case is building hardware in Clash. Yesterday, I've sent the below email to the Clash mailing list which describes my intended use for this new Barbies feature:

Barbie: the ultimate Bundle

I find myself often in a situation where I want to make a circuit's parameters use some record type to get to that sweet sweet syntax sugar of record fields (especially RecordWildCards!).

Bundles of signals

For example, suppose I have definitions like this:

data CPUIn dom = CPUIn
    { romRead :: Signal dom Word8
    , ramRead :: Signal dom Word8
    }

data CPUOut dom = CPUOut
    { romAddr :: Signal dom Word16
    , ramAddr :: Signal dom Word16
    , ramWrite :: Signal dom (Maybe Word8)
    , outPort :: Signal dom (Maybe Word8)
    }

cpu :: (HiddenClockResetEnable dom) => CPUIn dom -> CPUOut dom

Then, I can write some board containing a CPU and some memory in a very straightforward way, connecting signals to record fields directly:

board :: (HiddenClockResetEnable dom) => Signal dom (Maybe Word8)
board = outPort
  where
    CPUOut{..} = cpu CPUIn{..}

    romRead = unpack <$> romFilePow2 "rom.bin" romAddr
    ramRead = blockRam1 NoClearOnReset (SNat @30_000) 0 ramAddr ramWrite'
    ramWrite' = packWrite <$> ramAddr <*> ramWrite

Signals of bundles

At this point, I realize that the most straightforward way to implement cpu is as a Mealy-state machine:

cpu = mealyState cpuPeriod initCPUState

cpuPeriod :: CPUIn? -> State CPUState CPUOut?

And here we're busted because CPUIn and CPUOut are bundles of signals. Instead, we could have a signal of bundles:

data CPUIn = CPUIn
    { romRead :: Word8
    , ramRead :: Word8
    }

data CPUOut = CPUOut
    { romAddr :: Word16
    , ramAddr :: Word16
    , ramWrite :: Maybe Word8
    , outPort :: Maybe Word8
    }

which makes cpuPeriod easy to write:

cpuPeriod :: CPUIn -> State CPUState CPUOut
cpuPeriod CPUIn{..} = do
    ...
    return CPUOut{..}

but now our board looks like this:

board = outPort <$> cpuOut
  where
    cpuOut = cpu cpuIn

    cpuIn = CPUIn <$> romRead <*> ramRead

    romRead = unpack <$> romFilePow2 "rom.bin" (romAddr <$> cpuOut)
    ramRead = blockRam1 NoClearOnReset (SNat @30_000) 0 (ramAddr <$> cpuOut) ramWrite'
    ramWrite' = packWrite <$> (ramAddr <$> cpuOut) <*> (ramWrite <$> cpuOut)

Here, the definition of cpuIn is horrible because all connection to the field names are lost. We can improve that using ApplicativeDo:

cpuIn = do
    romRead <- romRead
    ramRead <- ramRead
    pure CPUIn{..}

but we don't have a similar way of accessing cpuOut's fields.

Or do we?

Making CPUIn and CPUOut higher-kinded

Suppose we make CPUIn and CPUOut into higher-kinded data types:

data CPUIn f = CPUIn
    { romRead :: f Word8
    , ramRead :: f Word8
    }

data CPUOut f = CPUOut
    { romAddr :: f Word16
    , ramAddr :: f Word16
    , ramWrite :: f (Maybe Word8)
    , outPort :: f (Maybe Word8)
    }

Now we can use CPUIn Identity inside cpuPeriod, and CPUIn (Signal dom) everywhere else:

cpu :: (HiddenClockResetEnable dom) => CPUIn (Signal dom) -> CPUOut (Signal dom)
cpu = to . mealyState cpuPeriod initCPUState . from

cpuPeriod :: CPUIn Identity -> State CPUState (CPUOut Identity)
cpuPeriod CPUIn{..} = do
    ...
    return CPUOut{..}

board :: (HiddenClockResetEnable dom) => Signal dom (Maybe Word8)
board = outPort
  where
    CPUOut{..} = cpu CPUIn{..}

    romRead = unpack <$> romFilePow2 "rom.bin" romAddr
    ramRead = blockRam1 NoClearOnReset (SNat @30_000) 0 ramAddr ramWrite'
    ramWrite' = packWrite <$> ramAddr <*> ramWrite

This is now very nice, but two problems remain:

• Inside cpuPeriod, all fields of CPUIn and CPUOut are wrapped in an Identity.
• Writing to and from is tedious. Here's their implementation for these specific CPUIn and CPUOut definitions:

from :: (Functor f) => CPUIn f -> f (CPUIn Identity)
from CPUIn{..} = CPUIn <$> romRead <*> ramRead

to :: (Functor f) => f (CPUOut Identity) -> CPUOut f
to fx = CPUOut
    { romAddr = romAddr <$> fx 
    , ramAddr = ramAddr <$> fx
    , ramWrite = ramWrite <$> fx
    , outPort = outPort <$> fx 
    }

Enter Barbies

The HKD library Barbies solves these problems:

• It has a concept of bare HKDs, where fields are not wrapped in any functor (not even Identity). So we can arrange for CPUIn Bare Identity to have bona-fide Word8 fields, while still having the type CPUIn Covered (Signal dom) where every field is a signal.

• It provides the TraversableB typeclass to implement our from function generically.

• Its companion package barbies-th uses Template Haskell to generate all required typeclasses

You might notice that this still leaves us with having to write to. Well, I'm glad you asked! I've been working with Daniel Gorín on adding a new DistributiveB typeclass to barbies, which gives us to. The patch for barbies-th is also on its way.

The glorious end result

declareBareB [d|
data CPUIn = CPUIn
    { romRead :: Word8
    , ramRead :: Word8
    } |]

declareBareB [d|
data CPUOut = CPUOut
    { romAddr :: Word16
    , ramAddr :: Word16
    , ramWrite :: Maybe Word8
    , outPort :: Maybe Word8
    } |]

cpu :: (HiddenClockResetEnable dom) => CPUIn Covered (Signal dom) -> CPUOut Covered (Signal dom)
cpu = bdistribute' . fmap bcover . mealyState cpuPeriod initCPUState . fmap bstrip . bsequence'

cpuPeriod :: CPUIn Bare Identity -> State CPUState (CPUOut Bare Identity)
cpuPeriod CPUIn{..} = do
    ...
    return CPUOut{..}

board :: (HiddenClockResetEnable dom) => Signal dom (Maybe Word8)
board = outPort
  where
    CPUOut{..} = cpu CPUIn{..}

    romRead = unpack <$> romFilePow2 "rom.bin" romAddr
    ramRead = blockRam1 NoClearOnReset (SNat @30_000) 0 ramAddr ramWrite'
    ramWrite' = packWrite <$> ramAddr <*> ramWrite

Let me know what you think.

Bye, G

[gergoerdi]

I am currently playing around with these ideas in my Brainfuck computer, see the CPU part here and the encompassing board here. Once I am convinced that this is the way to go, I will describe and incorporate this technique in a Clash book I am working on.

Perhaps of interest, the former file also uses Barbies heavily to assemble the CPUOut piecewise, I've written about this technique previously on SO.

[gergoerdi]

Do you have a name in mind? I can only think of bdiscover, which is not intuitive but at least is mnemonic

I think what I'm going to do is put bbundle = bdistribute' . fmap cover and bunbundle = fmap bstrip . bsequence' in https://github.com/gergoerdi/retroclash-lib and not pollute the Barbies namespace further. Maybe even add an orphan Bundle instance for Barbie.

[gergoerdi]

Should I close this issue, or do you plan to only when a new Barbies version is released with this new feature?

[jcpetruzza]

Just made a new release. Thanks for all your work!