9 ms·

> We can generalise this idea of being forced to handle the failure cases by saying that Haskell makes us write total functions rather than partial functions.

• samvher 2y ago
  For a long time already I've wanted to make the leap towards learning dependently typed programming, but I was never sure which language to invest in - they all seemed either very focused on just proofs (Coq, Lean) or just relatively far from Haskell in terms of maturity (Agda, Idris). I went through Software Foundations [0] (Coq) which was fun and interesting but I can't say I ever really applied what I used there in software (I did get more comfortable with induction proofs). You're mentioning Lean with Agda and Idris - is Lean usable as a general purpose language? I've been curious about Lean but I got the impression it sort of steps away from Haskell's legacy in terms of syntax and the like (unlike Agda and Idris) so was concerned it would be a large investment and wouldn't add much to what I've learned from Coq. I'd love any insights on what's a useful way to learn more in the area of dependent types for a working engineer today. [0] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
  • iso8859-1 2y ago
    Lean aims to be a general purpose language, but I haven't seen people actually write HTTP servers in it. If Leo de Moura really wanted it to be general purpose, what does the concurrent runtime look like then? To my knowledge, there isn't one? That's why I've been writing an HTTP server in Idris2 instead. Here's a todo list demo app[1] and a hello world demo[2]. The advantage of Idris is that it compiles to e.g. Racket, a high level language with a concurrent runtime you can bind to from Idris. It's also interesting how languages don't need their own hosting (e.g. Hackage) any more. Idris packages are just listed in a TOML file[3] (like Stackage) but still hosted on GitHub. No need for versions, just use git commit hashes. It's all experimental anyway. [1]: https://janus.srht.site/docs/todolist.html https://janus.srht.site/docs/todolist.html [2]: https://git.sr.ht/~janus/web-server-racket-hello-world/tree/master/item/src/HelloWorld.idr https://git.sr.ht/~janus/web-server-racket-hello-world/tree/... [3]: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...
    • drzzhan 2y ago
      This is not related to Lean or Haskell. I'm just wondering why when people are curious about a new general-purpose language, the first thing they test is an HTTP server.
    • ants_everywhere 2y ago
      > (like Stackage) but still hosted on GitHub I don't have much experience with Haskell, but one of the worst experiences has been Stack's compile time dependency on GitHub. GitHub rate limits you and builds take forever.
      • tome 2y ago
        That's interesting. Could you say more? This is something that we (speaking as part of the Haskell community) should fix. As far as I know Stack/Stackage should pick up packages from Hackage. What does it use GitHub for?
        • 2y ago
• lemonwaterlime 2y ago
  > why would you restrict yourself to Haskell? It's not bleeding edge any more. I'm not using Haskell because it's bleeding edge. I use it because it is advanced enough and practical enough. It's at a good balanced spot now to do practical things while tapping into some of the advances in programming language theory. The compiler and the build system have gotten a lot more stable over the past several years. The libraries for most production-type activities have gotten a lot more mature. And I get all of the above plus strong type safety and composability, which helps me maintain applications in a way that I find satisfactory. For someone who aims to be pragmatic with a hint of scholarliness, Haskell is great.
  • iso8859-1 2y ago
    > The compiler and the build system have gotten a lot more stable over the past several years. GHC2021 promises backwards compatibility, but it includes ill-specified extensions like ScopedTypeVariables. TypeAbstractions were just added, and they do the same thing, but differently.[0] It hasn't even been decided yet which extensions are stable[1], yet GHC2021 still promises compatibility in future compiler versions. So either, you'll have GHC retain inferior semantics because of backwards compatibility, or multiple ways of doing the same thing. GHC2024 goes even further and includes extensions that are even more unstable, like DataKinds. Another sign of instability is the fact that GHC 9.4 is still the recommended[2] release even though there are three newer 'stable' GHCs. I don't know of other languages where the recommendation is so far behind! GHC 9.4.1 is from Aug 2022. It was the same situation with Cabal, it took forever to move beyond Cabal 3.6 because the subsequent releases had bugs.[3] [0]: https://serokell.io/blog/ghc-dependent-types-in-haskell-3 https://serokell.io/blog/ghc-dependent-types-in-haskell-3 [1]: https://github.com/ghc-proposals/ghc-proposals/pull/669 https://github.com/ghc-proposals/ghc-proposals/pull/669 [2]: https://github.com/haskell/ghcup-metadata/issues/220 https://github.com/haskell/ghcup-metadata/issues/220 [3]: https://github.com/haskell/ghcup-metadata/issues/40 https://github.com/haskell/ghcup-metadata/issues/40
    • deleted 2y ago
      [deleted]
    • 2y ago
