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. 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. Actually. Hmm. Now that I see your next messages, I think I am wrong. (but I don't know how exactly I'm wrong) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
