On Mon, May 4, 2015 at 3:24 AM, Keean Schupke <ke...@fry-it.com> wrote: > I am saying there certainly exist type systems where the above property > doesn't hold, but that is a subset of all type systems. Starting with simple > type systems, the property above holds, so it seems reasonable to say it > holds in general unless you add a particular feature to your type system > that breaks it.
That's a silly argument. In other words, you don't have a system outside the subset you like until you do. > On 4 May 2015 at 00:23, Matt Oliveri <atma...@gmail.com> wrote: >> It's not just dependent type systems, it's practically all type >> systems from or based on typed functional languages. > > No, I disagree. Simply typed lambda calculus has the above property, and > adding higher order functions does not remove it. HM + higher order > functions retains it too.. You listed some type systems studied on paper. Full blown languages tend to fall outside your subset, as I understand it. (And to be pedantic, simply typed lambda calculus already has higher order functions.) >> 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. > > Okay, first you need to convince me the above property does not hold before > I think its worth discussing staging. Otherwise we have two mechanisms > trying to achieve the same thing, which seems like a bad design to me. Which property? That strata are pinned to stages? >> I don't see why boxing and garbage collection would be the culprits >> for losing static resolution. Those things make type systems easier. > > Because you get tagged types at runtime you end up with code that is > non-specialised. Yes, it does make things easier by removing the need to > completely specialise, but then it is no longer generating code as fast as > C/C++. If you're saying you need tags at runtime for the garbage collector, that doesn't mean you can't specialize user code. And even if it did, it's not because static resolution failed. So I see what you're saying, but technically you argued the wrong thing. >> Depends on what's "good enough". I think it's plenty good enough for >> most application code. > > Good enough for code for which performance (and hardware cost when scaled > out) is not a factor. > > But if you can have the performance and write beautiful elegant code what's > the problem? I think you can have both, and that the features I would leave > out would not make the code better (more readable, simple). > > The goal is to write the simplest and most understandable version of some > algorithm, and have it be fast too, without jumping through hoops. In C++ I > can write fast code with elegant abstractions using templates. In Haskell I > have to annotate my code for strictness in some arcane way. A lot of programmers would consider using C++ to be jumping through hoops already. But I didn't mean to start an argument about what should be considered good enough performance. We agree that the programmer should control performance in a systems language, after all. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
