On Sun, May 3, 2015 at 12:00 PM, Keean Schupke <ke...@fry-it.com> wrote: >> > Haskell could be as fast as C++ if the >> > compiler was good enough at optimising. >> > I don't think it will ever happen. >> > On 3 May 2015 16:16, "Matt Oliveri" <atma...@gmail.com> wrote: >> Me neither. What's your point? We started by discussing the >> correctness and convenience benefits of typeclasses vs. instance >> arguments. There's no difference in performance. > > The difference in performance between c++ where templates (which can be > modelled in a type safe way as type classes) and languages that have to use > dynamic dispatch is not small.
I meant the difference in performance between different abstraction mechanisms that aren't necessarily resolvable statically. But rather than argue the details, which I'm not an expert in, let's focus on our disagreement over restricting the type system vs. explicit staging. >> No, the language designers are well aware that you can't always >> specialize. There is no scandal of the missing optimizer. It's just >> that most language designers apparently don't think static resolution >> is as important as you do. > > C++ does not take that approach. Systems programming languages need to make > performance issues visible to the programmer. I agree. >> Yeah I know you want this. It's not a bad idea. But it seems totally >> orthogonal to typeclasses vs. instance arguments vs. dependent types. > > Type classes with global coherence can be statically resolved (when not > combined with existentials). Well, OK. If you're right, then they're not totally orthogonal. But I propose that a good design philosophy would be to treat staging and abstraction as separate issues as much as possible. Staging is about performance; abstraction is about modularity and correctness. >> But the type _isn't_ always known at compile time. > > If there is no existential encapsulation the types are always known at > compile time. Perhaps. But for type systems in general, they aren't. So the more robust point of view is to think of staging and strata as separate. As an example of a benefit of doing so, you could have a language with both dependent types and programmer control over specialization. I don't know of any existing language like this, but it doesn't seem too outrageously hard. >> That's what I've >> been trying to tell you. Whether you know something at compile time is >> unrelated to whether it's type-level or not. > > I disagree, you need existential types to enable runtime polymorphism, > otherwise type safety requires you know all types at compile time. Otherwise > type checking would not work. No. You can statically check that types agree without knowing what the types are. That's the whole point of type variables. And with dependent types, you can check types depending on values without knowing what the values are. Variables again. This is the basics, Keean. Variables are unknowns, just like in algebra. 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. >> If they were the same, >> you'd be absolutely right that dependent type systems break phase >> separation and are bad news. But you're wrong. Stages/phases and >> strata are unrelated phenomena. > > Well we might have to agree to disagree, although you would save me a lot of > wasted time if you could prove or convince me they are unrelated. 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? 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.) 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... 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. >> Dependent type systems get rid of >> strata, and this need not have any effect on staging. > > You need to introduce staging with dependent types, because they remove the > relationship between phase and strata. 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. 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.) 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 don't think implicit instance vs. explicit value is a good way for >> the programmer to control whether to allow runtime polymorphism. Try >> staging annotations. > > Why introduce a new mechanism and additional complexity > when you don't need to? I'll answer that along with your next reply. >> Even if you're right that type classes can be statically resolved in >> the absence of existential types, I think staging annotations would be >> a better way for the programmer to force specialization. Not relying >> on some brittle property of a type system that's been crippled in just >> the right way. > > What you call a brittle property is something that seems fundamental and > important to me. Your reasoning seems circular. Having strata correspond to stages "seems fundamental", therefore you should indicate stage by indicating value vs. type. You want to indicate stage by indicating value vs. type, therefore strata had better correspond to stages. 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. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
