category theory or lambda calculus - General

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Mason Mackaman

Which one improves ones FP ability more?

TheMatten

LC is to FP languages what Turing machine is to imperative languages - it's minimal model through which languages can be built and studied
CT is branch of mathematics interested in composition - that's something close to principles of FP upon which many patterns are built, but it's not directly related to LC (except that as with many other constructs, it provides it's generalization)

Vladimir Ciobanu

My experience has been that LC can bring some pretty immediate gains (i.e., you can read an article, or a book, and you get quite a bit out of it, especially if you're interested in type systems, languages, etc.). CT feels like a longer term thing. The gains aren't as immediate, you need to put in a lot more effort. BUT, it seems like you also tend to get a lot in return, later. Also, it seems like a bottomless pit that keeps on taking time but giving back cool abstractions.

I would say, have a look at LC. It's fun and doesn't take nearly as much to get a hang on than CT. Then, if you like CS, abstract thinking, etc., take the plunge into CT.

Again, this is definitely an opinion and none of the above are facts.

James King

I agree, in my experience LC is much easier to learn and is, "well understood," in that there isn't a huge amount of active research in the area. CT is still growing and is a large subject already and has taken me much longer to get into.

Mason Mackaman

interesting, thanks for the insight. I've already started down the CT road myself. But I hadn't really considered the benefits I could get from studying LC. I think I'll switch it up for a bit and give it a look.

Sandro Pollastrini

CT is vast. The risk is to loose one self. However this does not mean that it is worthless, but it is similar to approach the theme algebra with the aim of learning linear algebra: if you take a classical algebra book (say Lang's), you will loose your self pretty soon and will not find any linear algebra. But if you start from the right book, you'll gain what you want.

Which book about CT and FP? Definitely: Bartosz Milewski's Category Theory for Programmers (free pdf on GitHub): it contains examples in Haskell and in C++ (there is also a Scala version of the book); you don't actually need to read it all: you read something, you apply something; you read another bit, you apply the new bit; ...

The same argument is true even for LC. LC is vast (not as CT), because it encompass the various versions of it (from the untyped to the type versions).
I personally found usefull understand the principles, considering that they underlying all FP, both the untyped and the typed versions. But you'll risk to loose a lot of time (e.g., Barendregt's The Lambda Calculus - Its Syntax and Semantics is beautiful, but it too deep and it is not clear what you'll gain from it if your aim is to be better at FP).

Which book about LC and FP? Simon Thompson's Type Theory and Functional Programming (free pdf): it gives you both untyped and typed versions, showing you even type theory, which one of the point of conjunction with CT. And it is short!

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source - hmemcpy/milewski-ctfp-pdf
Vladimir Ciobanu

I love Bartosz, but I am not able to learn CT from his book. It feels too loose in terminology / theory. It has great explanations for early stuff though.

Georgi Lyubenov // googleson78

for lc I can recommend Pierce's Types and Programming Languages, because it is somewhat "programming/implementation oriented" (e.g. it discusses aspects of LC that you need for implementing it, and it also has an ocaml (iirc) implementation of the discussed topic at the end of some chapters)

Vladimir Ciobanu

I can second that. I also found Type Theory and Formal Proof to be excellent, especially if you want a more logical/formal approach than Pierce's CS/practical approach (https://www.amazon.com/Type-Theory-Formal-Proof-Introduction/dp/110703650X).

Sandro Pollastrini

Vladimir Ciobanu said:

I love Bartosz, but I am not able to learn CT from his book. It feels too loose in terminology / theory. It has great explanations for early stuff though.

Yes, I can see your point. But it is exactly the point of the book: to give you the most intuitive way of thinking to the FP stuff through the CT intellectual machinery. This could be a good entry point (which is what probably Mason asked about) to give basic concepts (already useful in FP context, expecially Haskell/Scala) and terminology.

Furthermore, the book goes way beyond the basics.

You can always help the reading with other books more specifically CT oriented, as Pierce's Category Theory for Computer Scientists (even if my favourite is Awodey's Category Theory, which is for me the right level of difficulty).

Vladimir Ciobanu

I would say Bartosz' book (and video series) are quite good up until limits. It seems to get a bit hairy after that, at least IME. OTOH, I guess part of the idea is to do a ton of exercises and exploring on one's own, which I have not done.

Sandro Pollastrini

You got me thinking to the exercises, and in fact I think that Bartosz's book would benefit from an expansions: some good exercize (with solutions!) would have been great!

Sandro Pollastrini

Vladimir Ciobanu said:

I can second that. I also found Type Theory and Formal Proof to be excellent, especially if you want a more logical/formal approach than Pierce's CS/practical approach (https://www.amazon.com/Type-Theory-Formal-Proof-Introduction/dp/110703650X).

Didn't know about this book of Nederpelt and Geuvers! Cool!