On 3 May 2015 at 22:15, Matt Oliveri <atma...@gmail.com> wrote: > On Sun, May 3, 2015 at 12:00 PM, Keean Schupke <ke...@fry-it.com> wrote: > If you are thinking of type-level variables as things we'll find out > later in compilation, you are *severely* restricting the type systems > you can deal with. But in fact, this is exactly what modal staging > (see below) is for: explicitly calling for that restriction. >
In the type inference systems I have written, you need a ground type for all type variables to allow the program to compile. The only exception is existentials, where you pass the witness at runtime. This is not some coincidence but a fundamental property, and precisely why you need a witness at runtime for existentials but not for any other type. Well what would you take as proof of my claim? I could point you to > some research about the two topics, and you could see for yourself > that they're talking about different things. Would that be good > enough? > Well, lets just say convince me then. I've already referred you to Pure Type Systems, which are standard > background for understanding distinctions like stratified vs. > dependent. (And also predicative vs. impredicative vs. inconsistent, > impredicative vs. ranked polymorphism, propositional vs. predicate > logic, and maybe more.) > I am not saying that there do not exist type systems which do not have the relationship between strata and phasing. Dependent types are the obvious counter example. Frank Pfenning did some cool stuff with staging using modal types. > There was/is also Meta OCaml or Meta ML or something, which looked > like it might be similar. It was a while ago that I looked into > this... > Staging is unnecessarily complex, and not really what i am talking about. Certainly not multiple stages. I am talking about something like C++ templates, or Ada's Generics, but implemented using parametric polymorphism and type classes, but with the same performance guarantees at C++ templates. I could also simply point out that most existing functional languages > do not always avoid dictionary passing, so there were type variables > that couldn't be statically resolved, so for these languages, strata > and stages were not quite the same. > Right, but thats due to other things like boxing, garbage collection etc. Personally I think a systems programming language should have all types unboxed, and no garbage collection. (Maybe GC as an optional library for when you want to do higher level stuff). > > You're half right, I think. Yes, dependent types remove the > relationship. But technically, so does anything else that can make > types unknown at compile time. And that's a lot of things. I don't think so. I think the only think that makes types unknown at compile time in a universally quantified type system is existentials. > Dependent > types go further and remove strata altogether. No, you don't _need_ to > introduce staging. You could also rely on the compiler to decide what > to implement dynamically. This is what I think they all do currently. > (Admittedly, they currently don't specialize enough, I think.) > Automatic specialisation / partial evaluation seems unable to achieve good enough results so far. Staging is messy and reminds me of using 'eval' in Lisp... it seems like something to avoid to me. Anyway, the way I'd say it is "you _get_ to introduce staging with > dependent types". :) That sounds like good combo for systems > programming to me. > I think dependent types with staging is one option. You have done enough to convince me that it is viable, but I don't yet think it is preferable. > Yes, separating them is more complex, but that's the way it is. If you > tie them together, there are tons of type system features that you > can't handle, and the burden is on you to try and come up with > adequate alternatives. Thinking of them as necessarily tied together > is unconventional. > I am yet to find any type system feature I cannot have that I need. I actually think I can get dependent types to fit this model too, by treating the types that depend on values as existentials. My concern is that existentials minimise the amount of the program that depend on the runtime value (as the type can only be known inside the container). Dependent types seem to allow this value-dependency to escape and propagate though the rest of the program. Looking at the lambda cube: values depending on values = functions values depending on types = polymorphism types depending on types = type families types depending on values = existentials So it seems it already is a dependent type system? Keean.
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
