Hacker News Reader

Comment by macromagnon | Hacker News Reader

I've been wanting to go towards category theory, homotopy type theory, etc. but I realized I need more abstract/algebraic geometry and then I need some topology, etc before category theory so I have more examples of morphisms to draw from.

Right now I'm mostly studying linear algebra and some combinatorics. Very interested in linear operators and the relationship between differential/finite difference operator, falling/rising factorials, stirling numbers, bernoulli numbers, etc.

I'm hoping math will get me a more interesting job than java programmer but I enjoy the math for its own sake anyways.

View on HN

I would strongly recommend looking at “standard” dependently-typed theories and languages (or even proof assistants without dependent types), instead of trying to plunge into homotopy theory. Learning how dependent types work will be much more illuminating than trying to catch up on the algebraic topology. While the link between topology and formal logic is certainly interesting, I think you’ll be much better served by starting on the logic side of things.

Software Foundations is a well-known book / series of Coq programs for theoretical computer science. [1]

Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems.

Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read and actually enjoyed :)

[1] https://softwarefoundations.cis.upenn.edu/

[2] Available for free here (1 MB pdf) https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard....

[3] https://www.manning.com/books/type-driven-development-with-i...

Seconded, but it might be worth learning a language with algebraic data types first (such as Haskell or OCaml).

Thanks for this very helpful comment which I've bookmarked for the links. Could I ask you for any more recommendations?!

I have background in standard undergrad math (linear algebra, calculus, real analysis, etc) and some basic undergrad CS, and I work as a software engineer (backend web stuff). However I've never really studied formal logic, or theoretical CS, or formal methods / verification, or type theory, and I was thinking of doing so. I enjoy studying math/theoretical things for its own sake, but I am of course also interested in techniques which might touch upon software engineering in practice.

Do you have any opinions on whether I am proposing something at all sensible for myself, and if so what sort of order to take things in?

Any recommended sources of exercises to work on (with solutions? seeing as I might well be self-studying)

Or lecture courses, or anything available online (even if it costs money)

Online communities you'd recommend for asking for help, e.g. with problems encountered in self-study?

And any more recommended books/lecture notes of course.

Disclaimer: I am not a domain expert in type theory and my background is algebraic combinatorics, not computer science. I also hate online courses, don’t like collaborative learning, and tend to read books and papers by myself. So I’m not a great source of advice for most people.

Unfortunately I don’t have many more suggestions that would be good pedagogically. Benjamin Pierce (who wrote Software Foundations) has another very famous intro book, Types and Programming Languages: https://www.cis.upenn.edu/~bcpierce/tapl/ which is regarded as a “Bible” of type theory for computer scientists. Note: I haven’t personally read this, but I have read the sequel, Advanced Types and Programming Languages. Both books have exercises and most exercises have solutions.

Simon Peyton-Jones wrote a very good book, the Implementation of Functional Programming Languages. It is old (1987), but free, a good read, and covers most of the “important” topics without assuming too much background: https://www.microsoft.com/en-us/research/publication/the-imp...

For formal verification - there are definitely better-qualified people than me. I found a lot of the source code to CompCert C (a verified C compiler) illuminating: https://github.com/AbsInt/CompCert However, it will be difficult to understand without doing Software Foundations first (I still find personally tactics-style proofs in Coq confusing and don’t like Coq as much as Idris or Agda).

I am very shy and can’t help you with the online communities :) The type theory subreddit is pretty active and they seem nice.

Great, thanks again! One more question: I imagine that it's not very important exactly what one picks as a beginner, but is Lean something which one might weight against Idris as something to start with, or would one get very different things out of learning about (and how to use) those?

I'm afraid homotopy type theory has zero relevance towards anything related to applied programming at this stage, especially if you are not already an academic doing PHD-level research.

if you want to learn some functional programming along with abstractions actually used in FP programming, that is one thing, but that is not homotopy type theory, which is squarely in the domain of purely abstract mathematics which would be interesting from a pure mathematics perspective, not a programming perspective.

The paper does appear to include some proof that utilize Coq, but unless you're interested in software that checks the validity of mathematical proofs, that is not going to help you get a more interesting programming job.

If you're a programmer, I wouldn't worry too much about examples of morphisms from math (unless you're interested in the math for its own sake). You already know tons of morphisms -- every function in any programming language is a morphism (e.g. square x = x * x is a morphism Num -> Num).

By the way, if you're interested in categories, you might like this post about using monoids for GPU parsing: https://raphlinus.github.io/gpu/2020/09/05/stack-monoid.html

(Monoids are the simplest examples of categories)

Suggestion: Don't follow advice not to read something.

Reply on news.ycombinator.com