5 ms·

"There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to

by eagle2001 12y ago

"There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff." Examples, please. (I like bright, shiny things.)

Chinjut 12y ago
Perhaps Coq, Agda, Idris, and other such dependently-typed languages are to be considered, at least in some dimensions, "more advanced" than Haskell.
- mercurial 12y ago
  I wouldn't say full-blown theorem provers (Coq, Agda) are really in the same category as Idris, which is supposed to be more practical.
  - tel 12y ago
    Why not? I'd say that Agda/Idris/Coq are substantially the same languages with variation arising only in the kind of styles of coding they emphasize.
    - mercurial 12y ago
      But isn't this a variant on the old "but it's Turing-complete, therefore you can do anything" fallacy? Sure, their type system may be similar, but the question is, which one will let you write, say, a robust, maintainable HTTP client with the least amount of pain?
      - tel 12y ago
        I suppose that's true. I guess in my eyes DTs are such a meteoric difference that Idris is not sufficiently more interesting than the others yet. But time will tell if they manage to build a better way to manage proofs, for instance, they could really change the game.
        coolsunglasses 12y ago
        That there is no game-plan for doing anything any better than Coq presently does is why I'm a bit skeptical. The trimmings are nicer - nothing else as of yet.
        freyrs3 12y ago
        The elephant in the room in these discussions is that the cost of bringing a function compiler to fruition is so high that too much of the discussion gets muddled in the semantics of these hypothetical Haskell-successor languages while no one is actually working on said language. Academia simply isn't set up to incentivize large engineering projects, and industry would never invest in building such a thing either since there's no profit in language dev sadly. The blunt truth is that at the end of the day Haskell works today, period, and until someone actually forks or starts writing a new language very little of these criticisms of Haskell actually matter if the answer to "what should I use for my project at work" is "well it doesn't exist yet, but it has modules and extensionality and a magical pony that shits money".
        coolsunglasses 12y ago
        This is more or less where I stand as well. Haskell has an efficient RTS, well designed compiler, best-in-industry concurrency, good-enough type-safety that is light-years ahead of even things like Scala, and a good library ecosystem. It's ready now and I'd like to begin work with Haskell in the hopes that industry wakes up to the utility of future successors to Haskell by seeing Haskell itself in action.
coolsunglasses 12y ago
The principal thing I push learners towards after Haskell would be things like Coq and Agda. Coq has better learning materials, Agda has Haskell integration. The usual sequence is [1] followed by [2]. Augment with [3] and [4] as needed. One negative thing about Coq/Agda/Idris is they don't have a satisfactory encoding of typeclasses [5]. This is a problem in general with all dependently typed languages. Proof obligations get "churned" by changing code and the only tool to address that is extremely general proof terms combined with proof search. The best proof search is Coq, but the code extraction is heartburn-inducing for Haskell users. Whereas in Haskell, we get extremely lightweight and type-safe code refactoring because of the way in which we leverage typeclasses and parametricity. This turns out to be very valuable as your projects get more serious. That said, still entirely worthwhile to learn Coq or Agda. By the way, this [6] is how I teach Haskell. Working on a book as well. [1]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html [2]: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ [3]: http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf [4]: http://www.amazon.com/How-Prove-It-Structured-Approach/dp/0521675995 http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05... [5]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa... [6]: https://github.com/bitemyapp/learnhaskell https://github.com/bitemyapp/learnhaskell
deleted 12y ago
[deleted]

Chinjut 12y ago

Perhaps Coq, Agda, Idris, and other such dependently-typed languages are to be considered, at least in some dimensions, "more advanced" than Haskell.

mercurial 12y ago
I wouldn't say full-blown theorem provers (Coq, Agda) are really in the same category as Idris, which is supposed to be more practical.
- tel 12y ago
  Why not? I'd say that Agda/Idris/Coq are substantially the same languages with variation arising only in the kind of styles of coding they emphasize.
  - mercurial 12y ago
    But isn't this a variant on the old "but it's Turing-complete, therefore you can do anything" fallacy? Sure, their type system may be similar, but the question is, which one will let you write, say, a robust, maintainable HTTP client with the least amount of pain?
    - tel 12y ago
      I suppose that's true. I guess in my eyes DTs are such a meteoric difference that Idris is not sufficiently more interesting than the others yet. But time will tell if they manage to build a better way to manage proofs, for instance, they could really change the game.
      - coolsunglasses 12y ago
        That there is no game-plan for doing anything any better than Coq presently does is why I'm a bit skeptical. The trimmings are nicer - nothing else as of yet.
        freyrs3 12y ago
        The elephant in the room in these discussions is that the cost of bringing a function compiler to fruition is so high that too much of the discussion gets muddled in the semantics of these hypothetical Haskell-successor languages while no one is actually working on said language. Academia simply isn't set up to incentivize large engineering projects, and industry would never invest in building such a thing either since there's no profit in language dev sadly. The blunt truth is that at the end of the day Haskell works today, period, and until someone actually forks or starts writing a new language very little of these criticisms of Haskell actually matter if the answer to "what should I use for my project at work" is "well it doesn't exist yet, but it has modules and extensionality and a magical pony that shits money".
        coolsunglasses 12y ago
        This is more or less where I stand as well. Haskell has an efficient RTS, well designed compiler, best-in-industry concurrency, good-enough type-safety that is light-years ahead of even things like Scala, and a good library ecosystem. It's ready now and I'd like to begin work with Haskell in the hopes that industry wakes up to the utility of future successors to Haskell by seeing Haskell itself in action.

coolsunglasses 12y ago

The principal thing I push learners towards after Haskell would be things like Coq and Agda. Coq has better learning materials, Agda has Haskell integration. The usual sequence is [1] followed by [2]. Augment with [3] and [4] as needed. One negative thing about Coq/Agda/Idris is they don't have a satisfactory encoding of typeclasses [5]. This is a problem in general with all dependently typed languages. Proof obligations get "churned" by changing code and the only tool to address that is extremely general proof terms combined with proof search. The best proof search is Coq, but the code extraction is heartburn-inducing for Haskell users. Whereas in Haskell, we get extremely lightweight and type-safe code refactoring because of the way in which we leverage typeclasses and parametricity. This turns out to be very valuable as your projects get more serious. That said, still entirely worthwhile to learn Coq or Agda. By the way, this [6] is how I teach Haskell. Working on a book as well. [1]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html [2]: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ [3]: http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf [4]: http://www.amazon.com/How-Prove-It-Structured-Approach/dp/0521675995 http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05... [5]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa... [6]: https://github.com/bitemyapp/learnhaskell https://github.com/bitemyapp/learnhaskell

deleted 12y ago

[deleted]