On Thu, Jul 3, 2014 at 10:55 AM, Geoffrey Irving <[email protected]> wrote: > On Thu, Jul 3, 2014 at 10:25 AM, Jonathan S. Shapiro <[email protected]> wrote: >> On Wed, Jul 2, 2014 at 6:31 PM, Geoffrey Irving <[email protected]> wrote: >>> >>> Languages with typical polymorphism have values that are all the same >>> shape in that sense, typically just a pointer. >> >> >> Not necessarily. BitC and C# stand out as counter-examples, because both >> have explicitly unboxed types, and you can use those types as type >> parameters. > > Sorry, by "typical" I sloppily meant languages where that isn't the case. :) > >> What is true is that all of the sizes and offsets are known at static >> compile time. That ceases to be true with dependent types, even in the >> constrained virulence that I am contemplating. Given "constructions over >> literals", you could well see a procedure like: >> >> fun f(i: Nat, vec : 'a[i]) >> >> where you do not know the size of /vec/ at compile time, but you know that >> the size will be fixed and that you will have it available at link time. It >> raises interesting problems for placement of objects on heap v. stack, and >> it changes how you think about sizeof(). sizeof('a[]) is an error. >> sizeof('a[i:Nat]) is well-typed, but not computable until all types are >> bound. The interesting question is whether we allow cases where we really >> won't know /i/ until runtime, either because we want to take that step or >> merely because we want to compile for code reuse (in which case we may need >> to generalize the implementation of /fun/). > > If you're okay delaying such calculations until link time, I'd argue > that the cleanest way is to have full dependent types with the runtime > / compile time striation added as an extra constraint. This means (1) > all the theory works, (2) everything is fast once you get to the final > compile step (even that is "link" time), and maybe most importantly > (3) the language and grammar are extensible to full dependent types > with runtime and compile time mixed if someone wants to implement that > later on. > > I don't think adding this striation to a dependent type system is > particularly difficult: there's usually a different kind of striation > already in place due to universe levels, and from various accounts > that I've seen this poses only mild difficulties. Indeed, if we went > this route, the system would probably be strictly simpler than full > support for universes. 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 realize the above may be outside the scope of bitc, and certainly > requires compilation to become undecidable in the sense of "easy but > nonterminating". I personally don't think this is a problem, but we > seem to differ on this point. :)
By the way: the reason I don't think this is a problem is that the compiler can just give up after a while and say "I'm not sure". I don't see how this pragmatic solution differs from standard Hindley-Milner eating all the RAM in the universe due to exponential blowup even with a simple decidable type system. Geoffrey > 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. I've written a prototype interpreter with > otherwise Haskell-like syntax where this is the case, and if I recall > correctly the only problem was the ambiguity of > > let f x = y > > In the language I was writing there was no grammar separation between > constructors and variable names, so unlike Haskell there was an > ambiguity between defining a function and pattern matching on a > constraint. Though now that I write this it doesn't seem to be > related to terms vs. types at all, so maybe there isn't a problem. I > can look up how we worked around the ambiguity if you're curious, > since I don't remember the resolution offhand. > >>> At least an earlier version of bitc did template-like instantiation to >>> push the problem to compile time. I do not remember whether that's changed. >> >> Conceptually it hasn't changed, and it can't because of unboxed types. There >> are various points in the continuum between unit-of-compilation time and run >> time where that expansion can occur. The hard requirement is that it can be >> checked early, and that it be possible to pre-expand everything in the >> absence of dynamically introduced types (e.g. through dynamic loading). So, >> for example, I don't want to have to put a run-time code generator into an >> operating system kernel. > > Great. > > Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
