You don't know all the types at compile time with polymorphism either, if I understand what you mean. So I don't think that's the issue.
On Wed, Jul 2, 2014 at 8:00 PM, Geoffrey Irving <[email protected]> wrote: > 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
