I keep hearing that, but I don't buy it. Whatever runs in the type checker is running at compile time. Do people really just mean that a given piece of code isn't necessarily uniquely destined for either compile time or runtime?
On Wed, Jul 2, 2014 at 3:19 PM, Geoffrey Irving <[email protected]> wrote: > In terms of your worry about shapes, the issue with dependent typing > is that there is no "now compile time is done" point in a fully > dependent typed language where you know what n is in Vec n a. That > is, there is no hard striation between compile time and runtime. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
