Personally I'm cool with the trade-off, but I've needed to make peace with the fact that there is no type system that will ever really satisfy me now. I'm optimistic that we are iterating towards a better place though. The future is exciting!
Conversation
Sorry to bring all this up in people's timeline again - I guess I'm just hoping to encourage empathy and build some bridges! I'm not alone in forgetting that we're all trying to solve hard problems, in different ways!
2
3
No worries! Haven't seen much except for the Rich Hickey's gist about open source—seems somewhat sour but also understandable and possibly a bit of a hissy/hickey fit. I noticed your secret project in another tweet … so the future of programming _is_ dependently typed, isn't it?
1
I'm pretty sure it is! But it's still a long road ahead. Many problems still need to be solved, and that's even with all the decades of research poured into it. I do think we need to try to get it into practical usage more though - hence my not-so-secret project :3
2
1
Good luck with it! A lot of programs can be written easily within an ML-style system but would be nice to know you have the power of dependent types when you need it. I find DT pretty tricky in Haskell and haven't really gotten into them there... but in Idris, it's pretty easy.
1
Yeah - big thing I'm missing in Idris is low level control over memory representation. I also want it to be more structural too. Unfortunately the combination of these two things is hard, and dependent types add to the pain! For now I'm just not worrying too much... we'll see!
1
I understand. The runtime and data representation are important too. I haven't looked too closely into your secret project but I approve and encourage you wholeheartedly 😃. Efficient runtime and GC has been a problem for Idris in addition to bugs (!).
2
If you're not trying to avoid GC altogether (like Rust), then the OMR might be worth a look eclipse.org/omr/
1
1
Ohh, will check that out! My ultimate goal is to avoid GC, but it might be nice to provide one if folks want one 🤔
1
1
Avoiding GC seems overrated to me for appdev. Comes from a C++ mindset at Mozilla? Maybe it's easy in Rust but I heard it can be cumbersome… However, it can be important sometimes — particularly in OS kernels IIRC — I imagine, in browser's too! Check out flyingfrogblog.blogspot.com/2018/11/on-qua
1
Replying to
It’s not that bad actually (having used Rust). I’m interested in it because not mandating dynamic allocation/gc greatly widens the number of different kinds of applications you can write.