On Fri, Jul 4, 2014 at 4:12 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Fri, Jul 4, 2014 at 12:30 PM, Matt Oliveri <[email protected]> wrote: >> Since when is 3 a type? > > The literal 3 is a value that inhabits the type 3 (among others), which in > turn inhabits Nat. The ambiguity is intentional; it's the key to literal > types.
Ah. So in other words, the type level nats _are_ the singleton types. Yeah that makes things trickier. And it's also true that List is both a type constructor and a list constructor? In that case, it seems like you have no choice but to know going in whether you want a type or not. Have you read about bidirectional type checking? It can use a lot of top-down type propagation to help disambiguate things. > The tricky bit is that [singleton constraints are] likely to cause value > dependencies to start showing up in type qualifications, and then we need to > think about how far we want to let those propagate. If we let them propagate > too far they start showing up in top-level signatures, and at that point I > think we go over the line into dependent types. I don't see why that becomes dependent types. But it's not really important what it is if it's still too messy. It may be that the constraints would propagate everywhere if the inference engine always does the simplest possible thing (which is the right default). But if top level definitions are expected to explicitly say any constraints that are assumed, then you're effectively telling the compiler that those constraints should be sufficient in any case, and someone has to prove that this implies whatever the compiler wanted to know. Loops are also a sensible place to be explicit about constraints, drawing an analogy to Hoare logic and proof theory. >> Wait, are you saying you thought you were going to get away without >> constraints on type-level Nats and stuff? > > I don't think so. I'm saying that sooner or later we're going to get a > procedure that takes an array 'a['i] and an int /ndx/ that wants to index > into it, and we're either going to have to have a way to express the range > constraint in the type (which is a form of dependence) or we're going to > have to introduce a dynamic check so that the range constraint doesn't > escape into the external procedure signature. I see. But the range constraint is not really a dependence on the values, it's just depending on the type-level Nats for the length of the array and the value of the index. Oh! Is that all you meant by value? Huh, maybe you really can think of it as dependent typing for that reason. But no matter how you think of it, the important break we get is that we know we'll never have types depending on an impure computation. You can think of it as the purity of type-level computation forcing the purity of elements of singletons, or just directly as dependency on pure computations. >> Oh, now it looks like you're saying you can't get away without >> constraints, and that they will show up in the surface syntax. > > Yes. And I'm further saying that some of those constraints involve values, > so there may end up being places where terms appear as arguments to types. I agree. >> I'm taking about impure data structures here. Supporting unboxed types >> only when they're pure seems like an empty victory to me. Propositions >> as types does everything, but then the problem is keeping the proof >> burden tractable. > > OK. But unboxed != mutable. It'll probably help us to keep the lexicon > straight in this discussion. I'm well aware of that, but thinking that the major use case of unboxed types is low-level programming, I figured immutable unboxed types would not be of much practical interest. But I think I got confused. Are we saying that dependent, unboxed types themselves would have to be immutable (bad), or that unboxed values a type depends on would have to be immutable (OK)? I guess the latter, but for some reason, I was worrying about the former. (Now I'm worrying about constraints.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
