On Sun, May 3, 2015 at 5:51 PM, Keean Schupke <[email protected]> wrote: > On 3 May 2015 at 22:15, Matt Oliveri <[email protected]> wrote: >> On Sun, May 3, 2015 at 12:00 PM, Keean Schupke <[email protected]> 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.
Hmm, well maybe that's a way to look at it. But it sure doesn't sound like the usual way to look at it. >> 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. There seems to be a bit of a disconnect in your responses, so I guess you're not understanding one of my points. All of those systems that we agree have a difference between strata and phases? I'm saying you can't type check them, as long as you continue to believe that type checking happens only at ground types. Either that, or you can only check them via some awkward encoding into whatever you're calling "existentials". It's not just dependent type systems, it's practically all type systems from or based on typed functional languages. >> 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. Strange. To me, doing (restricted) polymorphism and type classes, but with the same implementation style as C++ templates seems right up modal staging's alley. It would be an improvement over templates in that, like real type abstraction, you don't need to check each template instance. >> 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). I don't see why boxing and garbage collection would be the culprits for losing static resolution. Those things make type systems easier. >> 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. Well, we've established that you're thinking about type systems in a very strange way. We'll see how you'd express this after you realize you're supposed to be doing type checking at abstract types. >> 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. Depends on what's "good enough". I think it's plenty good enough for most application code. > Staging is messy and reminds me of using 'eval' in > Lisp... it seems like something to avoid to me. It shouldn't remind you of eval. It should remind you of macros. Just much much cleaner. (But also less expressive.) >> 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. Since you said your existantials have a runtime witness, I can tell you already that they are a dead wrong way of doing dependent types. One of the major draws of dependent types is moving evidence and checks to compile time. E.g. array bounds and bounds checking. > 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. Well I don't know if dependent types can be encoded with what you call "existentials". Just that it's a bad idea, and they can't be encoded with what I call "existentials". > Looking at the lambda cube: > > values depending on values = functions Yes. > values depending on types = polymorphism Yes. Specifically impredicative polymorphism, as in System F. Note that here, you already have existentials. > types depending on types = type families Yes. > types depending on values = existentials No. This is dependent types. This is exactly dependent types. We can talk about what existential-like types various systems have later. Dependent typing is conceptually prior to any specific type constructor. But understanding abstract types is conceptually prior to dependent typing. > So it seems it already is a dependent type system? The full lambda cube is the Calculus of Constructions, which is a dependent type system. So yes. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
