Haskell

Haskell book & Thinking with types are great intros to Haskell, type systems and Type-Level Programming in Haskell.

Notes

Kinds are the types of types. Typeclasses are more like predicates or relations between types.
The fewer type parameters in a class, the better. Can you turn any into associated types? Can you split the class into two classes? Can you hive off some of the parameters into a superclass?
Don't worry about strictness until it's time to optimize.
Intuition about optimization tends to be bad. Before profiling, limit yourself to reasoning about complexity classes.
Don't judge haskell based on these definitions. They appear strange and crazy, but when you actually do stuff most of them turn out to be quite intuitive.
- Advice is to ignore these things. Don't read a million monad tutorials. Just play around and code something, you don't have to understand the monad-definition before you can use the do-notation. Try to ignore them. After a while you get an intuition and then the definitions will make sense.
Objects are a way to generalize reusability and composability (Interheritance, Encapsulation, Polymorphism) Haskell goes down a different route of reusability and composability that draws more from math than from object models. The real benefit to learning haskell is learning to think in that way rather than an object oriented or imperative way.
In Haskell, you could say that the type system is a syntactic method for classifying program phrases according to the kinds of values they compute.
Because Haskell (usually) only evaluates into WHNF if you produce data constructors while doing the infinite recursion you can use infinite recursion.
If, while forcing a thunk, you see the same thunk being forced again, you can report infinite recursion.
GADTs might give you a radically simple way to express things that rudimentary type systems like Go's cant express.
Haskell's type system lets you express a lot of domain specific invariants and logic in a statically verifiable manner.
Go is as type safe as haskell, the language doesn't allow invalid operations on data types. What people mean with "weak" is often expressivity. Go's enums sucks and it doesn't have ADTs or generic.
- When people talk about strong type system, they usually just mean expressivity, not safety.