Tagged implementation

[jonfowler]

This is a work in progress rework of the type inference solution to use a "Tagged" implementation:

type TagCircuitT a b = (TagFwd a :-> TagBwd b) -> (TagBwd a :-> TagFwd b)

newtype Tag t b = Tag {unTag :: b}

type TagFwd a = Tag a (Fwd a)
type TagBwd a = Tag a (Bwd a)

pattern TagCircuit :: TagCircuitT a b -> Circuit a b
pattern TagCircuit f <- (runTagCircuit -> f) where
  TagCircuit f = mkTagCircuit f

With circuits passing around these Tagged types which include the type of the Bus. This has a major advantage for type inference because it can use the type of pre-defined circuits e.g.:

runTagCircuit idC :: (TagFwd a :-> TagBwd a) -> (TagFwd a :-> TagBwd a)

Which means the type of input & output (a) can be unified.

Generated Code

This meas the generated code no longer needs the inferenceHelper and can be just written with Tagged stuff:

swapC2 :: Circuit (a,b) (b,a)
swapC2 = circuit $ \ (a,b) -> (b,a)

results in:

swapC = TagCircuit
  (\ (~(TagBundle (a_Fwd, b_Fwd)) :-> ~(TagBundle (b_Bwd, a_Bwd)))
     -> let in TagBundle (a_Bwd, b_Bwd) :-> TagBundle (b_Fwd, a_Fwd))

TaggedBundle

The main challenge is we need to bundle up typed elements. Consider for example:

circuit $ \(a,b) -> do
  idC -< (b, a)

We will be given TagFwd (a,b) but we need TagFwd a and TagFwd b. We do this using a Tag bundle class which seems to work nicely in practice.

This only needs to support the types with special support in Circuit notation i.e. tuples, unit and vec

[jonfowler]

My ultimate motivation for this is to extend the Signal _ pattern to allow for an arbitrary type which only has a Fwd direction (and trivial Bwd direction).

The main problem is at the moment we rely on the Signal type been given a type to get any sort of type inference. This resolve the problem because the type inference can come from the Circuit that the type is pushed into.

[martijnbastiaan]

If I'm reading this correctly, this "just" produces easier to read core, right? As in, there is no direct benefit for users of circuit-notation. Didn't see your message in time.

My ultimate motivation for this is to extend the Signal _ pattern to allow for an arbitrary type which only has a Fwd direction (and trivial Bwd direction).

Could you expand on this? I'm not familiar with the Signal _ pattern.

[jonfowler]

So the use case is around having better support for Signal/DSignal when using Circuit. We have some circuits which are mainly free-flowing but contain some circuits which require a circuit interface (typically being configured via a memory map). I want to able to use Signal's more easily in this case. So you can do something like:

circuit (mm, Signal x) -> do 
     configurableFunc -< (mm, Signal (fmap (+2) x))

The Signal pattern allows you to access x :: Signal dom Int so you can use normal functions on it.

The problem with the current implementation is relies on knowing the Signal pattern has bus type Signal _ _ otherwise it has really bad inference. That means we can only use this pattern for signals but we really want it for DSignal / Vec (Signal ..) etc.

Doing the tagging fixes this problem because it can use the type of the user supplied function. In the example above configurableFunc might have type:

configurableFunc :: Circuit (MM dom x, Signal dom Int) (Signal dom Int)

So the type inference would just work.

[jonfowler]

This is the example I added that shows what you can do now:

fwdWithLetCircuit :: KnownNat n => Circuit (Vec n (Signal dom Int)) (Vec n (Signal dom Int))
fwdWithLetCircuit = circuit $ \(Fwd x) -> do
  let y = fmap (+1) x
  i <- idC -< Fwd y
  idC -< i

[cchalmers]

I'd expect writing Signal to enforce the type to be Signal. I'm fine with it how it is if that's too much hassle.

[jonfowler]

Yeah it'd be pretty annoying because I would need an inference_helper to do it..

[bgamari]

For what it's worth, this work is extremely useful for my use-case (which sounds very similar to @jonfowler's). I do, however, wish that more of the PR description had made it into the Haddocks. It would have been extremely hard to deduce the motivation for things like, e.g., TagCircuit if I hadn't stumbled upon the MR.