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. > This worries me too, as noted in the other email. 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. > I think it has to be coq, for the key reason that it will give you the best sense where defaulted and hidden type arguments and how we might handle those in bitc. This may be the biggest stumbling block. I'd work through at least part of Adam Chlipala's book. The issue is that in languages like Haskell, all type arguments to polymorphic functions are kept separate, and are always inferred. We would like to preserve this for functions that aren't doing fancy dependent type stuff. In coq, though, the polymorphic identity function looks like Inductive id t (x : t) : t := x. That is, the type parameter is explicit in the definition. Coq then has some frontend machinery for filling in these arguments, so that users of id don't need to pass both arguments. Coq's solution works quite transparently in practice, after the initial function definition. In the prototype language I played with for a while, all functions effectively had an extra type argument for each explicit argument, and a similarly thing could likely work for bitc if we decide coq's machinery is too much. This would make let id x = x map to the coq version above. The next concern is how this works when you mix function definitions and type annotations. I think it will take a bit of thought to get right, but coq is a good example to pull ideas from. Geoffrey > 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. > If + is overloaded, I don't think there's a problem here. + acting either on compile time naturals vs. integers is no different than + acting on float vs. double. > 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 > I'm all for anything that pushes towards multivariable type classes, as long as there's a clean solution. :) Geoffrey
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
