Conversation

Brendan Zabarauskas
@brendanzab
Different static type systems offer different trade-offs, and most are far from perfect. If you ask people to adopt them then you are asking them to accept their failings in exchange for some some compelling super-powers, and a promise that they will be better in the future.
Quote Tweet
Hillel
@hillelogram
·
((Hopefully last thread on the "Maybe Not" talk)) I'm seeing a lot of people object with the following argument: 1. Hickey has problem X with type system A 2. Type system B doesn't have X => Hickey is wrong about static typing. This is a really common, and IMO poor, argument.
Show this thread
1
6
Brendan Zabarauskas
@brendanzab
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!
1
7
Brendan Zabarauskas
@brendanzab
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
Steven Shaw
@steshaw
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
Brendan Zabarauskas
@brendanzab
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
Steven Shaw
@steshaw
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
Brendan Zabarauskas
@brendanzab
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
Steven Shaw
@steshaw
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
Brendan Zabarauskas
@brendanzab
Atm I’m gutting the internals to make way for normalisation-by-evaluation, but feel free to have a look! My main motivation is that Rust (as much as I love it) can’t do category theory nicely, is impure, is rather complex, and doesn’t have dependent types.
1
1
Steven Shaw
@steshaw
I've only read the introductory book to Rust. I would hope that you can have a completely pure language that is just as efficient at runtime—with a sufficiently smart compiler. My understanding of CT is also rather limited so I'll watch your progress with enthusiasm. Seen ATS?
1