On Wed, Jul 2, 2014 at 4:18 PM, Matt Oliveri <[email protected]> wrote: > 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?
It is true that *type checking* runs at compile time, but it is not true in dependent typed language that type checking means you actually know all the types. Similarly, in a normal language type checking at compile time doesn't mean you know all the runtime values at compile time. You know the values will be safe, just like in dependent typed languages you know the types will be safe, but you don't know what they will be. Geoffrey > 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 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
