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.
Oops, I may need to withdraw the above paragraph. It works fine in the sense that if you passed link time everything is perfectly safe, since everything is now concrete, but it does not work in the sense that if Girard's paradox is possible in a simplified system with Type : Type, you might get type checking errors at link time. Geoffrey > 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. :) > > 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
