## Circuits as a bicartesian closed category

My previous few posts have been about cartesian closed categories (CCCs). In From Haskell to hardware via cartesian closed categories, I gave a brief motivation: typed lambda expressions and the CCC vocabulary are equally expressive, but have different strengths:

• In Haskell, the CCC vocabulary is overloadable and so can be interpreted more flexibly than lambda and application.
• Lambda expressions are friendlier for human programmers to write and read.

By automatically translating lambda expressions to CCC form (as in Overloading lambda), I hope to get the best of both options.

An interpretation I’m especially keen on—and the one that inspired this series of posts—is circuits, as described in this post.

Edits:

• 2013–09–17: “defined for all products with categories” ⇒ “defined for all categories with products”. Thanks to Tom Ellis.
• 2013–09–17: Clarified first CCC/lambda contrast above: “In Haskell, the CCC vocabulary is overloadable and so can be interpreted more flexibly than lambda and application.” Thanks to Darryl McAdams.

### CCCs

First a reminder about CCCs, taken from From Haskell to hardware via cartesian closed categories:

You may have heard of “cartesian closed categories” (CCCs). CCC is an abstraction having a small vocabulary with associated laws:

• The “category” part means we have a notion of “morphisms” (or “arrows”) each having a domain and codomain “object”. There is an identity morphism for and associative composition operator. If this description of morphisms and objects sounds like functions and types (or sets), it’s because functions and types are one example, with `id` and `(∘)`.
• The “cartesian” part means that we have products, with projection functions and an operator to combine two functions into a pair-producing function. For Haskell functions, these operations are `fst`, `snd` and `(△)`. (The latter is called “`(&&&)`” in `Control.Arrow`.)
• The “closed” part means that we have a way to represent morphisms as objects, referred to as “exponentials”. The corresponding operations are `curry`, `uncurry`, and `apply`. Since Haskell is a higher-order language, these exponential objects are simply (first class) functions.

As mentioned in Overloading lambda, I also want coproducts (corresponding to sum types in Haskell), extending CCCs to bicartesian close categories, or “biCCCs”.

Normally, I’d formalize a notion like (bi)CCC with a small collection of type classes (e.g., as in Edward Kmett’s categories package). Due to a technical problem with associated constraints (to be explored in a future post), I’ve so far been unable to find a satisfactory such formulation. Instead, I’ll convert the biCCC term representation given in the post Overloading lambda.

#### Circuits

How might we think of circuits? A simple-sounding idea is that circuits are directed graphs of components components (logic gates, adders, flip-flops, etc), in which the graph edges represent wires. Each component has some input pins and some output pins, and each wire connects an output pin of some component to an input pin of another component.

On closer examination, some questions arise:

• How to identify intended inputs and outputs?
• How to ensure that the graphs are fully connected other than intended external inputs and outputs?
• How to ensure that input pins are driven by at most one output pin, while allowing output pins to drive any number of input pins?
• How to sequentially compose graphs, matching up and consuming free outputs and inputs?

Note that similar questions arose in the design of programming languages. In functional languages (or even semi-functional ones like Fortran, ML, and Haskell+IO), we answer the connectivity/composition questions by nesting function applications. Overall inputs are identified syntactically as function parameters, while output corresponds to the body of the function.

We can adapt this technique to the construction of circuits as follows. Instead of building graph fragments directly and then adding edges/wires to connect those fragments, let’s build recipes that consume output pins, build a graph fragment, and indicate the output pins of that fragment. A circuit (generator) is thus a function that takes some output pins as arguments, instantiates a collection of components, and yields some output pins. The passed-in output pins come from other component instantiations, or are the top-level external inputs to a circuits. The number and arrangement of the pins consumed and yielded vary and so will appear as type parameters. Since distinct pins are generated as needed, a circuit will also consume part of a given supply of pins, passing on the remainder for further component construction.

``type CircuitG b = PinSupply → (PinSupply, [Comp], b) -- first try``

Note that the input type is absent, because it can show up as part of a function type: `a → CircuitG b`. This factoring is typical in monadic formulations.

##### A circuit monad

Of course, we’ve seen this pattern before, in writer and state monads. Moreover, the writer will want to append component lists, so for efficiency, we’ll replace `[a]` with an append-friendly data type, namely sequences represented as finger trees (`Seq` from `Data.Sequence`).

``type CircuitM = WriterT (Seq Comp) (State PinSupply)``

