Software Foundations (https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource.

The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.