Conal Elliott

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.

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...