25 ms·

Dependent Haskell Is the Future (2018)

• kasperni 7y ago
  > Why Dependent Haskell Is the Future of Software Development I find this hard to believe, considering probably less then 1-2% of developers in the world have any clue to what this article is about.
  • Southy 7y ago
    > 0.1-0.2% FTFY! :D
    • JamesBarney 7y ago
      I remember going to a happy hour at a large consulting company I worked for and 95% of people had never heard of Haskell much less knew anything about it. So needless to say I was easily pulled away from that company when the next person I interviewed with had written production Haskell code.
      • UncleMeat 7y ago
        I find this to be odd. Haskell seems to be the one language where recruiters lead with "we program in Haskell here" before saying what the company does. Do people really choose companies based on the language they are using?
        • dymk 7y ago
          At some point, money is no longer an issue (or falls into diminishing returns), and I'd even take some amount of a pay cut if it meant working in a language and on projects that were mentally stimulating
          • UncleMeat 7y ago
            But even this is odd to me. Programming seems to be the easy part. The hard (and stimulating part) is everything around that. If somebody says that they work in Haskell but doesn't say what they are working on then I'll just be confused. To me, it is like selling a company based on where you put the curly braces (a slight exaggeration here).
        • tempguy9999 7y ago
          "We Program in COBOL!" (Walks away slowly avoiding eye contact) A bit less facs- fascatio- fesceeshus- silly, companies that aren't smart enough to invest in good tools probably aren't smart enough to invest in good people. You can overdo the tech worship, but you can totally underdo it and cost yourself a bomb.
        • PeCaN 7y ago
          Haskell is less of a programming language and more of a religion, so people choosing companies based on their religion makes sense.
  • onion2k 7y ago
    This is probably because it's about cutting edge language design. The feature the article is about (dependent types) might well be the future of software development and could end up in every strongly typed language, but because it's new and Haskell's functional syntax looks weird compared to C-based languages, it makes the headline sound a bit hyperbolic.
    • wbhart 7y ago
      I wouldn't disagree that dependent types are great for certain specialised problem domains, but they've already been around for ages and didn't yet revolutionise the world of software design. I think the sentiment that this is unlikely to make a big splash is totally on point. Languages have to balance ease of use with features in order to become very popular. Nothing as purebred as Haskell is likely to become the next Python or Visual Basic. Real work horses are dirty, messy machines. Of course this new feature might turn out to be popular for Haskell users.
      • antisemiotic 7y ago
        >but they've already been around for ages and didn't yet revolutionise the world of software design. I think it's mostly because languages with dependent types are awfully clunky to use. Perhaps dependent typing is even a dead end, but I wouldn't count out other ideas such as refinement typing just yet. I think it will take a lot of work and failed attempts (such as typestate in early Rust) to get fancy type theory into mainstream languages (just like it took a while for Java to get lambdas). Case in point: static analysis tools for C++ are getting more capable and popular recently.
        • krapht 7y ago
          Formal methods in general are extremely clunky to use. Just see how much hate Rust gets for making it extremely difficult to make an intrusive linked list. And memory safety is only one kind of correctness assertion. So I'm gonna be a pessimist here and say: nope, not gonna be the future, because programmers are lazy and "ship it now" is better than "prove the bugs don't exist".
  • worldsayshi 7y ago
    That.. is mostly the case for innovative concepts at some point before they get adopted. At some point some years ago you could write a lengthy and passionate article about React or Typescript and discuss why it would be so advantageous and most front end developers would feel lost. Good ideas aren't necessarily easy to comprehend. In order for them to work for a wider audience someone need to properly package, document and maybe simplify them for it to work for them.
    • kasperni 7y ago
      I agree. But the headline was not referring to a concept (Dependent Types) but specifically to "Dependent Haskell" as the future of software development. Making it sound like we all are going to be Haskell programmers in the future.
      • worldsayshi 7y ago
        I think I can rephrase my opinion for either the language or concept and still agree with it. I believe Haskell has continuously become more developer friendly and may some time reach some kind of friendliness and use case support threshold that allows for a wider adoption. I recently started looking at Haskell a couple of weeks ago after years of hiatus. The IDE support have gone from almost none-existing and/or bug ridden to almost as good as Java and the new package manager has so far been pleasant to use. Although I'm using it for small side projects so it might not be fair comparison to my day work use case.
