You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jonathan Beardsley (Mar 27 2020 at 20:29):So I'm somewhat interested in understanding functional programming, primarily because I'm interested in category theory. In other words, a lot of the benefits of functional programming that one can read about online don't really blow my mind (mostly because I literally don't know what the words mean, and I don't spend time writing code and having desires about ways to write code). I have this book called "Learn You a Haskell for a Great Good!" and I've read a bit of it, but again, I have a hard time getting motivated to learn all of this language. If you wanted to motivate someone who knew a lot of math, and had some basic programming skills, to get into functional programming, is there some kind of basic project you would encourage them to try to write up using Haskell or some other language? Are there fun math things that can be done with this type of programming language?
Stelios Tsampas (Mar 27 2020 at 20:47):Hmmm, for a person with a background as strong as yours (I see online that your interests include Algebraic Topology, Category Theory, Homotopy Theory, Non-Commutative Geometry, Operads. That means you should already know at least some dependent type theory), I'm sorry but in terms of insights or a-ha moments I struggle to find good reasons for you to get into functional programming. Unless you want to program! Is programming fun? Idk, is football or basketball fun? I guess you should try it to find out ;).
The one important reason you might want to try a functional language is theorem proving (like Agda). If I could, I would do all my CT in Agda but it's not quite there yet (maybe @Reed Mullanix disagrees). Machine-checked proofs force you to be precise, to be economic in your definitions and give you a safety net that the paper can't. Which is worth it, if you're willing to spend the time for it.
Jonathan Beardsley (Mar 27 2020 at 20:52):So I mean, there are things I think might be fun to do, like construct an operad "type" in functional programming, or a simplcial set "type." Maybe some of this stuff has already been done. I think it'd also be interesting to use some kind of "lazy evaluation" to potentially compute low level things about infinite things (like operads or infinite simplicial sets).
Jonathan Beardsley (Mar 27 2020 at 20:53):Maybe write code to compute (parts of) the Koszul dual of an operad. Or maybe try to compute something like (parts of) homotopy pushouts and pullbacks of simplicial sets.
Gershom (Mar 27 2020 at 20:55):One very simple exercise that might grab you is coding up something like the quadratic sieve. You could also start exploring doing simple computer algebra, like writing a library for manipulating polynomials, or given a concrete description of a structure, checking if it satisfies the axioms of a ring, etc.
Jonathan Beardsley (Mar 27 2020 at 20:57):I seem to recall there being some kind of book or library written up about programming and operads, but I don't know what/where it is/was.
Stelios Tsampas (Mar 27 2020 at 20:57):I think you ought to take a look at Cubical Agda :) (https://agda.readthedocs.io/en/v2.6.1/language/cubical.html, https://github.com/agda/cubical) or HoTT-Agda (https://github.com/HoTT/HoTT-Agda). There are similar attempts in other theorem provers.
sarahzrf (Mar 27 2020 at 20:58):hey!
Jonathan Beardsley (Mar 27 2020 at 20:59):HEY
sarahzrf (Mar 27 2020 at 20:59):do you have any interest in programming language theory per se? or mostly just picking up the pragmatic skill of being able to get computers to do stuff
Jonathan Beardsley (Mar 27 2020 at 20:59):Both I think. But as always, I basically don't have time to do anything these days unless I can turn it into something of the form "This would be cool to figure out and play with."
sarahzrf (Mar 27 2020 at 21:00):wait a sec, is this
sarahzrf (Mar 27 2020 at 21:00):oh lmao i didnt recognize you
Jonathan Beardsley (Mar 27 2020 at 21:00):yes. it is I.
sarahzrf (Mar 27 2020 at 21:03):hmm, completely random thought, you might enjoy trying out the diagrams library for haskell
sarahzrf (Mar 27 2020 at 21:05):image.png
image.png
you can use it to make drawings like this
sarahzrf (Mar 27 2020 at 21:06):except that unlike tikz or whatever, it's actually great
Jonathan Beardsley (Mar 27 2020 at 21:06):O those are pretty.
sarahzrf (Mar 27 2020 at 21:06):(those are from brent yorgey(the library creator)'s dissertation (on combinatorial species))
sarahzrf (Mar 27 2020 at 21:08):it's built on a whole set of Actually Thought-Out Abstractions instead of commands for moving shapes around or whatever
sarahzrf (Mar 27 2020 at 21:08):like, the kinds of objects ("objects" in more of a "mathematical object" sense than an "object oriented programming" sense) that you manipulate have sensible geometric behavior and are nicely compositional in many ways
sarahzrf (Mar 27 2020 at 21:10):and there are very smart distinctions drawn, like having a type for a path vs. a type for a path associated with a particular origin in space
sarahzrf (Mar 27 2020 at 21:11):which have the same inhabitants, but different instances for overloaded operations like "translation"
sarahzrf (Mar 27 2020 at 21:12):also, vitally, diagrams are actual values
sarahzrf (Mar 27 2020 at 21:12):it's not some kind of window onto a drawing API that lets you say "draw a circle here, then a square there"
Jonathan Beardsley (Mar 27 2020 at 21:13):oh that seems nice.
sarahzrf (Mar 27 2020 at 21:13):rather, "a diagram comprising a square" is a value you can carry around, and "a diagram comprising a circle" is another, and then you can put them next to each other to make a bigger diagram if you want, and then write a function which builds a big one
sarahzrf (Mar 27 2020 at 21:15):yeah, it occurred to me to mention it because i was thinking about what kinda stuff you might want to try writing by thinking back thru what projects ive done, and i remembered one where i built up a bunch of machinery for talking about compact closed category gadgetry, and part of it was drawing stuff using diagrams
sarahzrf (Mar 27 2020 at 21:17):so like, guessing from the fact that you're a geometer that there's probably slightly better than even odds that you like pretty pictures, maybe youd find it handy to be able to programmatically build up this kind of illustration
Jonathan Beardsley (Mar 27 2020 at 21:18):yeah, i dunno if i'm a geometer, but sure. might be good motivation for learning the basics of haskell.
Jonathan Beardsley (Mar 27 2020 at 21:18):really i think i just wanna make a data type called "operad"
sarahzrf (Mar 27 2020 at 21:18):hmm, homotopy theory is surely geometry
sarahzrf (Mar 27 2020 at 21:18):image.png
(here's the kind of thing i was using diagrams for in that compact closed category project)
Jonathan Beardsley (Mar 27 2020 at 21:20):well, whether or not homotopy theory is geometry is a conversation for another thread i think ;-)
sarahzrf (Mar 27 2020 at 21:25):anyway, here's a little diagrams poem for u https://gist.github.com/sarahzrf/08ddbe732965dc4b97691843500f5d8d
sarahzrf (Mar 27 2020 at 21:28):let us ponder the mystery of the catalan numbers :ghost:
sarahzrf (Mar 27 2020 at 21:32):oh hmm i had an idea :thinking:
sarahzrf (Mar 27 2020 at 23:02):after a bunch of false starts, here is my idea https://gist.github.com/sarahzrf/a65917c4b6826e85753662e1145750e8
Jonathan Beardsley (Mar 27 2020 at 23:57):What is this idea. I can't read code.
sarahzrf (Mar 28 2020 at 00:11):just look at the picture
sarahzrf (Mar 28 2020 at 00:13):it is the little discs operad, as far as i understand it
sarahzrf (Mar 28 2020 at 00:14):or, well, a very very loose approximation
Faez Shakil (Mar 28 2020 at 00:54):sarahzrf said:
after a bunch of false starts, here is my idea https://gist.github.com/sarahzrf/a65917c4b6826e85753662e1145750e8
@sarahzrf how are you running an ipynb with haskell??? I miss the clarity of thought afforded by those from my emacs terminal!
sarahzrf (Mar 28 2020 at 00:54):it's "ihaskell"
sarahzrf (Mar 28 2020 at 00:55):a haskell kernel for jupyter
sarahzrf (Mar 28 2020 at 00:55):absolutely killer way to use diagrams
Faez Shakil (Mar 28 2020 at 00:58):Jonathan Beardsley said:
really i think i just wanna make a data type called "operad"
@Bartosz Milewski has a very patient blogpost about building decision trees over a tic-tac-toe algebra. There's a monadic implementation linked in the intro that I found an easier example to get started with than the co-monadic one used in the post.
https://bartoszmilewski.com/2015/10/07/operads-type-level-nats-and-tic-tac-toe/
Faez Shakil (Mar 28 2020 at 01:06):Diagrams looks awesome. Do you run the kernel against ghci or is there a docker image? I've had trouble setting it up for one reason or the other in the past
sarahzrf (Mar 28 2020 at 01:15):i'm not sure what you mean by "run the kernel against ghci"
Faez Shakil (Mar 28 2020 at 01:16):sarahzrf said:
i'm not sure what you mean by "run the kernel against ghci"
Sorry I mean does ghci do what an ipython kernel usually does in python terms?
sarahzrf (Mar 28 2020 at 01:16):ihaskell is what does that
sarahzrf (Mar 28 2020 at 01:17):you're familiar with jupyter or only ipython?
Faez Shakil (Mar 28 2020 at 01:17):Both, I once tried living in jupyterlab which was nice but strangely unproductive.
sarahzrf (Mar 28 2020 at 01:18):ihaskell is a haskell kernel for jupyter
sarahzrf (Mar 28 2020 at 01:18):ghci by itself cannot talk to jupyter afaik
Faez Shakil (Mar 28 2020 at 01:19):Ah yes you'd need a layer in the middle wouldn't you.
Faez Shakil (Mar 28 2020 at 01:29):Also this (from www.github.com/conal/concat) is generated from a very similar thing to what you are doing extended to affine transformations and their derivatives!
sarahzrf said:
image.png
(here's the kind of thing i was usingdiagramsfor in that compact closed category project)
sarahzrf (Mar 28 2020 at 01:37):"extended to"?
sarahzrf (Mar 28 2020 at 01:38):also actually i have some thoughts on compiling to categories :-)
sarahzrf (Mar 28 2020 at 01:38):but compact closed categories are orthogonal to cartesian closed ones
sarahzrf (Mar 28 2020 at 01:39):i don't think i'd call it "extended" so much as just different
sarahzrf (Mar 28 2020 at 01:39):although the graphics look a lot more working!
Faez Shakil (Mar 28 2020 at 01:41):Uh I am generally very ignorant about categorical abstraction but there's support for compact closed categories too I think if you define enough instances. Would a Braided Monoidal Product Category be compact closed?
Faez Shakil (Mar 28 2020 at 01:41):and Symmetric
sarahzrf (Mar 28 2020 at 01:42):a compact closed category is a symmetric monoidal category where every object has a dual
sarahzrf (Mar 28 2020 at 01:43):"dual" in a sense which generalizes that of the dual of a finite dimensional vector space
sarahzrf (Mar 28 2020 at 01:44):a ton of the characteristic features of FinVect can be derived from it being compact closed
sarahzrf (Mar 28 2020 at 01:44):another category that's compact closed is Rel
Faez Shakil (Mar 28 2020 at 02:14):Yes so what I loved about concat was that you can work with vector spaces and even build neural networks with all their interesting compositions of linear maps and relus and have everything be translated from a category which just has to fulfill HasRep and HasV instances and you get all the properties you need for Rel or Aff or AffLagRel
sarahzrf (Mar 28 2020 at 03:26):anyway @Jonathan Beardsley @Faez Shakil check out the diagrams tutorial https://archives.haskell.org/projects.haskell.org/diagrams/doc/quickstart.html and/or manual https://archives.haskell.org/projects.haskell.org/diagrams/doc/manual.html
sarahzrf (Mar 28 2020 at 03:26):it's just excellent software with great documentation
sarahzrf (Mar 28 2020 at 03:26):it makes me happy inside knowing documentation like diagrams's exists
Gershom (Mar 28 2020 at 04:23):setting up ihaskell can be a bit irritating, but you can run it in the browser, free using https://cocalc.com/
sarahzrf (Mar 28 2020 at 04:25):"a bit irritating" 🩸
Gershom (Mar 29 2020 at 23:45):Earlier, @Jonathan Beardsley asked how to represent simplicial sets in functional programming. I have an old blog post I dug out and revived where I gave one (nice, categorical) approach in Haskell that people may find of interest: https://gist.github.com/gbaz/ff92e63968d32e0ae92ecbb44f0677b8
One could also take a purely combinatorial approach, which would be less elegant, but perhaps lend itself more to doing some actual work with these things. Mainly, when I look at libraries for computational homology I've seen simplicial complexes, or even just flag complexes which are much more straightforward to represent in their "raw" form.