Implementing Profunctor Equipment in Haskell

Category theory often feels abstract until it is grounded in a concrete implementation. In a recent exploration, Bartosz Milewski demonstrates how to implement "Profunctor Equipment"—a sophisticated categorical structure—within Haskell. While a full implementation would ideally require a dependently typed language, Haskell's type system is powerful enough to provide a toy implementation that allows programmers to verify these mathematical intuitions via the compiler.

The Core Components of Profunctor Equipment

To implement Profunctor Equipment in Haskell, we must map categorical concepts to Haskell's type system. The implementation focuses on a single category (the Haskell category of types and functions) and restricts itself to endo-functors and endo-profunctors.

0-Cells, 1-Cells, and 2-Cells

In this framework, the components are defined as follows:

• 0-Cells: The Haskell category of types and functions.
• Vertical 1-Cells: Implemented using the standard library's Functor.
• Horizontal 1-Cells: Implemented using Profunctor.
• 2-Cells: These are implemented as natural transformations. In Haskell, this is represented as a polymorphic function:

type Cell f g h j = forall a c . h a c -> j (f a) (g c)

Here, the forall serves as the universal quantifier, ensuring the transformation holds for all types a and c.

Composition and Units

One of the primary challenges in implementing equipment is handling the different modes of composition: horizontal and vertical.

Horizontal Composition

Horizontal composition combines two cells to create a new cell that operates on composed functors. Using the Compose newtype for functor composition, the implementation is as follows:

hcomp :: (Functor f, Functor f', Functor g, Functor g'
         , Profunctor h, Profunctor j, Profunctor k) =>
    Cell f g h j -> Cell f' g' j k 
                 -> Cell (Compose f' f) (Compose g' g) h k

hcomp fg_hj fg_jk hac = dimap getCompose Compose $ fg_jk (fg_hj hac)

Vertical Composition and Coends

Vertical composition is more complex and requires profunctor composition. This is implemented using a coend, which in Haskell is represented as an existential type:

data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

In this definition, x is an existential type—it does not appear in the argument list, meaning it is hidden from the outside world, which is exactly how coends behave in category theory.

Unit Cells

To satisfy the laws of equipment, unit cells must be defined for both dimensions:

• Horizontal Unit: type Hunit p = Cell Identity Identity p p
• Vertical Unit: type Vunit f a b = Cell f f (->) (->)

Companions and Conjoints

The implementation further extends to the concepts of companions and conjoints, which are essentially synonyms for the Costar and Star types found in the Haskell ecosystem.

• Companion: Represented as Costar f d c, defined as newtype Costar f d c = Costar { runCostar :: f d -> c }.
• Conjoint: Represented as Star f d c, defined as newtype Star f d c = Star { runStar :: d -> f c }.

These are equipped with unit and counit cells. For example, the companion unit and counit are defined as:

type CompUnit f   = Cell Identity f (->) (Costar f)
compUnit :: Functor f => CompUnit f
compUnit h = Costar (fmap (h . runIdentity))

type CompCoUnit f = Cell f Identity (Costar f) (->)
compCoUnit (Costar h) = Identity . h

Technical Reflections and Limitations

While this Haskell implementation provides a valuable bridge between abstract math and executable code, it has limitations. The author notes that a more adequate implementation would require a dependently typed language (such as Lean), where the relationships between these types could be more strictly enforced and proven.

This sentiment is echoed in the community, with some suggesting that dependently typed languages are better suited for this level of formal verification. However, the utility of this "toy" implementation remains: it allows the programmer to use the Haskell compiler as a sanity check for categorical constructions.

Despite the theoretical depth, some practitioners note a gap between these constructions and practical application. The challenge remains in translating these high-level categorical equipments into day-to-day software engineering patterns that provide tangible benefits to the developer.