HackerTrans
TopNewTrendsCommentsPastAskShowJobs

blueberry87

no profile record

Submissions

[untitled]

1 points·by blueberry87·6개월 전·0 comments

Horrible answers to "What is a type?"

blueberrywren.dev
1 points·by blueberry87·8개월 전·0 comments

Opinion Piece: On Zig

blueberrywren.dev
18 points·by blueberry87·9개월 전·4 comments

Crafting a dependent typechecker, part 1

blueberrywren.dev
7 points·by blueberry87·12개월 전·0 comments

De Bruijn notation, and why it's useful

blueberrywren.dev
141 points·by blueberry87·작년·44 comments

comments

blueberry87
·2년 전·discuss
i mean, then we get into defining multi-paradigm :P does it have objects that could, theoretically, be used in a java-like object oriented system? yes! does anybody do that? not really! it's far more functional than any other paradigm, and that's what counts.
blueberry87
·2년 전·discuss
this is wrong! ocaml is a functional programming language with side effects.
blueberry87
·2년 전·discuss
annoyingly go can't have proper sum types, as the requirement for a default value for everything doesn't make any sense for sum types
blueberry87
·3년 전·discuss
that's not how compile time works buddy
blueberry87
·3년 전·discuss
You lose a very large amount of expressive power if you don't. Any formalisation of the reals requires at least 3 levels, if I remember correctly.
blueberry87
·3년 전·discuss
What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
blueberry87
·3년 전·discuss
Trying to compare a switch statement to proper pattern matching is like comparing a rock to a rocket.
blueberry87
·3년 전·discuss
Also agda: https://plfa.github.io/
blueberry87
·3년 전·discuss
What's your workflow for adding a new feature to something? In OCaml, with it's "high-tech language features like algebraic data types and ultra-strict typing", my entire workflow is: - Modify the types to add the new thing. - Fill in all the pattern matching cases that the compiler tells me I need to fill in. - Maybe write a little bit extra logic. And then i'm done, with a solution I know is type safe, will never crash unless i've explicitly let it, etc. How does this help with moving data? Well, wouldn't it be handy if the compiler could stop your program from crashing when something goes wrong, or you could have the compiler track where you've safely and unsafely done operations, or a million other things. Maybe this is too strong a statement, but if you can't see the advantage of that, I don't want to work with code you've written, because you're not doing everything you can to make it as safe as possible.
blueberry87
·3년 전·discuss
Yeah, in any modern language with pattern matching stuff like this is absolutely the compiler's job, and can be done pretty well[1] - of course, there are plenty of legacy languages that don't have pattern matching, but seeing as it can be compiled straight to switches and whatnot, even the lowest level languages don't have /that/ much of an excuse.

refs: [1]: http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf https://julesjacobs.com/notes/patternmatching/patternmatchin...
blueberry87
·3년 전·discuss
+1 for "Brady_story".
blueberry87
·3년 전·discuss
The point of this website isn't to mock software that has bugs - it's to show pitfalls that have been fallen into before, and could be fallen into again. If popular languages have encountered them in the past, and fixed them, why not document it? Helps people in the future. Sure, actual examples of pure unsoundness are more interesting, but creating unsoundness in what should be a sound system is also useful to implementers of these sorts of systems.