&gt; I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file. You cannot apply directly any of the size-aware functions, because it will not typecheck.<p>Yes, you can in fact do that! Let&#x27;s assume you&#x27;re building the list you&#x27;re reading from a file as if it were a linked list. That&#x27;s the point of dependent types -- the types can (and often do) depend on run-time values.<p>EDIT: I suppose I should expand on this a bit. The idea is that the &quot;read-Vec-from-file&quot; function can look like this:<p><pre><code>    readVecFromFile :: File -&gt; (n, Vec n Int)
</code></pre>
(let&#x27;s say it&#x27;s reading Ints)<p>So the readVecFromFile function will return you a run-time value &quot;n&quot; (the number of items) and a vector which has that exact length. When <i>using</i> readVecFromFile, you&#x27;d do something like<p><pre><code>    (n, v) &lt;- readVecFromFile
</code></pre>
and you&#x27;d be absolutely free to call any function which expects a vector of any length. (If necessary you could also supply the actual length, but that&#x27;s just a detail.)<p>The implementation of readVecFromFile is left as an exercise, but it can be done. One idea is to start with the empty vector (length 0) and an &quot;n&quot; of 0 -- and then to just accumulate into it, all the while keeping a &quot;proof&quot; that the length of the vector is way the runtime value says it is. (Using structural induction, basically, to build a proof that the runtime value is the same as the length of the vector.)