One very simple operation is generation of a single pin (producing no components).

``````newPin ∷ CircuitM Pin
newPin = do { (p:ps') ← get ; put ps' ; return p }``````

In fact, this definition has a considerably more general type, because it doesn’t use the `WriterT` aspect of `CircuitM`. The `get` and `put` operations come from the `MonadState` in the `mtl` package, so we can use any `MonadState` instance with `PinSupply` as the state. For convenience, define a constraint abbreviation:

``type MonadPins = MonadState PinSupply``

and use the more general type:

``newPin ∷ MonadPins m ⇒ m Pin``

We’ll need this extra generality later.

I know I promised you a category rather than a monad. We’ll get there.

Each pin will represent a channel to convey one bit of information, but varying with time, i.e., a signal. The values conveyed on these wires will not be available until the circuit is realized in hardware and run. While constructing the graph/circuit, we’ll only need a way of distinguishing the pins and generating new ones. Given these simple requirements, we’ll represent pins simply as integers, but `newtype`-wrapped for type-safety:

``````newtype Pin = Pin Int deriving (Eq,Ord,Show,Enum)
type PinSupply = [Pin]``````

Each circuit component is an instance of an underlying primitive and has three characteristics:

• the underlying “primitive”, which determines the functionality and interface (type of information in and out),
• the pins carrying information into the instance (and coming from the outputs of other components), and
• the pins carrying information out of the instance.

Components can have different interface types, but we’ll have to combine them all into a single collection, so we’ll use an existential type:

``````data Comp = ∀ a b. IsSource2 a b ⇒ Comp (Prim a b) a b

deriving instance Show Comp``````

For now, a primitive will be identified simply by a name:

``````newtype Prim a b = Prim String

instance Show (Prim a b) where show (Prim str) = str``````

The `IsSource2` constraint is an abbreviation for `IsSource` constraints on the domain and range types:

``type IsSource2 a b = (IsSource a, IsSource b)``

Sources will be structures of pins. We’ll need to flatten them into sequences, generate them for the outputs of a new instance, and inquire the number of pins based on the type (i.e., without evaluation):

``````class Show a ⇒ IsSource a where
toPins    ∷ a → Seq Pin
genSource ∷ MonadPins m ⇒ m a
numPins   ∷ a → Int``````

Instances of `IsSource` are straightforward to define. For instance,

``````instance IsSource () where
toPins () = ∅
genSource = return ()
numPins _ = 0

instance IsSource Pin where
toPins p  = singleton p
genSource = newPin
numPins _ = 1

instance IsSource2 a b ⇒ IsSource (a × b) where
toPins (sa,sb) = toPins sa ⊕ toPins sb
genSource      = liftM2 (,) genSource genSource
numPins ~(a,b) = numPins a + numPins b``````

Note that we’re taking care never to evaluate the argument to `numPins`, which will be `⊥` in practice.

##### A circuit category

I promised you a circuit category but gave you a monad. There’s a standard construction to turn monads into categories, namely `Kleisli` from `Control.Category`, so you might think we could simply define

``type a ⇴ b = Kleisli CircuitM  -- first try``

What I don’t like about this definition is that it requires parameter types like `Pin` and `Pin × Pin`, which expose aspects of the implementation. I’d prefer to use `Bool` and `Bool × Bool` instead, to reflect the conceptual types of information flowing through circuits. Moreover, I want to generate computations parametrized over the underlying category (and indeed generate these category-generic computations automatically from Haskell source). Explicit mention of representation notions like `Pin` would thwart this genericity, restricting to circuits.

To get type parameters like `Bool` and `Bool × Bool`, we’ll have to convert value types to pin types. Type families gives us this ability:

``type family Pins a``

Now we can say that circuits can pass a `Bool` value by means of a single pin:

``type instance Pins Bool = Pin``

We can pass the unit with no pins at all:

``type instance Pins () = ()``

The pins for `a × b` include pins for `a` and pins for `b`:

``type instance Pins (a × b) = Pins a × Pins b``

Sum types are trickier. We’ll get there in a bit.

Now we can define our improved circuit category:

``newtype a ⇴ b = C (Kleisli CircuitM (Pins a) (Pins b))``
##### Sum types

As we say above, the `Pins` type family distributes over `()` and pairing. The same is true for every fixed-shape type, i.e., every type in which all values have the same representation shape, including $n$-tuples, length-typed vectors and depth-typed perfect leaf trees.

The canonical example of a type whose elements can vary in shape is sums, represented in Haskell as the `Either` algebraic data type, for instance `Either Bool (Bool,Bool)`, which I’ll write instead as `Bool + Bool × Bool`. Can `Pins` distribute over `+`, i.e., can we define

``type instance Pins (a + b) = Pins a + Pins b  -- ??``

We cannot use this definition, because it implies that the we must choose a shape statically, i.e., when constructing the circuit. The data may, however, change shape dynamically, so no one static choice suffices.

I’ll give a solution, which seems to work out okay. However, it lacks the elegance and inevitability that I always look for, so if you have other ideas, please leave suggestions in comments on this post.

The idea is that we’ll use enough pins for the larger of the two representations. Since the two `Pins` representations (`Pins a` vs `Pins b`) can be arbitrarily different, flatten them into a common shape, namely a sequence. To distinguish the two summands, throw in an additional bit/pin:

``````data a :++ b = UP { sumPins ∷ Seq Pin, sumFlag ∷ Pin }

type instance Pins (a + b) = Pins a :++ Pins b``````

Now we’ll want to define an `IsSource` instance. Recall the class definition:

``````class Show a ⇒ IsSource a where
toPins    ∷ a → Seq Pin
genSource ∷ MonadPins m ⇒ m a
numPins   ∷ a → Int``````

It’s easy to generate a sequence of pins:

``````instance IsSource2 a b ⇒ IsSource (a :++ b) where
toPins (UP ps f) = ps ⊕ singleton f``````

The number of pins in `a :++ b` is the maximum number of pins in `a` or `b`, plus one for the flag bit:

``  numPins _ = (numPins (⊥ ∷ a) `max` numPins (⊥ ∷ b)) + 1``

To generate an `a :++ b`, generate this many pins, using one for `sumFlag` and the rest for `sumPins`:

``````  genSource =
liftM2 UP (Seq.replicateM (numPins (⊥ ∷ (a :++ b)) - 1) newPin)
newPin``````

where `Seq.replicateM` function here comes from `Data.Sequence`:

``replicateM ∷ Monad m ⇒ Int → m a → m (Seq a)``

This `genSource` definition is one motivation for the `numPins` method. Another is coming up in the next section.

### Categorical operations

I’m working toward a representation of circuits that is both simple and able to implement the standard collection of operations for a cartesian closed category, plus coproducts (i.e., a bicartesian closed category, IIUC). Here, I’ll show how to implement these operations, which are also mentioned in my recent post Overloading lambda.

#### Category operations

A category has an identity and sequential composition. As defined in `Control.Category`,

``````class Category k where
id  ∷ a `k` a
(∘) ∷ (b `k` c) → (a `k` b) → (a `k` c)``````

The required laws are that `id` is both left- and right-identity for `(∘)` and that `(∘)` is associative.

Recall that our circuit category `(⇴)` is almost the same as `Kleisli CircuitM`, where `CircuitM` is a monad (defined via standard monadic building blocks). Thus we almost have for free that `(⇴)` is a category, but we still need a little bit of work.

``newtype a ⇴ b = C (Kleisli CircuitM (Pins a) (Pins b))``

Since this representation wraps `Kleisli CircuitM`, which is already a category, we need only do a little more unwrapping and wrapping:

``````instance Category (⇴) where
id  = C id
C g ∘ C f = C (g ∘ f)``````

The category laws for `(⇴)` follow easily. For instance,

``id ∘ C f ≡ C id ∘ C f ≡ C (id ∘ f) ≡ C f``

I’ll leave the other two (right-identity and associativity) as a simple exercise.

There’s an idiom I like to use for definitions such as the `Category` instance above, to automate the unwrapping and wrapping:

``````instance Category (⇴) where
id  = C id
(∘) = inC2 (∘)``````

where

``````inC  =   C ↜ unC
inC2 = inC ↜ unC``````

The `(↜)` operator here adds post- and pre-processing:

``(h ↜ f) g = h ∘ g ∘ f``

#### Product operations

Next, let’s add product types and a minimal set of associated operations: One simple formulation:

``````class Category k ⇒ ProductCat k where
exl ∷ (a × b) `k` a
exr ∷ (a × b) `k` b
(△) ∷ (a `k` c) → (a `k` d) → (a `k` (c × d))``````

If you’ve used `Control.Arrow`, you’ll recognize `(△)` as “`(&&&)`”. The `exl` and `exr` methods generalize `fst` and `snd`. There are other operations from `Arrow` methods that can be defined in terms of these primitives, including `first`, `second`, and `(×)` (called “`(***)`” in `Control.Arrow`):

``````(×) ∷ ProductCat k ⇒ (a `k` c) → (b `k` d) → (a × b `k` c × d)
f × g = f ∘ exl △ g ∘ exr

first ∷ ProductCat k ⇒ (a `k` c) → ((a × b) `k` (c × b))
first f = f × Id

second ∷ ProductCat k ⇒ (b `k` d) → ((a × b) `k` (a × d))
second g = Id × g``````

Notibly missing is the `Arrow` class’s `arr` method, which converts an arbitrary Haskell function into an arrow. If I could implement `arr`, I’d have my Haskell-to-circuit compiler. I took the names “`exl`”, “`exr`”, and “`(△)`” (pronounced “fork”) from Jeremy Gibbon’s delightful paper Calculating Functional Programs.

Again, it’s easy to define a `ProductCat` instance for `(⇴)` using the `ProductCat` instance for the underlying ProductCat for `Kleisli CircuitM` (which exists because `CircuitM` is a monad):

``````instance ProductCat (⇴) where
exl = C exl
exr = C exr
(△) = inC2 (△)``````

There is a subtlety in type-checking this instance definition. In the `exl` definition, the RHS `exl` above has type

``Kleisli CircuitM (Pins a × Pins b) (Pins b)``

but the `exl` definition requires type

``Kleisli CircuitM (Pins (a × b)) (Pins b)``

Fortunately, these two types are equivalent, thanks to the `Pins` instance for products given above:

``type instance Pins (a × b) = Pins a × Pins b``

Again, the class law proofs are again straightforward.

The product laws are given in Calculating Functional Programs (p 155) and again are straightforward to verify. For instance,

``exl ∘ (u △ v) ≡ u``

Proof:

``````  exl ∘ (C f △ C g)
≡ C exl ∘ C (f △ g)
≡ C (exl ∘ (f △ g))
≡ C f``````

#### Coproduct operations

The coproduct/sum operations are exactly the duals of the product operations. The method signatures thus result from those of `ProductCat` by inverting the category arrows and replacing products by coproducts:

``````class Category k ⇒ CoproductCat k where
inl ∷ a `k` (a + b)
inr ∷ b `k` (a + b)
(▽) ∷ (a `k` c) → (b `k` c) → ((a + b) `k`  c)``````

The coproduct laws are also exactly dual to the product laws, i.e., the operations are replaced by their counterparts, and the the compositions are reversed. For instance,

``exl ∘ (u △ v) ≡ u``

becomes

``(u ▽ v) ∘ inl ≡ u``

Just as the `IsSource` definition for sums above is more complex than the one for products, similarly, the `CoproductCat` instance I’ve found is much trickier than the `ProductCat` instance. I’d really love to find much simpler definitions, as the extra complexity worries me. If you think of simpler angles, please do suggest them in comments on this post. Alternatively, if you understand the essential cause of the loss of simplicity in going from products to coproducts, please chime in as well.

For the left-injection, `inl ∷ a ⇴ a + b`, flatten the `a` pins, pad to the longer of the two representations as needed, and add a flag of `False` (left):

``````inl = C ∘ Kleisli \$ λ a →
do x ← constM False a
let na  = numPins (⊥ ∷ Pins a)
nb  = numPins (⊥ ∷ Pins b)
pad = Seq.replicate (max na nb - na) x
return (UP (toPins a ⊕ pad) x)``````

Similarly for `inr`. (The implementation refactors to remove redundancy.)

There is a problem with this definition, however. Its type is

``inlC ∷ IsSourceP2 a b ⇒ a ⇴ a + b``

where

``````type IsSourceP  a   = IsSource (Pins a)
type IsSourceP2 a b = (IsSourceP a, IsSourceP b)``````

In contrast, the `CoproductCat` class definition insists on full generality (unconstrained `a` and `b`). I don’t know how to resolve this problem. We can change the `CoproductCat` class definition to add associated constraints, but when I tried, the types of derived operations (definable via the class methods) became terribly complicated. For now, I’ll settle for a near miss, implementing operations like those of `CoproductCat` but with the extra constraints that thwarts the instance definition I’m seeking.

For the `(▽)` operation, let’s assume we have a conditional operation, taking two values and a boolean, with the `False`/`else` case coming first:

``condC ∷ IsSource (Pins c) ⇒ ((c × c) × Bool) ⇴ c``

Now, given an `a :++ b` representation,

• extract the `sumFlag` for the `Bool`,
• extract pins for `a` and feed them to `f`,
• extract pins for `b` and feed them to `g`, and
• feed these three results into `condC`:
``f ▽ g = condC ∘ ((f × g) ∘ extractBoth △ pureC sumFlag)``

The `(×)` operation here is simple parallel composition and is defined for all categories with products:

``````(×) ∷ ProductCat k ⇒
(a `k` c) → (b `k` d) → ((a × b) `k` (c * d))
f × g = f ∘ exl △ g ∘ exr``````

The `pureC` function wraps a pins-to-pins function as a circuit and is easily defined thanks to our use of the `Kleisli` arrow:

``````pureC ∷ (Pins a → Pins b) → (a ⇴ b)
pureC = C ∘ arr``````

The `extractBoth` function extracts both interpretations of a sum:

``````extractBoth ∷ IsSourceP2 a b ⇒ a + b ⇴ a × b
extractBoth = pureC ((pinsSource △ pinsSource) ∘ sumPins)``````

Finally, `pinsSource` builds a source from a pin sequence, using the `genSource` method from `IsSource`.

``````pinsSource ∷ IsSource a ⇒ Seq Pin → a
pinsSource pins = Mtl.evalState genSource (toList pins)``````

It is for this function that I wanted `genSource` to work with monads other than `CircuitM`. Here, we’re using simply `State PinSupply`.

So here we have circuits as a category with coproducts. It “seems to work”, but I have a few points of dissatisfaction:

• We don’t quite get the `CoproductCat` instance, because of the `IsSource` constraints imposed by all three would-be method definitions.
• The definitions are considerably more complex than the `ProductCat` instance and don’t exhibit an apparent duality to those definitions.
• The use of `extractBoth` frightens me, as it implies a sort of dynamic cast between any two types. (Consider `exr ∘ extractBoth ∘ inl`.)

#### Closure

My compilation scheme relies on translating Haskell programs to biCCC (bicartesian closed category) form. We’ve seen above how to interpret the category, cartesian, and cocartesian (coproduct) aspects as circuits. What about closed? I don’t have a precise and implemented answer. Below are some thoughts.

Recall from Overloading lambda, that a (cartesian) closed category is one with exponential objects `b ⇨ c` (often written “${c}^{b}$”) with the following operations:

``````apply   ∷ (a ⇨ b) × a ↝ b
curry   ∷ (a × b ↝ c) → (a ↝ (b ⇨ c))
uncurry ∷ (a ↝ (b ⇨ c)) → (a × b ↝ c)``````

What is a circuit exponential, i.e., a “hardware closure”?

We could operate on lambda expressions, removing inner lambdas, as traditional (I think) in defunctionalization. (See, e.g., Defunctionalization at Work and Polymorphic Typed Defunctionalization.) In this case, `curry` would not appear in the generated CCC term, and application (by other than statically known primitives) would be replaced by pattern matching and invocation of statically known functions/circuits.

Alternatively, first convert to CCC form, simplify, and then look at the remaining uses of `curry`, `uncurry`, and `apply`. I’m not sure I really need to handle `uncurry`, which is not generated by the lambda-to-CCC translation. I think I currently use it only for uncurrying primitives. In any case, focus on `curry` and `apply`.

As in defunctionalization, do a global sweep of the code, and extract all of the closure formations. If we’ve already translated to CCC form, those formations are just the explicit arguments to `curry` applications. Assemble all of these `curry` applications into a single GADT:

``````data b ⇨ c where
⋯``````

For every application `curry f` in our program, where `f ∷ A × B ↣ C` for some types `A`, `B`, and `C`, generate a GADT constructor/tag like the following:

``  Clo_xyz ∷ A → (B ⇨ C)``

where “`xyz`” is generated automatically for distinctness. Note that we cannot use simple algebraic data types, because the type `B ⇨ C` is restricted. Furthermore, if `f` is polymorphic, we may have an existential constructor. Since there are only finitely many occurrences of `curry`, we can represent the GADT constructors with finitely many bits, generalizing the treatment of coproducts described above. If we monomorphize, then we can use several different closure data types for different types `b` and `c`, reducing the required number of bits.

Now consider `apply`. Each occurrence will have some type of the form `(b ⇨ c) × b ↝ c`. The implementation of apply will extract the closure constructor and its argument of some type `a`, use the constructor to identify the intended circuit `f ∷ a × b ↣ c`, and feed the `a` and `b` into `f`, yielding `c`.

What about `uncurry`?

``uncurry ∷ (a ↝ (b ⇨ c)) → (a × b ↝ c)``

The constructed circuit would work as follows: given `(a,b)`, feed `a` to the argument morphism to get a closure of type `b ⇨ c`, which has an `a'` and a tag that refers to some `a' × b → c`. Feed the `a'` and the `b` into that circuit to get a `c`, which is returned.

### Status

I have not yet made the general plan for exponentials precise enough to implement, so I expect some surprises. And perhaps there are better approaches. Please offer suggestions!

Recursive types need thought. If simply translated to sums and products, we’d get infinite representations. Instead, I think we’ll have to use indirections through some kind of memory, as is typically done in software implementations. In this case, dynamic memory management seems inevitable. Indirection might best be used for sums whether appearing in a recursive type or not, depend on the disparity and magnitude of representation sizes of the summand types.

1. #### Warbo:

Having both sides of a sum use the largest number of pins reminds me of studying ALU design at University. Rather than selecting which circuit (operation) to send data to, we would send it to all circuits and select the output we want to keep.

The type-unsafe scariness may come from the fact that this is evaluated eagerly, so all operations will be performed even if they’re meaningless, as long as we select the result of a meaningful operation.

2. #### ao:

I wonder if you tried looking into Temperley-Lieb categories (eg. http://www.math.helsinki.fi/logic/sellc-2010/course/final.pdf)?. There is a neat way to represent sums, evaluate (simply typed) lambda calculus, not to mention that representing them as circuits is as straight-forward as it gets

3. #### Jacques Carette:

I believe that the fundamental reason you are not able to implement inl/inr without constraints is that the implementation fundamentally assumes that a and b are Finite [that’s what numPins forces]. Which is a perfectly fine assumption, but it is not one which is ‘native’ to Category. It might be expedient to make that assumption, and work over a finite category, which you can here define as one which has a map from all objects to Nat. You’ll probably want a comonoid structure as well, which decomposes objects (aka toPins).

4. #### Tom Ellis:

I belive Warbo’s observation about selecting which output you want to keep corresponds to the identification of `A + B -> X` with `(A -> X, B -> X)`.

5. #### Tom Ellis:

I have had a lot of success with a “wiring diagram” API based on arrows that I am using to write relational queries and compile them to SQL. The inspiration was David Spivak’s The operad of wiring diagrams: formalizing a graphical language for databases….

I have managed to avoid type instances and “IsSource” constraints with what seems to be a cunning trick. I used `Wire` rather than `Pins`, and instead of requiring `Wire` to be the type constructor in front of every datatype that represents connectors, I just store `Wire`s in any Haskell datatype, so for example we have `plus :: QueryArr (Wire Int, Wire Int) (Wire Int)` and `restrict :: QueryArr (Wire Bool) ()`.

The definition is `data Wire a = Wire String`, where the string field is the column name of a database table. Typesafety is provided by ensuring that you can only produce a `Wire` in the context of a table which contains a column which is referred to in the `Wire`.

This approach has worked very well. I haven’t considered coproducts, but would probably fake them up by representing `A + B ~> X` as `(A ~> X, B ~> X)` rather than trying to construct `A + B` itself.

6. #### Ryan:

I think you can derive uncurry as uncurry f := apply . (f * id). When f := curry f’, you obtain that curry and uncurry are inverses by beta.

7. #### Sjoerd Visscher:

The methods I use for CCCs in data-category are:

```apply ∷ (a ⇨ b) × a ↝ b
tuple ∷ a ↝ (b ⇨ (a × b))
(^^^) ∷ (a ↝ b) → (d ↝ c) → ((c ⇨ a) ↝ (d ⇨ b))```

with `curry f = (id ^^^ f) . tuple` and `uncurry f = apply . (f *** id)`.

`(^^^)` is analogous to `(+++)` and `(***)`.

8. #### Kari:

Dan Ghica has suggested symmetric monoidal closed categories as models for circuits (http://www.cs.bham.ac.uk/~drg/papers/popl07x.pdf). He introduces specific categories ‘Category of handshake circuits’ HC and another called SHC.

I don’t know how these compare to the ‘Circuit Category’ C (Kleisli CircuitM (Pins a) (Pins b)).