• p4bl0 7y ago
  What about F*? It has dependant types, and is already in use in production at some places (there is a project of making a proved TLS implementation with it and it is quite advanced iirc). Also, it is somewhat based on F# which is based on OCaml so I would bet that performance wise it can beat Haskell. https://www.fstar-lang.org/ https://www.fstar-lang.org/
  • carlmr 7y ago
    I would also say OCaml and F# style is also less foreign than Haskell to most newcomers. It's almost like (type-hinted) python + match expressions + pipes.
  • Hitton 7y ago
    I guess that the author didn't consider them, because neither of them is lazy by default, at the beginning he mentioned laziness as major Haskell advantage.
• deleted 7y ago
  [deleted]
• whateveracct 7y ago
  There are a lot of exciting new things on the medium-term horizon for Haskell. -XDependentTypes, -XLinearTypes, and a new pluggable concurrent (latency-optimized) GC
  • verttii 7y ago
    Can you link to more info about that latency-optimized GC?
    • mjh2539 7y ago
      source here: https://github.com/pepeiborra/gc-benchmarks/blob/master/README.md https://github.com/pepeiborra/gc-benchmarks/blob/master/READ...
    • mjh2539 7y ago
      Discussion here: https://www.reddit.com/r/haskell/comments/cp21wg/shorter_gc_pauses_coming_to_ghc/ https://www.reddit.com/r/haskell/comments/cp21wg/shorter_gc_...
    • deleted 7y ago
      [deleted]
• couchand 7y ago
  Previous discussion: https://news.ycombinator.com/item?id=18703245 https://news.ycombinator.com/item?id=18703245
• anonnybonny 7y ago
  There is a persistent myth that "A Haskell program that compiles is correct by definition" Indeed it is "correct" in the sense that it has a very high likelihood (maybe 90% ?) of doing what the programmer intended (Unlike say C or C++ where the probability drops to about 50% for beginners) However, that is a poor definition of "correct". While it's true that a lot of huge consequences have occurred due to stupid errors like buffer overflows (unintended bug), there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail. The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that
  • dmitriid 7y ago
    I sometimes phrase it as “yeah, your program is correct because it’s type-checked, but who has checked that your types are correct”? With dependent types some of the logic will be coded in types, and we would need to check those.
    • moomin 7y ago
      Indeed, that’s why Dan North, Liz Keogh, et al have been banging the requirements capture drum for the last ten/twenty years. Doesn’t mean it might not be useful.
    • grumdan 7y ago
      At least now we are checking that two pieces of saying what we want a program to do match up. It's less likely to get both the implementation and specification (in the form of types) wrong. Whenever the program fails to type-check, it will make you think about both bugs in the type and bugs in the code, even if the latter is more likely.
      • dmitriid 7y ago
        Types can’t encode the specification fully, or require a lot of work to encode a specification (so most people will skip this work). The simplest example is very common banking and e-commerce logic which is basically a series of checks in the form: if <some piece of data retrieved at runtime at that particular moment> is consistent with <multiple other pieces whose number and relevance depends on that data retrieved at runtime from potentially multiple sources>.
• dmitriid 7y ago
  > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This can potentially unseat the current reigning champ of Haskell-related statements which is “A monad is just a monoid in the category of endofunctors, what's the problem?”
  • Sharlin 7y ago
    To be fair, at least that's computer science speak rather than category theory speak.
    • asplake 7y ago
      What body of knowledge defines "type classes"? I ask out of relative ignorance, kinda saw it as Haskell thing
      • Sharlin 7y ago
        The term "type class" is original to Haskell, I think, but the concept (constrained parametric polymorphism) is fairly standard programming language theory.
      • pwm 7y ago
        If you are curious this is a good read: https://www.parsonsmatt.org/2017/01/07/how_do_type_classes_differ_from_interfaces.html https://www.parsonsmatt.org/2017/01/07/how_do_type_classes_d...
    • tiborsaas 7y ago
      If the author really wants Dependent Haskell to be the future, maybe he should use Pyhon and JavaScript speak to spread concepts. A world with little handles attached to it slips too fast out of the curious minds.
      • Sharlin 7y ago
        The title notwithstanding, this article is definitely aimed at Haskellers, or at least people who have more than rudimentary knowledge of Haskell and type systems. Anyway, it's rather difficult to talk about advanced type systems in terms of languages that have no type system at all :)
