Laziness in prod3C

Clash Help
1

While writing some code that uses clash-protocols, I implemented prod3C in the expected way:

prod3C
  :: Circuit a b
  -> Circuit c d
  -> Circuit e f
  -> Circuit (a, c, e) (b, d, f)
prod3C (Circuit x) (Circuit y) (Circuit z) =
  Circuit
  ( \((xFwd, yFwd, zFwd), (xBwd, yBwd, zBwd)) ->
    let
      (xBwd', xFwd') = x (xFwd, xBwd)
      (yBwd', yFwd') = y (yFwd, yBwd)
      (zBwd', zFwd') = z (zFwd, zBwd)
    in ((xBwd', yBwd', zBwd'), (xFwd', yFwd', zFwd'))
  )

But this causes my hedgehog tests to hang. To fix this it was enough to make the pattern irrefutable by adding the tilde ~:

  :: Circuit a b
  -> Circuit c d
  -> Circuit e f
  -> Circuit (a, c, e) (b, d, f)
prod3C (Circuit x) (Circuit y) (Circuit z) =
  Circuit
  ( \ ~((xFwd, yFwd, zFwd), (xBwd, yBwd, zBwd)) ->
    let
      (xBwd', xFwd') = x (xFwd, xBwd)
      (yBwd', yFwd') = y (yFwd, yBwd)
      (zBwd', zFwd') = z (zFwd, zBwd)
    in ((xBwd', yBwd', zBwd'), (xFwd', yFwd', zFwd'))
  )

(I can’t post the rest of the code but plan to find a small reproducible example next week that I can post here).
Is there an obvious reason why I need the irrefutable pattern in prod3C while it’s not present in prod2C? Does it imply a problem elsewhere?

2

In your first example without ~ you strictly pattern match on (xBwd, yBwd, zBwd)) which requires the spine of that tuple. Haskell has to evaluate Bwd (b, d, f) to match the pattern. However, it’s common practice that the backward channel of a Protocol depends on the forward, if Bwd (b, d, f) depends on Fwd (b, d, f) we get a deadlock.

The ~ operator makes the pattern match lazy, so we don’t require the spine of Bwd (b, d, f) to match on your lambda.

3

Is there an obvious reason why I need the irrefutable pattern in prod3C while it’s not present in prod2C? Does it imply a problem elsewhere?

We should add the ~ to prod2C. It’s also something the circuit-notation plugin does:

prod3C ab cd ef = circuit $ \(a, c, e) -> do
  b <- ab -< a
  d <- cd -< c
  f <- ef -< e
  idC -< (b, d, f)

~

TaggedCircuit
  (\ (~(TaggedBundle (a_Fwd, c_Fwd,
                      e_Fwd)) `(,)` ~(TaggedBundle (b_Bwd, d_Bwd, f_Bwd)))
     -> let
          a_Bwd `(,)` b_Fwd = taggedCircuit ab (a_Fwd `(,)` b_Bwd)
          c_Bwd `(,)` d_Fwd = taggedCircuit cd (c_Fwd `(,)` d_Bwd)
          e_Bwd `(,)` f_Fwd = taggedCircuit ef (e_Fwd `(,)` f_Bwd)
        in
          TaggedBundle (a_Bwd, c_Bwd, e_Bwd)
            `(,)` TaggedBundle (b_Fwd, d_Fwd, f_Fwd))
4

I’ve opened an issue: `prod2C` is too strict · Issue #149 · clash-lang/clash-protocols · GitHub.

5

I see, that makes sense. It turns out my tests did not pass - that must be because I need the inner tuples to be matched with ~ also.

Thank you both!

6

Thanks for making us aware of this bug!

1 Like
7

The fix is in main now.