Feature offer: n-ary product type

[gergoerdi]

This is the dual of a feature request: I am offering the below module for consideration into inclusion in clash-prelude. It is not in the form of a pull request because I'd like to know first if this is something you guys would want.

It is an n-ary product type: Product [t1, t2, t3] is isomorphic to the tuple type (t1, t2, t3). My motivation for it is using it for a product-of-sums (sic!) ripple counter as can be seen here: this, in turn, allows me to write a VGA signal generator as simply as

    horiz :-: vert :-: _ = counterMul $ Proxy
        @'[ [w, preH, pulseH, postH]
          , [h, preV, pulseV, postV]
          ]

    vgaX :-: _ :-: (toSync (Proxy @polH) -> vgaHSync) :-: _ = horiz
    vgaY :-: _ :-: (toSync (Proxy @polV) -> vgaVSync) :-: _ = vert

giving me vgaX :: Signal _ (Maybe (Index w)) and vgaHSync :: Signal _ Bit, etc. from a type-level VGA mode specification like

vga640x480at60 :: SVGATimings ('VGATimings
    (FromHz 25_175_000)
    ('VGATiming Negative 640 16 96 48)
    ('VGATiming Negative 480 11  2 31))
vga640x480at60 = SVGATimings

(see the full VGA implementation here)

So anyway, is the below code something that would be a good idea to add to clash-prelude?

{-# LANGUAGE GADTs, StandaloneDeriving, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies, FlexibleInstances #-}
module Clash.Data.Product where

import Clash.Prelude
import Control.DeepSeq

data Product (ts :: [*]) where
    PNil :: Product '[]
    (:-:) :: a -> Product ts -> Product (a : ts)
infixr 5 :-:

instance Show (Product '[]) where show PNil = "PNil"
deriving instance (Show t, Show (Product ts)) => Show (Product (t : ts))

instance Eq (Product '[]) where _ == _ = True
deriving instance (Eq t, Eq (Product ts)) => Eq (Product (t : ts))

instance Ord (Product '[]) where compare _ _ = EQ
deriving instance (Ord t, Ord (Product ts)) => Ord (Product (t : ts))

instance NFData (Product '[]) where
    rnf PNil = ()

instance (NFData t, NFData (Product ts)) => NFData (Product (t:ts)) where
    rnf (x :-: xs) = rnf x `seq` rnf xs

headP :: Product (t : ts) -> t
headP (x :-: xs) = x

tailP :: Product (t : ts) -> Product ts
tailP (x :-: xs) = xs

data SLength :: [k] -> * where
    SLenNil :: SLength '[]
    SLenCons :: SLength xs -> SLength (x : xs)

class KnownLength (xs :: [k]) where
    knownLength :: SLength xs

instance KnownLength '[] where knownLength = SLenNil
instance (KnownLength xs) => KnownLength (x : xs) where knownLength = SLenCons knownLength

type family ToSignals (dom :: Domain) (ts :: [*]) = (r :: [*]) | r -> ts dom where
    ToSignals dom '[] = dom ::: '[]
    ToSignals dom (t : ts) = Signal dom t : ToSignals dom ts

instance (KnownLength ts) => Bundle (Product ts) where
    type Unbundled dom (Product ts) = Product (ToSignals dom ts)

    bundle = go knownLength
      where
        go :: forall dom us. SLength us -> Product (ToSignals dom us) -> Signal dom (Product us)
        go SLenNil PNil = pure PNil
        go (SLenCons n) (x :-: xs) = (:-:) <$> x <*> go n xs

    unbundle = go knownLength
      where
        go :: forall dom us. SLength us -> Signal dom (Product us) -> Product (ToSignals dom us)
        go SLenNil _ = PNil
        go (SLenCons n) xs = (headP <$> xs) :-: (go n $ tailP <$> xs)

[martijnbastiaan]

I don't understand what the advantages are over using tuples. Could you expand on that? Thanks!

[christiaanb]

I guess it allows things like mapping type-level functions over all the arguments. So you could eg specify that you increase the number of elements of every Vector in the product by one.

So e.g.

addOne :: a -> Product [*] -> Product (Map AddOneSym [*])
addOne = leftAsAnExercise

type family AddOne a where
  AddOne (Vec n a) = Vec (n+1) a
  AddOne ty = ty

doAddOne :: Product [Vec 3 Int, Vec 5 Int] -> Product [Vec 4 Int, Vec 6 Int]
doAddOne = addOne 2

[christiaanb]

@martijnbastiaan : exactly as I thought, mapping type-level functions: https://github.com/gergoerdi/clash-utils/blob/f9c57526381892b8109e72f1724faca42f8ba544/src-clash/Cactus/Clash/Counters.hs#L88-L92

[christiaanb]

@gergoerdi I'm interested: apparently you had a need to write and use it, so I assume eventually other Haskellers will as well. Even though it might not be super friendly to people new to Haskell, I think that's kind of a non-argument: It's not like we'll suddenly be using this n-ary product instead of regular tuples in all of our documentation.

In addition it solves some pet peeves of mine wrt to tuples:

• So many instances!!!! with n-ary products I have to write at most two.
• An actual EMPTY product, as opposed to () which in GHC 8.8 can only be treated as sum-type. Scratch that, I see you also used ::: to circumvent the injectivity checker in the Bundle instance.

One question w.r.t. to the Bundle instance: why does bundle need the knownLength? I can see why unbundle needs it: so it has a structure to recurse on. But why does bundle need it?

[martijnbastiaan]

Even though it might not be super friendly to people new to Haskell, I think that's kind of a non-argument

Maybe we could put things like this in an extra package clash-extra?

[gergoerdi]

So I see @christiaanb has already answered the question on motivation: in my case, I originally wanted something that, given a counter structure like [[10, 24, 13, 7], [9, 13, 5]] will give me some counter signals of type ((Signal dom (Maybe (Index 10)), Signal dom (Maybe (Index 24)), Signal dom (Maybe (Index 13)), Signal dom (Maybe (Index 7))), (Signal dom (Maybe (Index 9)), Signal dom (Maybe (Index 13)), Signal dom (Maybe (Index 5)))). But what is, in general, the type of this function?

[gergoerdi]

One question w.r.t. to the Bundle instance: why does bundle need the knownLength? I can see why unbundle needs it: so it has a structure to recurse on. But why does bundle need it?

Yes you are in good company for saying this; however, the reality is that the GHC type checker barfs on the knownLength-less version:

    bundle PNil = pure PNil
    bundle (x :-: xs) = (:-:) <$> x <*> bundle xs

    • Could not deduce: ts ~ '[]
      from the context: ToSignals domain ts ~ '[]
        bound by a pattern with constructor: PNil :: Product '[],
                 in an equation for ‘bundle’

    • Could not deduce: ts ~ (a0 : ts0)
      from the context: ToSignals domain ts ~ (a : ts1)
        bound by a pattern with constructor:
                   :-: :: forall a (ts :: [*]). a -> Product ts -> Product (a : ts),
                 in an equation for ‘bundle’

    • Could not deduce: a ~ Signal domain a0
      from the context: ToSignals domain ts ~ (a : ts1)
        bound by a pattern with constructor:
                   :-: :: forall a (ts :: [*]). a -> Product ts -> Product (a : ts),
                 in an equation for ‘bundle’
        at clash-utils/src-clash/Cactus/Clash/Product.hs:58:13-20

(and no, this doesn't go away even with an explicitly-polymorphic recursion a la

    bundle = go
      where
        go :: forall dom us. Product (ToSignals dom us) -> Signal dom (Product us)
        go PNil = pure PNil
        go (x :-: xs) = (:-:) <$> x <*> go xs

[gergoerdi]

Ooh I am just now realizing that for the nicest possible type for my product-of-sums ripple counter, I would probably also want n-ary sums, so that something like

[ [1, 2, 3], [4, 5] ]

would be mapped to

Product [ Sum [Signal dom (Index 1), Signal dom (Index 2), Signal dom (Index 3)]
        , Sum [Signal dom (Index 4), Signal dom (Index 5)]]

[gergoerdi]

In case anyone is interested in this, I have now implemented the above with product-of-sum types: see https://github.com/gergoerdi/clash-utils/blob/9e333b3482788220d6f37e1018f57f117a58826f/src-clash/Cactus/Clash/Counters.hs and as an example of use: https://github.com/gergoerdi/clash-utils/blob/9e333b3482788220d6f37e1018f57f117a58826f/src-clash/Cactus/Clash/VGA.hs

vgaDriver
    :: forall timings dom gated synchronous s ps polH w preH pulseH postH polV h preV pulseV postV.
      (HiddenClockReset dom gated synchronous)
    => (dom ~ Dom s ps)
    => (timings ~ 'VGATimings ps ('VGATiming polH w preH pulseH postH) ('VGATiming polV h preV pulseV postV))
    => SVGATimings timings
    -> VGADriver dom w h
vgaDriver timings@SVGATimings = VGADriver{..}
  where
    counters = Proxy
        @'[ [w, preH, pulseH, postH]
          , [h, preV, pulseV, postV]
          ]
    horiz :-: vert :-: PNil = counterProdSum counters (pure True)

    unpackVGA :: Sum (Indices '[visible, pre, sync, post]) -> (Maybe (Index visible), Maybe (Index sync))
    unpackVGA (Here x) = (Just x, Nothing)
    unpackVGA (There (There (Here cnt))) = (Nothing, Just cnt)
    unpackVGA _ = (Nothing, Nothing)

    (vgaX, toSync (Proxy @polH) -> vgaHSync) = unbundle $ unpackVGA <$> horiz
    (vgaY, toSync (Proxy @polV) -> vgaVSync) = unbundle $ unpackVGA <$> vert

    vgaEndLine = isFalling False (isJust <$> vgaX)
    vgaEndFrame = isFalling False (isJust <$> vgaY)

[martijnbastiaan]

Very cool @gergoerdi ! I wanted to let you know your contributions are greatly appreciated, even though we're a bit slow to respond from time to time..