On Thu, Jul 3, 2014 at 3:19 PM, Geoffrey Irving <[email protected]> wrote: > On Thursday, July 3, 2014, Jonathan S. Shapiro <[email protected]> wrote: >> One thing you said concerns me: >> >>> We would likely not want a compile time system >>> that is strongly normalizing, which means we have to essentially run >>> the compile time portion of the evaluation in a checked interpreter, >>> which means we don't need to worry about Girard's paradox, which means >>> Type : Type is fine. >> >> I'm not so sure about that. I'm concerned that if we give up strong >> normalization, we lose structural type equality. > > This worries me too, as noted in the other email.
I don't see how this ruins structural type equality. It just seems like sometimes the compiler would go into a loop trying to figure out type equality. This de facto means the program was ill-typed. I agree that even the compile-time language should not be strongly normalizing, because this rules out efficient implementations of some (compile-time) algorithms. Weakly normalizing is actually OK, if you're willing to pay with termination proofs. But I don't see a need for that either. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
