Possible Enhancement for 'Clash.Sized.Vector'

[paddytheplaster]

Happy New Year.

I noticed that Vec n a extends Ord as follows:

instance (KnownNat n, Ord a) => Ord (Vec n a) where
  compare x y = foldr f EQ $ zipWith compare x y
    where f EQ   keepGoing = keepGoing
          f done _         = done

Unless I'm missing something, this is a pity because f is associative, so the following should also be possible

instance (KnownNat n, Ord a) => Ord (Vec n a) where
  compare = compare_vec

compare_vec
    :: forall (n :: Nat)  .  (KnownNat n,Ord a) => Vec n a -> Vec n a -> Ordering
compare_vec a b
    = case (compareSNat $ SNat @n d0,compareSNat d1 $ SNat @n) of
          (SNatLE,_) -> EQ
          (_,SNatLE) -> compare_vec' @(n-1) a b

compare_vec'
    :: forall (n :: Nat) a
    .  (Ord a)
    => Vec (n+1) a
    -> Vec (n+1) a
    -> Ordering
compare_vec' a b = fold cmp $ zipWith compare a b
    where cmp EQ b  = b
          cmp a  _  = a

Regards,

Paddy

[martijnbastiaan]

Happy new year!

Maybe I'm stating the obvious, but this would trade simulation performance for hardware efficiency (which is a good trade-off IMO), at least naively. Maybe the synthesis tools already rearrange this to a tree structure?

[gergoerdi]

Your cmp function in compare_vec' is just (<>) because the semigroup instance of Ordering does exactly this lexicographical ordering. This means you are folding along the semigroup operator, which is nice because it makes it obvious that the association doesn't matter.

However, I don't understand the reason behind writing compare_vec in this strange style. Is there any benefit compared to using GADT pattern matching to refine n in the two branches?

compare_vec :: (KnownNat n,Ord a) => Vec n a -> Vec n a -> Ordering
compare_vec Nil Nil = EQ
compare_vec xs@Cons{} ys@Cons{} = fold (<>) $ zipWith compare xs ys

In fact, we could have a generic "monoid folder":

foldM :: (KnownNat n, Monoid a) => Vec n a -> a
foldM Nil = mempty
foldM xs@Cons{} = fold (<>) xs

allowing

compare_vec xs ys = foldM $ zipWith compare xs ys)

[paddytheplaster]

Happy new year!

Maybe I'm stating the obvious, but this would trade simulation performance for hardware efficiency (which is a good trade-off IMO), at least naively. Maybe the synthesis tools already rearrange this to a tree structure?

Thanks. first I'd prefer hardware efficiency. Second, why rely on the hardware tool if it's possible to avoid it. (I consider not using fold a missed opportunity.)

[paddytheplaster]

Your cmp function in compare_vec' is just (<>) because the semigroup instance of Ordering does exactly this lexicographical ordering. This means you are folding along the semigroup operator, which is nice because it makes it obvious that the association doesn't matter.

However, I don't understand the reason behind writing compare_vec in this strange style. Is there any benefit compared to using GADT pattern matching to refine n in the two branches?

compare_vec :: (KnownNat n,Ord a) => Vec n a -> Vec n a -> Ordering
compare_vec Nil Nil = EQ
compare_vec xs@Cons{} ys@Cons{} = fold (<>) $ zipWith compare xs ys

In fact, we could have a generic "monoid folder":

foldM :: (KnownNat n, Monoid a) => Vec n a -> a
foldM Nil = mempty
foldM xs@Cons{} = fold (<>) xs

allowing

compare_vec xs ys = foldM $ zipWith compare xs ys)

Thanks. The GADT pattern matching solution is definitely better. I hadn't thought of it. The 'Monoid' folder makes sense.

[martijnbastiaan]

I'm not sure about the name foldM, which I'd expect to be foldM ::: Monad m => (b -> a -> m b) -> b -> Vec n a -> m b but otherwise @gergoerdi's implementation looks like a nice addition to clash-prelude (both foldM and compare_vec).

Second, why rely on the hardware tool if it's possible to avoid it.

Well if it turns out all major HDL tools create optimal hardware anyway, I don't think we should sacrifice any simulation performance. Clash's simulation performance isn't that great to begin with.

[christiaanb]

Closing since we use a tree-based fold these days: https://github.com/clash-lang/clash-compiler/blob/133c73aa8b89e2ccc3ca40b3a36248b766e3cca2/clash-prelude/src/Clash/Sized/Vector.hs#L292-L294

[DigitalBrains1]

I think you've made a mistake, Christiaan. Eq is tree-based, but the issue is about Ord (just below in the code, actually). That's expressed in foldr, although I'm hoping that synthesis tools would see the opportunity for optimization.

[gergoerdi]

I'm not sure about the name foldM, which I'd expect to be foldM ::: Monad m => (b -> a -> m b) -> b -> Vec n a -> m b but otherwise @gergoerdi's implementation looks like a nice addition to clash-prelude (both foldM and compare_vec).

Yeah foldM was a brain-fart on my end, it should be called mfold to be consistent with mappend/mconcat.