Benton’s Linear/Nonlinear Logic has models in (lax) monoidal adjunctions between monoidal and cartesian categories.

The tasks performed in GPU kernels often deal with linear and nonlinear maps between real vector spaces.

I want to take this and run with it: let’s see what it looks like to define some mixed linear/nonlinear functions in a linear/nonlinear type theory. This feels to me so obvious that it must be written down somewhere already. In the literature there is work that gets close (and I’ll do some comparisons at the end), but none are quite what I want. Please let me know if I’ve missed something.

Edit: It’s been pointed out to me that the type theory I’ve put together is almost exactly the Enriched Effect Calculus, though I still haven’t seen the semantics in ordinary vector spaces discussed anywhere. And see my follow-up!

Code available on GitHub.

For a little while I have been working on this port of Kenzo from Common Lisp to Haskell. Kenzo is a collection of algorithms for explicit constructions on simplicial sets: the README in the repository gives a list of what’s implemented and what should be possible. The algorithms and implementations in Kenzo were created by Francis Sergeraert, Julio Rubio Garcia, Xavier Dousson, Ana Romero and many collaborators.

My goal was to implement just enough to compute \pi_4 S^3, and I reached it today.

...
> let x = totalSpace s3 (Wbar kz1) fibration
> putStrLn $ "π₄ S³ is: " ++ show (homology x !! 4)
π₄ S³ is: ℤ/2

A fun capability it picked up along the way is calculating the homology of Eilenberg-MacLane spaces K(ℤ/m,n), for example, here is K(ℤ/3,2).This makes my laptop get hot pretty quickly.

> homology (Wbar (WbarDiscrete (Zmod 3)))
[ℤ,0,ℤ/3,0,ℤ/3,0,ℤ/(3^2),ℤ/3,ℤ/3,ℤ/3,ℤ/3 ⊕ ℤ/3,^C

I have a lot of ideas for improvements and additional features if anybody is interested in joining in, so please email me if that’s you or you know a student for whom this would make a good project. For example, adding the construction of loop spaces and their homology would be nice, as would homotopy pushouts in general.

On the implementation side, I have not spent any time optimising the code and there are some obvious places to start, like using a proper integer matrix library instead of a homemade one. These sorts of optimisations would also make a good project for an undergraduate, with not much mathematical background required.

Below, I’ve copy-pasted a quick introduction I wrote to the ideas behind Kenzo.