Might be hard to approach but my favorite is Pierce's "Types and Programing Languages":
https://www.cis.upenn.edu/~bcpierce/tapl/ (known as TAPL). Was grateful to take a graduate level class using it in college.
https://www.cs.cmu.edu/~rwh/pfpl.html
It’s far more directed than TAPL, so I think it’s easier to read from start to finish. TAPL feels better as a reference.
What type does is to have a set of classes of data, then have rules between those classes. You then annotate your code with those classes (combining them if it's possible) and then your type system can verify that the relations between them hold. To the type system, your program is data.
There is a clever way to encode Turing machines into Diophantine equations, so Diophantine equations (linear equations