If Scala syntax is more up your alley, here's an intro to dependent types that has more Scala-esque syntax: https://shuangrimu.com/posts/language-agnostic-intro-to-depe...

Scala has only a very limited version of dependent types. Even its "dependent function types" are a more restricted version of general dependent function types. Full dependent types can in a certain sense be even simpler than non-dependently-typed languages (e.g. you no longer need a separate notion of generics).