Meh, it's like this: You have values. Then you have types. You can modify values, you can't modify types. If you want to modify types, then you need a third t

Meh, it's like this: You have values. Then you have types. You can modify values, you can't modify types. If you want to modify types, then you need a third thing, let's call it 'kinds'. Then if you want to modify kinds, then you need a forth thing. That's when you realize oh, why not just have types be same as values - you've now arrived at dependent types :) If you're curious about this sorta thing - play with Idris (the language) for a few days. It's the most approachable dependent type system in a friendly package that I've seen.