On Sun, Jun 17, 2012 at 9:51 AM, Elias Gabriel Amaral da Silva < [email protected]> wrote:
> On Sat, Jun 16, 2012 at 6:11 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > > The platform-specific implementation type is not (and should not be) > > revealed, but > > We need to know that type in order to stack-allocate an instance. > > You don't, you need to know only its size. This means that a formal > proof that your type has size N is enough (even if N is only known at > run time), and then you pass this N to alloca. > Umm. Yes. I mis-spoke. To allocate, I agree that you only need to know the size. But to pass the resulting object back into a later procedure, you need enough information to check type agreement at the procedure call boundary. > If you language has the notion of "the kind of all types whose > representation has size N", you can encode this pattern on the > language (and let the user prove that each concrete type in fact is of > this kind). I think this would require dependent typing. > That sort of kindling is doable. In this peculiar case, it doesn't require dependent typing, because sizes are concrete natural numbers. We can avoid dependent typing by introducing a Nat kind and then re-introducing 1, 2, 3, ... at the type level. But as I say above, this wouldn't be enough to check for type agreement when the allocated object is passed back in. Though now that I think about it, full type agreement may not be required. We're only going to be passing around a pointer to the supertype (the generic interface), and we *do* know the type of that. I *think* that reduces the problem down to ensuring that stack region safety is not violated. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
