Think about generics in any language, say Java Stack&lt;String&gt;. The type Stack is parametrized by the type String. What would you do in a language without generic types? To achieve the same effect, you&#x27;d need to create a custom StackString type, which itself is trivial. But then, you&#x27;d need StackInteger, StackBoolean, StackSomeoneElsesCustomType, etc.<p>Language with a type system but without generics have this above downside. Usually you&#x27;d just give up making a type for each of these, and simply use the Stack type.<p>Language without Idris-like dependent types suffer the same downside: instead of creating Stack&lt;String, n&gt;, you&#x27;re forced to create Stack&lt;String, One&gt;, Stack&lt;String, Two&gt;, Stack&lt;String, Three&gt;, where One&#x2F;Two&#x2F;Three are unique types you created to conceptually represent a number. If you don&#x27;t even have generics, you&#x27;d need to create StackStringOne, StackStringTwo, ...<p>Dependently typed languages encode numbers (among others) as unique types, to simplify. Imagine this:<p><pre><code>  put: Stack&lt;String, Three&gt; -&gt; String -&gt; Stack&lt;String, Four&gt;
</code></pre>
This isn&#x27;t too hard to imagine is it? No runtime checks needed. Once you get the output you can carry it around, along with its type, to places that accept Stack&lt;String, Four&gt;.<p>So, asking &quot;how come you don&#x27;t have to generate these checks at runtime?&quot; is similar to a programmer who&#x27;s never seen generics asking &quot;how come you can parametrize? Don&#x27;t you have to generate all the StackString and StackInteger, etc.&quot;. It just works. Hope that analogy was clear =).<p>Dependent types in general blur the line between values and types, as you&#x27;ve seen above. Think of the usual values you use, and imagine having a new type to represent each one. Dependent types let you do this in a sane and logical way.