I want to understand Julia type system, I need some guide for this quest

Internals & Design
1

I must say that I’m intrigued by Julia type system and I want to understand it more. In particular I want to understand works like this of prof. Jan Vitek and his collaborators mentioned in his 2021 JuliaCon keynote and newer papers like _ Decidable Subtyping of Existential Types for Julia_ published in 2023, but I lack a background for it, so I want to ask for help. What material should I studied to get into this topic? I assume I should now some solid type theory, but I don’t know where to start.

I’m person that is very found of logic, mathematical logic and math in general, so I would prefer resources that emphasis rigour and formal structures, not something that is easy for beginners. Even if this first route cost me more sweet, I strongly believe that I will gain much more from it. At this moment price of books and related materials is secondary thing to me, quality is the most important factor.

2

You can have a look at [1209.5145] Julia: A Fast Dynamic Language for Technical Computing (written by language authors, so that should be a start, I guess), [2310.16866] A Type System for Julia, etc.

3

I found “Julia Subtyping: A Rational Reconstruction” delightful.

4

Perhaps it’d be better to first read the Julia-related papers, trying to understand them as much as possible on the first read, and only then reach for more general literature. It could also be a good idea to ask specific questions here on Discourse.

NB: keep in mind that all of these papers only describe simplified versions of the actual mechanisms as defined by the reference implementation.

5

Please note that while the general mechanism of the type system continues to work, the exact mechanism of the type system might change over time.