• cryptica 7y ago
  Functional programming was a fad and it's going out of fashion (again). It gives you rerefential transparency at the expense of real modularity. Real modularity can only be achieved through proper separation of concerns. The best way to achieve that is by categorizing system state and system logic and allowing chunks of logic to be colocated with the relevant parts of the system state. This is what OOP excels at. With functional programming, you cannot colocate module logic with module state so you often end up with a large monolithic state store on one side of the system and logic which is completely decoupled and sitting on the opposite side of the system... Then the challenge is to apply functions to various relevant parts of the state to transform it in a referentially transparent way. The modularity problem then comes when you need to make a change to the schema/structure of the state; whenever you change the structure of the state, you need you need to search through your logic to identify all the parts of the logic which depend on that state and update them to work with the new structure. This is a massive problem and leads to what OOP developers call spaghetti code.
  • sbergot 7y ago
    This is like saying non-nullable references are a problem because nullable refs are sometime useful. Nothing prevents you from having state in an haskell application. You just have to be explicit about it. Whether the language ergonomics are better or worse than a language that allows state without an explicit type is another question but your reasoning is questionable.
    • cryptica 7y ago
      You can also have pure functions in OOP languages. You can even have a code linter to enforce it as a rule. When discussing programming languages, it's more about what behaviours they encourage rather than what behaviours they support.
      • rowanG077 7y ago
        OOP language aren't explicit in what function is pure. If I'm working on a 10MLoC project and touching hundreds of methods while working I can't lookup the implementation of each one to determine whether they are pure. And no a comment saying they are pure is not sufficient. The above is trivial in FP languages.
• deleted 7y ago
  [deleted]
• veonik 7y ago
  I spent a long winter understanding dependent types followed by a short summer forgetting everything. Anyway, I'm here for the koolaid.
  • bingerman 7y ago
    I'm curious which language/approach did you take. I recently picked Idris with the book Type-driven development in Idris and so far I'm enjoying the ride (I have some experience in functional programming but not in Haskell).
• nudpiedo 7y ago
  > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. No, it’s not, if you can say this sentence without laugh at it, it is because you developed a deep understanding about all the core concepts, meanings, semantics and most probably now you know how to exploit them for their appropriate usage to solve even more complex problems.
  • tthisk 7y ago
    Yes this quote got me cringing, these things are definitely not 'simple'. The post's title is also presumptuous. While Haskell is a brilliantly elegant language, by capturing abstractions at a high level (i.e. category theory). This is also it's fallacy, these abstraction are inherently hard to understand because, well, they are so abstract. When writing most software in the real world we need to be pragmatic to be able to recruit people to actually write that software. So will Haskell take over all software engineering, I don't think so. Fortunately we can, and are already learning a lot from ideas introduced by Haskell.
    • UK-Al05 7y ago
      They are simple, but not easy learn. Lambda calculus is simple. Incredibly simple. But trying use lamda calculus to do anything with is hard.
  • Certhas 7y ago
    It's simple as opposed to complex, not simple as opposed to difficult.
    • nudpiedo 7y ago
      Three different areas of computer science, highly related to mathematics AND interrelated. Don’t you think these are not just difficult but also complex since all their rules are combined and compose?
      • 7y ago