• gtf21 2y ago
  > That's why, if you like the Haskell philosophy, why would you restrict yourself to Haskell? In the essay, I didn't say "Haskell is the only thing you should use", what I said was: > Many languages have bits of these features, but only a few have all of them, and, of those languages (others include Idris, Agda, and Lean), Haskell is the most mature, and therefore has the largest ecosystem. On this: > It's not bleeding edge any more. "Bleeding edge" is certainly not something I've used as a benefit in this essay, so not really sure where this comes from (unless you're not actually responding to the linked essay itself, but rather to ... something else?).
• giraffe_lady 2y ago
  > As the typed FP ecosystem is moving towards dependent typing (Agda, Idris, Lean) I'm not really sure where the borders of "the typed FP language ecosystem" would be but feel pretty certain that such a thing would enclose also F#, Haskell, and OCaml. Any one of which has more users and more successful "public facing" projects than the languages you mentioned combined. This is not a dig on those languages, but they are niche languages even by the standards of the niche we're talking about. You could argue that they point to the future but I don't seriously believe a trend among them represents a shift in the main stream of functional programming.
  • xupybd 2y ago
    This is the F# time that I've seen F# contrasted as the more mainstream option and it warms my heart.
• mightybyte 2y ago
  > That's why, if you like the Haskell philosophy, why would you restrict yourself to Haskell? It's not bleeding edge any more. Because it has a robust and mature ecosystem that is more viable for mainstream commercial use than any of the other "bleeding edge" languages.
• js8 2y ago
  > As the typed FP ecosystem is moving towards dependent typing (Agda, Idris, Lean), this becomes an issue, because you don't want the type checker to run indefinitely. First of all, does ecosystem move to dependent types? I think the practical value of Hindley-Milner is exactly in the fact that there is a nice boundary between types and terms. Second, why would type checking running indefinitely be a practical problem? If I can't prove a theorem, I can't use it. The program that doesn't typecheck in practical amount of time is in practice identical to non-type-checked program, i.e. no worse than a status quo.
  • DonaldPShimoda 2y ago
    No, the FP community at large is definitely not moving toward dependent types. However, much more of the FP research community is now focused on dependent types, but a good chunk of that research is concerned with questions like "How do we make X benefit of dependent types work in a more limited fashion for languages without a fully dependent type system?" I think we'll continue to see lots of work in this direction and, subsequently, a lot of more mainstream FP languages will adopt features derived from dependent types research, but it's not like everybody's going to be writing Agda or Coq or Idris in 10 years instead of, like, OCaml and Haskell.
    • cubefox 2y ago
      I'm not even sure if any human is still writing code in 10 years.
      • ParetoOptimal 2y ago
        Based on what?
        • cubefox 2y ago
          Looking back where we were 10 years ago in terms of AI: If we get a similar jump in 10 years from now, we have superintelligence.
• tkz1312 2y ago
  > So what does unique value proposition does GHC have left? Possibly the GHC runtime system, but it's not as sexy to pitch in a blog post like this. The point is that programming in a pure language with typed side effects and immutable data dramatically reduces the size of the state space that must be reasoned about. This makes programming significantly easier (especially over the long term). Of the languages that support this programming style Haskell remains the one with the largest library ecosystem, most comprehensive documentation, and most optimised compiler. I love lean and use it professionally, but it is nowhere near the usability of Haskell when it comes to being a production ready general purpose language.
  • dataflow 2y ago
    > dramatically reduces the size of the state space that must be reasoned about True > This makes programming significantly easier (especially over the long term) Not true. (As in, the implication is not true.) There are many many factors that affect ease of programming and the structure of the stage space is just one of them.
    • tkz1312 2y ago
      It’s true that things like docs and error messages are also important, but the fundamental task of understanding and reasoning about code is significantly easier if you restrict yourself to pure functions over immutable data.
      • dataflow 2y ago
        No, I didn't mean docs and error messages, I meant even more basic things. Like sheer code size, visual noise, and intuitiveness, to give a few examples. There's no free lunch, everything is a tradeoff. Just because you're constraining the program's state space that doesn't imply you're making the code more succinct or intuitive. You could easily be adding a ton of distracting noise or obscuring the core logic with all your awesome static typing.
        • 2y ago
• aSanchezStern 2y ago
  Uhh, endless recursion doesn't cause your typechecker to run indefinitely; all recursion is sort of "endless" from a type perspective, since the recursion only hits a base case based on values. The problem with non-well-founded recursion like `main = main` is that it prevents you from soundly using types as propositions, since you can trivially inhabit any type.
  • remexre 2y ago
    The infinite loop case is: loopType : Int -> Type loopType x = loopType x foo : List (loopType 3) -> Int foo _ = 42 bar : List (loopType 4) bar = [] baz : Int baz = foo bar Determining if baz type-checks requires evaluating loopType 3 and loopType 4 to determine if they're equal.
    • HelloNurse 2y ago
      Given line "loopType : Int -> Type", how can line "loopType x = loopType x" mean anything useful? It should be rejected and ignored as a tautology, leaving loopType undefined or defined by default as a distinct unique value for each int.
      • remexre 2y ago
        What makes it ill-defined is that it computes infinitely -- that's why you need a totality checker (or a total language).
• throwthrow5643 2y ago
  >Haskell doesn't prevent endless recursion. (try e.g. `main = main`) Do you mean to say Haskell hasn't solved the halting problem yet?
  • xigoi 2y ago
    There are languages that don’t permit non-terminating programs (at the cost of not being Turing-complete), such as Agda.