3 ms·
This is where I believe strong typing (like, Haskell-strong or stronger) and functional programming in general will be a win. The confidence I have that my fixe
by black_knight 2mo ago
This is where I believe strong typing (like, Haskell-strong or stronger) and functional programming in general will be a win. The confidence I have that my fixes are localised when fixing Haskell code is infinitely stronger than fixing even Java, not speak about C, code.
- astrange 2mo agoHaskell's type system would not easily prevent this bug. It's not good at numeric/logic issues like that. When people say "Haskell makes it impossible to write bugs" they mean "Haskell has enums" (ADTs).
- black_knight 2mo agoI am not claiming you cant write buggy code in Haskell! But following good functional style, your bug will more likely be compartmentalised, and fixing it will not break some other part of your program.
- StilesCrisis 2mo agoYou can write good functional code in many languages. (Even C++!)
- black_knight 2mo agoSure! I have done my fair share of pretending Java and C++ support my functional style. But at the end of the day, you have better support for writing that style in a real functional programming language. And I wonder how well one can enforce a functional style in say Java or C++ upon the LLMs. Who knows, they might be great at it?
- _jackdk_ 2mo agoLiquid Haskell might require you to prove that the divisor is nonzero, but even in standard Haskell there's common idioms for ensuring that a list is non-empty (data NonEmpty a = a :| [a]) or that text is non-empty (newtype NonEmptyText = NonEmptyText Text, with non-exported constructor, helpers like make :: Text -> NonEmptyText, or more advanced tricks like https://exploring-better-ways.bellroy.com/haskell-koan-type-checked-non-empty-strings.html https://exploring-better-ways.bellroy.com/haskell-koan-type-... ). The big problem preventing this approach from working for numbers is that it's just so cumbersome there. Most of this is because all the arithmetic operators are bundled into a single Num typeclass, and `fromInteger :: Num a => Integer -> a` has a type that's impossible for a "non-zero number" wrapper to satisfy.
- inigyou 2mo agoOOP has those too, and they're very annoying.
- nh2 2mo agoIn Haskell they are a little less annoying. It is just easier to reason about (including proving) pure functions.
- inigyou 2mo agoI meant the constrained types by hiding the constructors. Super annoying, not automatically convertible, in Haskell you have to remember what the fake constructor is called, and write it every time you use it, but at least it's efficiently implemented with newtype, unlike the Java OOP version. Think about writing a value with several nested constrained types, like NonEmptyListOne (makeNonZeroNumber 42, 'h' `NonEmptyString` "ello world"). It's just really annoying.
- _jackdk_ 2mo agoThe blog link I mentioned avoids this cost with literals, by providing using a required type argument to check the string length at compile time without TH. It requires a relatively recent GHC: make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText type family IsNonEmptySymbol symbol :: Constraint where IsNonEmptySymbol "" = Unsatisfiable (Text "Expected a non-empty string") IsNonEmptySymbol _ = (()::Constraint) -- empty constraint is always satisfied
- black_knight 2mo agoDefinitely room for improvement on Haskell's standard library when it comes to the number-related type classes. Modern Haskell could do very well in this area with a good type-class redesign in this area. The issue I think is that this would invalidate a lot of existing code, relying upon that. But you can already replace Prelude with something else in your own code if you want to.
- tome 2mo agoPeople don’t say "Haskell makes it impossible to write bugs"! You may have heard "if it compiles it works" which is somewhat tongue in cheek, but also true for a sufficiently loose interpretation of "works" in a way it is not true for languages with a less strong and flexible type system.
- fouronnes3 2mo agoWhat's stronger than Haskell?
- theLiminator 2mo agoPerhaps coq/agda/idris/etc.
- astrange 2mo agoAnything with ranged numeric types. Like everyone's favorite functional programming language, Ada.
- black_knight 2mo agoOr Liquid Haskell.
- ghaslt 2mo agoThis issue raises SIGFPE. Ada would raise Constraint_error, which is easier to catch than a signal, but still occurs at runtime. You need range proofs to be 100% safe, and then you can as well use the regular type because invalid values will not occur.
- black_knight 2mo agoDependent types is one possible direction. Not sure when a language with dependent types will arise which will be useful for making real programs. Agda is the most mature dependently typed programming languae (having been around since the 90s – it is basically Haskell on steroids), but has a more proof-assistant flavor than an actual programming language flavor. Opus & Fable write Agda quite well, so LLMs can understand dependent types.
- TheGoddessInari 2mo agoLean 4, Idris 2.
- theLiminator 2mo agoImo, formal methods like more expressive/stricter type systems are key to making LLM generated code successful. Of course models will get better, but trusting the output will become much easier with a type system that proves more properties.
- UltraSane 2mo agoEven Lean 4 strong typing
- deepsun 2mo agoYou haven't mentioned the dynamic typed languages that I believe should die -- Python and Javascript. The only good use case for dynamic typing is notebooks (niche of R lang) where you're throwing out the code you just wrote after getting the result you wanted from it.