Add linear arrows

[oliverbunting]

Propose definitions for Control.Category.Linear and Control.Arrow.Linear

Happy to discuss / modify.

[aspiwack]

Hi @oliverbunting,

I'm so sorry, I don't know how I missed this PR 😕 .

Can you comment a little on how you came up with this particular choice of design? Was it guided by applications? By theory? Something else

[oliverbunting]

@aspiwack

Control.Category.Linear

Trivial. Takes existing linear id and (.)

Control.Category.Arrow.Linear

My motivation is driven as an ex-professional user of clash. An API for high-level high-level circuit design using arrows to linearly connect circuits is something I've long wanted.

I'll comment per typeclass

Arrow

class Category a => Arrow where
   -- I think this is the only sane linear choice. 
   -- Making either of the arrows non-linear precludes the category instance
   arr :: (b %1 -> c) %1 -> a b c

   -- The 'Dupable' constraint is required
   (&&&) :: (Dupable b) => a b c %1 -> a b c' %1 -> a b (c,c')
   
   -- the other methods follow naturally. 

ArrowLoop

class Arrow a => ArrowLoop a where
    -- Linearly consume / supply d.
    loop :: a (b,d) (c,d) %1 -> a b c

This is the most contentious thing here. For example, an instance for Fun 'One can be shown to be inadmissible by considering the following linear function

notAnArrowLoop :: (Int,Bool) %1 -> (Int,Bool)
notAnArrowLoop n b = if b then (n, False) else (n,True)

ArrowApply

-- ArrowApply is equivalent to Linear control Monad
class Arrow a => ArrowApply a where
    app :: a (a b c, b) c

Methods

(^>>) :: Arrow a => (b %1 -> c) %1 -> a c d %1 -> a b d
(>>^) :: Arrow a => a b c %1 -> (c %1 -> d) %1 -> a b d
(<<^) :: Arrow a => a c d %1 -> (b %1 -> c) %1 -> a b d
(^<<) :: Arrow a => (c %1 -> d) %1 -> a b c %1 -> a b d

These follow directly from the Category and arr definitions

[aspiwack]

Thanks!

I've had time, today, to think about this some. Here are my current thoughts:

---

Let me start by an aside. I recently wrote a paper regarding using linear functions to draw circuits, and how Arrow is not necessarily a suitable abstraction Evaluating Linear Functions to Symmetric Monoidal Categories. You may want to have a look.

---

So, I've thought about the theoretical side of things (always good to have both a theoretical and a practical perspective).

One helpful definition of an Arrow is a strong monad in the bicategory of profunctors. (if you are reading this and you are not familiar with defining monads in a bicategory, and you're curious (you probably shouldn't), the monad page on the nlab starts from this definition).

• The unit (𝜂/return) gives us arr
• The product (𝜇/join) gives us >>> (aka the composition in the Category instance)
• The strength gives us first

Specifically, the Arrow type class from base is about such monads, which are profunctors from and to the notional category Hask of types and (unrestricted) functions.

The simplest way to make a linear arrow out of this is to say: let's take a profunctor from and to the (still notional) category Lin of types and linear functions. It gives us the following types.

arr :: (a %1 -> b) -> p a b
(>>>) :: p a b -> p b c -> p a c -- uses base's `Category` class
first :: p a b -> p (a, c) (b, c)

I've got to admit: this is a bit boring.

However, it may very well be sufficient. For instance, linear Kleisli categories are instances of this linear Arrow class.

With this abstraction we cannot define arrows p a (a, a) in general either.

---

The version you propose would correspond to making linear arrows strong monads in the bicategory of Lin-enriched profunctors. I think. I haven't fully worked this out, but I think it works. (the key point being that in a V-enrichment, you want to replace the definition of profunctor from Cᵒᵖ×D⟶Set to Cᵒᵖ×D⟶V)

Since Arrow is firmly in the Control side of things, it feels natural to work in this encriched setting.

But I would be much more comfortable if we could provide evidence that the enriched definition is more suitable than the rather plain definition from above.

[oliverbunting]

@aspiwack thanks for a detailed reply. I'll confess most of that went by me - both undergrad and research is electronic engineering, and whilst I've used Haskell professionally for the best part of a decade, I've no theoretical background.

---

To respond to your aside, and possibly explain my motivations better:

Let me crudely outline my thoughts on circuit representations. It starts with the observation that in most systems the connections between circuits are bidirectional - circuits communicate using busses - in CMOS with dedicated routing master to slave in each direction (not shared routing resources).

Therefore, if Circuits take and produce instances of Bus as arguments which are glorified functions, linear arrows can be used to define the connectivity between functions. Working with the more restrictive version of arrow is basically essential here, because you want to ensure a bus is consumed exactly once. Circuits with hanging busses are probably a design mistake, whilst reusing a bus implies either hardware duplication, or multiply driven busses, both of which don't want to happen by accident.

You can do most of this with linear Control.Monad, but linear MonadFix is a none starter. However, linear ArrowLoop allows you to define recursive connectivity.

My thoughts are publicly visible, although incomplete and possibly flawed, here if you're interested. I intend to finish that work, it still interests me, but free time is at a premium, so it's happening very slowly. I'd be happy to discuss, but there's got to be a better forum than this PR.

Whilst doing all this a number of years ago, we basically used a source plugin hack to workaround the lack of linear types. An ex-colleague of mine, and one of those (along with christiaanb, martijnbastiaan, JonFowler) who've spent countless hours discussing circuit representations with me, has published that here. I believe its still used in production.

[aspiwack]

Hello again,

Sorry I'm taking so much time to answer. It's been busy times, I'm afraid.

I'll confess most of that went by me - both undergrad and research is electronic engineering, and whilst I've used Haskell professionally for the best part of a decade, I've no theoretical background.

It's alright, I suppose this was mostly for my personal consumption 🙂 .

Therefore, if Circuits take and produce instances of Bus as arguments which are glorified functions, linear arrows can be used to define the connectivity between functions. Working with the more restrictive version of arrow is basically essential here, because you want to ensure a bus is consumed exactly once.

Ok, so, do I understand right that, in this scenario, a bus is a value of type Circuit A B, and we have Arrow Circuit?

My thoughts are publicly visible, although incomplete and possibly flawed, here if you're interested.

It is a bit over my head, I'm afraid.

I'd be happy to discuss, but there's got to be a better forum than this PR.

I'm available for a call if you wish. You can send me an email. First name dot last name @tweag.io .