Re: Does Bind beat Kleisli in Hilbert space?

[Alan Jeffrey <ajeffrey@bell-labs.com>]

I appreciate the long-term vision of your VCs.

For your Haskell engineers, isn't this exactly what arrows are designed
to do?  For your category theorists, isn't this exactly what a
premonoidal category or a Freyd category are designed to do?

In both cases, it seems that the mismatch is due to the monadic
requirement that thunks be first-class citizens: this results in types
such as T(T(X)) existing, which seem to be at the root of your problem
with overflow exceptions.

Of course, premonoidal categories are not as prevalent in the industry
as monads are, and the arrows API is not as heavily adopted as the
monads API, so you may have problems interfacing to the large existing
monadic code-base.  I'm sure your leadership team of strategic
visionaries will see the value-add.

Alan.

John Hughes, Generalising Monads to Arrows, in Science of Computer
Programming 37, pp67-111, May 2000.

John Power and Edmund Robinson. Premonoidal Categories and Notions of
Computation, in Mathematical Structures in Computer Science
7(5):453-468, 1997.

John Power and Hayo Thielecke. Closed Freyd- and kappa-categories,
ICALP'99, LNCS 1644, pp 625-634, Springer, 1999.

Vaughan Pratt wrote:
> Project:            Operation QCvac
> Sensitivity level:  Black hole
> Situation report:   Unanticipated overflow exception in a monad
> Reporting analyst:  Vaughan Pratt
> Project status:     On hold pending resolution
> Action item:        Solicit qualified expert opinion
> Date:               October 7, 2007
>
> Situation summary.  We're working on a quantum computer in anticipation
> of a Request for Proposal (RFP) for the next One Laptop Per Child (OLPC)
> computer for a value of "next" that is acceptable to our venture
> capitalists (VCs) yet feasible for our engineers.
>
> To be sure of not being out-competed we've assembled a crack team of
> physicists from Fermilab to get the physics right, category theorists
> from Fairfield, Iowa to design the linear algebra implementation,
> electrical engineers (EEs) from Silicon Valley to build the machine,
> Haskell programmers from Glasgow to implement the ideal third-party
> value-add software environment, and marketers from Boston to understand
> the market's needs and tastes.
>
> Marketing feels we have to be able to offer lots of storage (qubits).
> The physicists said no problem, they work in separable (countably
> dimensioned) Hilbert space all the time.  (You see how physics
> works---physics is scale-invariant, what's good for describing the
> universe is good for describing computers.)  Marketing said great,
> countably infinite storage will make us unbeatable, even Google will
> want one.
>
> Marketing wants to pitch the reliability of our machine.  The category
> theorists said no problem, on their previous consulting job, D-Wave's
> 16-qubit quantum computer, they'd represented linear algebra as God's
> own monad, a monoid object (T,mu,eta) of Set^Set implementing matrix
> multiplication via the Kleisli construction.  They took the functor T(X)
> to be the set C^X of X-dimensional almost-everywhere-zero complex
> vectors with T(f:X->Y): C^X --> C^Y sending v: C^X to the vector u: C^Y
> describable as starting with u = 0 and adding v_x to u_{f(x)} for all x
> in X, the multiplication mu_X: C^(C^X) --> C^X to send V: C^(C^X) to u:
> C^X with u_x the sum of V_v * v_x over all v in C^X (dot product), and
> the unit eta_X: X --> C^X as eta_X(x)(y) = (x=y) (the unit vectors).  It
> worked like a charm.  (You see how category theory works in
> computers---everything is an adjunction, or was in the 1970s, nowadays
> it's all done with monads.)
>
> The EEs expressed concern about the ambitious number of qubits.  The
> category theorists reassured them that infinity held no fears for them
> as the infinite set C^(2^16) had worked fine in the D-Wave machine since
> mu only encountered finitely many nonzero values when summing over the
> domain C^(2^16) of T(f): C^(C(2^16)) --> C(2^16).  The physicists
> reassured them that linear algebra lifted reliably to infinite
> dimensions provided the vectors were kept square summable as confirmed
> by a vast body of experimental evidence, so even though the sums would
> now be infinite they would still converge.  (You see how systems
> analysis works---if monads and square-summability each coordinate well
> with the world they must coordinate well with one another.)
>
...