How do we overcome the compile time and runtime gap when programming in a Dependently Typed Language? : <p>I'm told that in dependent type system, "types" and "values" is mixed, and we can treat both of them as "terms" instead.</p>

<p>But there is something I can't understand: in a strongly typed programming language without Dependent Type (like Haskell), Types is decided (infered or checked) at <strong>compile time</strong>, but values is decided (computed or inputed) at <strong>runtime</strong>.</p>

<p>I think there must be a gap between these two stages. Just think that if a value is interactively read from STDIN, how can we reference this value in a type which must be decided AOT?</p>

<p>e.g. There is a natural number <code>n</code> and a list of natural number <code>xs</code> (which contains n elements) which I need to read from STDIN, how can I put them into a data structure <code>Vect n Nat</code>?</p>
