On Mon, Mar 2, 2015 at 10:26 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Mon, Mar 2, 2015 at 6:50 AM, Keean Schupke <[email protected]> wrote: >> >> I have a question. I import an arity-concrete function from 'C' that: >> >> test :: fn 2 'a 'b -> 'c >> >> I apply it like this: >> >> ((test 1) 2) instead of (test 1 2). >> >> Do I care? As long as the intermediate (test 1) is a temporary value (in >> the C++ sense), it does not cause any problems as it cannot escape, and gets >> the (2) applied to it right away. > > > In principle I agree that this is fine. In BitC it is a syntax error, > because you are relying on the optimizer to restore a correct concrete > application, and the optimizer may be entirely turned off. Also, your > "temporary" value allocates a closure object. You are tacitly assuming that > this can be stack-allocated, but nothing in the language semantics allows > you to do that. > > You are also teetering here on a different problem. You're arguing here that > a heap allocation can be moved to the stack by optimization. I agree that it > *can* be, and I agree that in this particular example that optimization can > be done 100% of the time. Separately, you ague that optimization must always > be non-semantic. It would follow that optimization should never alter the > types of things. But you are arguing here that we can justify eliding the > HeapAllocates effect on the basis of an optimization. I claim that if > optimizations are non-semantic, then the HeapAlloc effect cannot be removed, > even if we can perform this particular optimization 100% of the time. > > BitC *never* gets to rely on the optimizer to put things right.
But Keean never actually said "optimization", Shap. You did. An explanation of why we could allow that is that we say to coalesce applications chained via temporaries before inferring any types. This _resembles_ an optimization, and results in non-compositional typing rules. But it technically seems to be a valid, albeit very unconventional type system. Because the coalescing behavior is part of the type system, it cannot be turned off. My whole problem with Keean's proposal is that it seems increasingly like he's actually perfectly OK with this non-compositional style of type system, and that he's planning to rely on it very heavily. The first hint was when he said something about logical clauses for AST rewrites being used in his logic-programming-based type checker. I have argued against subtyping with unrestricted subsumption as a solution for arity specialization, but that proposal may have just been my imagination all along. Keean may be doing something far stranger. But I also argue against non-compositional typing rules. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
