On Fri, Jul 4, 2014 at 3:21 AM, Gabriel Dos Reis < [email protected]> wrote:
> > One thing I've found is that programmers (as opposed to type theoretists) > don't really care about strong normalization. They care that the > computation they are doing at compile time is terminating (or not).... > I tend to agree. The only reason that I am tentatively holding on to strong normalization is that it induces a simple theory of type equality. Though I'm not entirely convinced that we will turn out to need that. I suspect that in our use cases it will turn out that the compile-time operations on types will turn out to be limited to construction and destruction/inspection. That doesn't guarantee strong normalization, but I suspect that normalized results will tend to emerge from the [human] use of these two operations. I also suspect that concerns about equality will end up to be sufficiently covered by unifiability and subsumption. We'll see, I guess. :-) shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
