tuura / plato

A DSL for asynchronous circuits specification
Other
12 stars 2 forks source link

Concept wrappers #25

Open snowleopard opened 8 years ago

snowleopard commented 8 years ago

As discussed during today's Tuura meeting, we need a way to compose two concepts by matching some of their interface signals. As a simple example, consider connecting two buffers together in sequence:

data S1 = A | B | C | ...
b1 :: CircuitConcept S1
b1 = buffer A B

data S2 = X | Y | ...
b2 :: CircuitConcept S2
b2 = buffer X Y

-- This won't compile due to type mismatch
composition = b1 <> b2

How do we tell that we want to connect b1's output B to b2's input X?

A good solution seems to rely on wrappers:


wrap :: (a -> b) -> CircuitConcept a -> CircuitConcept b
wrap = ...

map21 :: S2 -> S1
map21 X = B
map21 Y = C

composition :: CircuitConcept S1
composition = b1 <> wrap map21 b2

An alert reader will spot that wrap is just an fmap! Indeed, all we need to do is to write a Functor instance for CircuitConcept, and then we will be able to wrap simply by fmap map21 b2 or map21 <$> b2 using a fancy standard operator.

I'll give this a try.

snowleopard commented 8 years ago

As soon as I started on a test implementation I realised that we actually need isomorphism between the original type of signals and the wrapper interface. Indeed, if we only have a one-way mapping a -> b then we can map two two previously distinct signals into one, which would be a mess. Haskell spots this and doesn't allow me to implement a Functor instance :)

So, the right direction seems to be towards an Iso typeclass, and while we are at it, why not give a try to the revered Control.Lens library: https://hackage.haskell.org/package/lens.

snowleopard commented 8 years ago

I've added a draft implementation for wrappers in #27:

wrap :: (a -> b) -> (b -> a) -> CircuitConcept a -> CircuitConcept b
wrap to from c = Concept
                 {
                     initial   = wrapSpace $ initial c,
                     excited   = \e -> wrapSpace $ excited c (fmap from e),
                     invariant = wrapSpace $ invariant c
                 }
  where
    wrapSpace p = \s -> p (State $ getState s . to)

My previous comment was somewhat misguided: I mixed up isomorphisms with invariant functors. The wrap function actually implements the Invariant class from Data.Functor.Invariant.

Having said that, the input to the wrap function is indeed an isomorphism: we need both to :: a -> b as well as from :: b -> a to wrap a circuit, which prevents us from smashing two different signals together, assuming that to . from = id.