• epiphone 7y ago
  How come none of the mainstream static type systems support dependent types? On paper they seem like such a neat idea for defining constraints and preventing bugs. I heard Scala and Haskell have optional/partial support for them, so I suppose it takes a pretty sophisticated type system to begin with?
  • Sharlin 7y ago
    To implement dependent types, your type system must go much deeper into the theorem prover territory than is normal in mainstream imperative programming languages (whose type systems are often more or less ad-hoc rather than based on rigorous theory). Furthermore, dependent types break the fundamental property that the relationship between types and terms is one-directional: types constrain terms but not the other way around. As one example, C++ has had non-type template parameters (types parameterized by values) for a long time, but only for compile-time constants. AFAIK there have been no formal proposals to introduce full-blown dependent types, rather the focus has been on improving the facilities for compile-time term-level computation.
  • mrkeen 7y ago
    The problem is that mainstream static types systems have two massive holes in them: nulls and pervasive mutability. Knowing that a list has length n at compile time isn't that useful if you're expecting the program to change the list's length at runtime. Or maybe there was never a list in the first place because it was null.
  • 6gvONxR4sf7o 7y ago
    People are still figuring out how to make things "easy" with them. The theory says you can prove cool stuff, but the syntax to do that while making it approachable is still something people work on. But that's an outsider's perspective.
  • UK-Al05 7y ago
    Dependent types are only recently becoming well known and popular. The type systems in mainstream languages were not built with these kind of flexibility required by dependent types.
• pron 7y ago
  The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in practice -- that the author does not seem to be aware of. He also does not seem to be aware of all the other approaches for software verification and correctness (sound static analysis, model checking, concolic testing) that have so far shown greater promise, and formal methods research focuses on them rather than on dependent types (the approach that scales least and suffers from the most limitations); in fact, last I spoke with a dependent type researchers, he told me that now they're trying to weaken the soundness of their type systems (sort of gradual-dependent-types) to try and fight the problems types suffer from. I'm not saying dependent types don't have some uses, or that they won't change enough so they could play a central role in software correctness, but thinking that they're the future of software correctness (in their current form) shows a complete lack of familiarity with this field.
  • tav 7y ago
    Could you elaborate on the "fundamental, serious limitations" by any chance?
    • 9q9 7y ago
      1. No type inference (unlike ML-style types). 2. Oracle problem: In practise you never have full specifications (let me be provocative: Facebook has no specification in principle, only its ever changing code), and often, especially in early phases you rarely have specifications. 3. You pay the price for dependent types always (e.g. having to prove termination), even if you don't use interesting specifications. 4. Like Java's exception specifications, dependent types are 'non local', meaning that a change in one part of the code may ripple through the entire code bases, this stands in the way of quick code evolution, which is important -- at least in early parts of large-scale software projects. 5. Despite dependent types being 1/2 century old by now, and despite intensive effort, dependent types have not really been successfully been generalised to other forms of computing (OO, stateful, concurrecy, parallel, distributed, timed) -- unlike competing approaches. Summary: dependent types are wonderful as a foundations of mathematics, but have failed to live up to their promise as general purpose languages.
• gridlockd 7y ago
  bullshit :: Haskell -> DependentTypes -> Sunglasses -> Blockchain
• ErotemeObelus 7y ago
  Err... the problem with this is that the size of a list/array is sometimes determined at runtime. This means that if you use dependent types, you can't determine whether a program is correctly typed until you run the code.
  • rq1 7y ago
    Not at all. The verification is symbolic.
    • ErotemeObelus 7y ago
      Let's say we're creating an array of strings separated by newlines obtained from reading a file. Call this arr[n] where n is determined at runtime. Now let's have String index(arr:int[], i:(Fin(arr):int)), where FinInt(arr) is a dependent type that is an integer between zero and the length of the array. As the code is compiling, we have this int i = 24951; String str = index(f, i); The file exists in the future after the compilation. If the future file has at least 24951+1 lines, then the compiler can verify that i < n and that i is correctly typed. But if the file is short, then the type of i is incorrect. So at compile-type the type of i is indeterminate.
      • aeneasmackenzie 7y ago
        you get a compile time error saying f isn't known to have enough entries, and you resolve it by adding a decidable check that produces a proof that it does. (the check at runtime is just >)
    • ErotemeObelus 7y ago
      The solution is to just accept that types might change during runtime. Give up the assumption that types are fixed at compilation and that the compiler can catch all errors. Computer programs exist inseparably from the operating system. The type of a circle might change to that of an ellipse. The size of a file can only be known at runtime. The only way the compiler can catch all errors is if no object is mutable and everything except for closed variables is allocated on the stack. And both of those preconditions are insane. This is still superior to dynamic typed languages because it tells you exactly what the type problem is and where.
• deleted 7y ago
  [deleted]
• auslander 7y ago
  Lisp is like a religion. Once you get it, you cannot help yourself spreading the Word.