On Wed, Jul 2, 2014 at 6:31 PM, Geoffrey Irving <[email protected]> wrote:
> Languages with typical polymorphism have values that are all the same
> shape in that sense, typically just a pointer.
>
Not necessarily. BitC and C# stand out as counter-examples, because both
have explicitly unboxed types, and you can use those types as type
parameters.
What *is* true is that all of the sizes and offsets are known at static
compile time. That ceases to be true with dependent types, even in the
constrained virulence that I am contemplating. Given "constructions over
literals", you could well see a procedure like:
fun f(i: Nat, vec : 'a[i])
where you do not know the size of /vec/ at compile time, but you know that
the size will be fixed and that you will have it available at link time. It
raises interesting problems for placement of objects on heap v. stack, and
it changes how you think about sizeof(). sizeof('a[]) is an error.
sizeof('a[i:Nat]) is well-typed, but not computable until all types are
bound. The interesting question is whether we allow cases where we really
won't know /i/ until runtime, either because we want to take that step or
merely because we want to compile for code reuse (in which case we may need
to generalize the implementation of /fun/).
> 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.
>
Conceptually it hasn't changed, and it can't because of unboxed types.
There are various points in the continuum between unit-of-compilation time
and run time where that expansion can occur. The hard requirement is that
it can be checked early, and that it be *possible* to pre-expand everything
in the absence of dynamically introduced types (e.g. through dynamic
loading). So, for example, I don't want to have to put a run-time code
generator into an operating system kernel.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
