On Wednesday, July 2, 2014, Matt Oliveri <[email protected]> wrote: > 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.
I was responding to shap's concern that in dependent types you don't know the shape of values at compile time (their size, for instance). Languages with typical polymorphism have values that are all the same shape in that sense, typically just a pointer. When that breaks down, such as for float arrays in ocaml, you have to make up the difference with runtime type checking. That is, if you pull an entry out of a polymorphic array in ocaml, a runtime check is required to know whether it needs to be reboxed. If bitc were to have full dependent types with no runtime / compile time separation, as well as full support for unboxed values, that issue in ocaml would become the norm. You're correct that it's already the norm even with simple polymorphism, but at least an earlier version of bitc did template-like instantiation to push the problem to compile time. I do not remember whether that's changed. Geoffrey > On Wed, Jul 2, 2014 at 8:00 PM, Geoffrey Irving <[email protected] > <javascript:;>> wrote: > > On Wed, Jul 2, 2014 at 4:18 PM, Matt Oliveri <[email protected] > <javascript:;>> 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] > <javascript:;>> 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] <javascript:;> > http://www.coyotos.org/mailman/listinfo/bitc-dev >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
