What *sort* of mathematical foundations are required to contribute to the research on modular implicits, typed effects, and the like?

Splitting off from this thread, which is getting a bit off-topic …

I’m “just” a dayjobber, but I have some meaningful experience with compilers and typesystems. Unfortunately, I have little-to-no solid mathematical background. (Failed out of Discrete a decade ago. :P)

I’ve been thinking a lot (last year or two) about ‘fixing’ that — picking up some of the mathematical background that I missed, ‘leveling up’ to properly follow the talks and papers I read on type-theory (and typechecker-implementation, haha) that I currently only barely understand.

Is there anything out there like an overview of that “background” that people keep saying ‘not enough people in the OCaml community have to work on this problem?’ Even if it’s years of learning to get there, something like a roadmap would be nice.

I’m sure this is a huge ask, because pretty much everybody assumes that you’d only ever possibly arrive at these problems via the same rigorous academic process that is the norm, with an advisor and whatnot … I’m aware I’m an outlier, in wishing to go this process on my own …

4 Likes

For others coming across this thread, although I’m intending this question to be more “if I’m laser-focused on contributing to OCaml’s research-base”, here’s some more-general resources I already know of to pass on:

2 Likes

In my experience: relatively little mathematical foundations are necessary to work with type systems for mainstream programming languages (as opposed to type systems for proof assistants, which prove consistency/normalization and are another class of beasts). You need to be comfortable with common notations to specify type systems by systems of inference rules, and you can get part of the way by reading the TAPL. In particular, you do not need any background on category theory or homotopy type theory.
Mathematics skills make people effective at describing their idea precisely and as simply as possible, and this is very helpful to communicate type-system ideas, but this is different from being familiar with specific mathematical theories, and perfectionist programming also gives strongly related skills.

What one does need on the other hand is good understanding of ML module systems (for modular implicits), type inference and effect systems (for effect typing) as they exist in the existing related work on programming language theory. And this, while typically not super elaborate mathematically, is still a lot of complex works to understand, and it takes a while.

And then there are some people who are very familiar with how things are formalized / described on paper (and reasoned about formally), but not with how they are implemented, and conversely people who can work their way through the OCaml type-checker implementation with ease (no small feat!) and have a very strong intuition of what would work or wouldn’t, but are not so good at publishing their proposed designs in a way other people can understand.

17 Likes