Geoffrey: I need to contemplate the rest of this, but you are saying things that feel right. I was already headed in the direction of a grammar that would leave options open for later on dependent types.
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. > As a compromise though, if you're concerned about future extensibility > to full dependent types, we definitely want to have the same grammar > for types and terms. That seems right. If you had to point me at *one* language to play with this a bit, what language would you suggest? I'm embarrassed to say that this class of languages is completely outside my experience. Oddly enough, mixfix concerns me a bit. I can readily imagine that we want different bindings for '+' at the expression level and the type level... Though perhaps this falls out through the combination of rank-n polymorphism and type classes. It's an interesting set of questions, anyway. And it *definitely* pushes us to multivariable type classes, because in (e.g.) "1 + 2" at the type level, + is a functor having type 'a x 'b -> 'c shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
