On Thursday, July 3, 2014, Jonathan S. Shapiro <[email protected]> wrote:
> 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. > 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). Not that all possible compile-time computations terminate. That means, in practice, they are willing to specify/increase a computation budget if needed. I believe recent extensions to Haskell have eventually taken this approach. > > >> 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
