6 ms·

I remember wondering why "return" is in the Monad class when you can just use "pure" from Applicative, and why (<>) and "mapped" both exist, so it's cool to rea

by jpe90 5y ago

I remember wondering why "return" is in the Monad class when you can just use "pure" from Applicative, and why (<>) and "mapped" both exist, so it's cool to read the historical explanations here. They are all logical, but will unfortunately add to the burden of new learners who read books and guides that contain obsolete references. I know a lot of the material I learned with will be confusing when examples start spitting out compile errors. I didn't see if there are efforts to account for this with some custom error messages that notify you why the obsolete code no longer works and suggests how to fix it, but I think that would be helpful. Edit: It looks like that concern was already raised and addressed, glad to see it.

mdm12 5y ago
The return/pure distinction is due to history, I believe. The Monad typeclass was defined before the Applicative typeclass. Part of the fun of being a research language is that you don't know everything up-front!
- quchen 5y ago
  Monad and Functor were first, if I remember correctly Applicative made its debut when Parsec became popular. For a long time, the hierarchy was »Functor ===> Applicative, Monad is independent«. We made Applicative a superclass of Monad around 2015, and since then return has been a historical artifact (with a dangerously misleading name).
  - 1-more 5y ago
    ty for this history! I write haskell at work but with an honestly middling understanding of the category theory that goes into what typeclasses are supersets of other typeclasses. Mostly because we use an overly verbose version of Prelude. So it's wild to me that these mathy bits were not always set in stone!
nerdponx 5y ago
If you are interested in "Haskell, but with a nicer standard library", Idris 2 might actually be an interesting choice. The Idris 2 prelude very much feels like a cleaned-up version of the Haskell prelude, and all the fancy dependent and quantitative type stuff is mostly "opt-in". For example, in Idris 2, the `[ foo | x <- bar ]` syntax is not just a "list comprehension", but a "monad comprehension", and `map` is not specialized for lists but it is actually what `fmap` is in Haskell. There is also other interesting shorthand syntax like `!foo` which is equivalent to something like `do x <- foo ; x`. The fact that it compiles to Chez Scheme and has a fairly easy-to-use FFI is even nicer. Would I deploy it in production yet? No. But the language is trying to be fundamentally practical and user-friendly while still being dependently- and quantitatively-typed. And in my opinion, it's succeeding so far! It also has a language server, so you can get advanced interactive editing features in pretty much any code editor that supports LSP. Oh, and there's no `return` in Idris 2, only `pure` :)
- mdm12 5y ago
  Your description of a monad comprehension in Idris reminds me of computation expressions in F#[1]. Looks like I have one more programming language to dive into! [1] https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/computation-expressions https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
  - sullyj3 5y ago
    A closer analogue is probably do-notation, which comprehensions are syntactic sugar for. Comprehensions can be terser for simple expressions, but for anything longer, do notation is generally more readable.
- kaba0 5y ago
  Isn’t haskell’s list comprehension can be used for monad comprehensions as well with a language extension? I remember using that once.
- wk_end 5y ago
  I want to like Idris - as a language it does so much right - but I still feel a little burnt. A few years ago were exciting times; Idris 1 had hit 1.0 and was humming along nicely, there was excellent tooling available, & Type-Driven Development with Idris had been published - a real printed book about practical coding with dependent types! Could reliable software be far behind? Would I maybe get to develop somewhere that took software engineering seriously in my lifetime? And then, with the possibility of success on the horizon, the Idris folk(s) got distracted by the QTT hype and decided to abandon ship so they could start on Idris 2. And, like, don't get me wrong - the QTT stuff is cool, and I'm a Rust fan in part because getting to encode linearity in your types is a real superpower - but it's so depressing that the world of practical dependent types feels just as far away now as it did ten years ago, after getting so excited about it five years ago. And it underscores what might be a bigger problem: at the end of the day - and by the Idris FAQ's own admission - Idris is a research project into practical dependent types, and Edwin Brady is an academic. Which means that when he gets interested in some other area of research, he's free to just...do that instead, or start over on Idris n+1, and leave Idris 1, 2, 3 ... n to wither.

by jpe90 5y ago

mdm12 5y ago

The return/pure distinction is due to history, I believe. The Monad typeclass was defined before the Applicative typeclass. Part of the fun of being a research language is that you don't know everything up-front!

quchen 5y ago
Monad and Functor were first, if I remember correctly Applicative made its debut when Parsec became popular. For a long time, the hierarchy was »Functor ===> Applicative, Monad is independent«. We made Applicative a superclass of Monad around 2015, and since then return has been a historical artifact (with a dangerously misleading name).
- 1-more 5y ago
  ty for this history! I write haskell at work but with an honestly middling understanding of the category theory that goes into what typeclasses are supersets of other typeclasses. Mostly because we use an overly verbose version of Prelude. So it's wild to me that these mathy bits were not always set in stone!

nerdponx 5y ago

If you are interested in "Haskell, but with a nicer standard library", Idris 2 might actually be an interesting choice. The Idris 2 prelude very much feels like a cleaned-up version of the Haskell prelude, and all the fancy dependent and quantitative type stuff is mostly "opt-in". For example, in Idris 2, the `[ foo | x <- bar ]` syntax is not just a "list comprehension", but a "monad comprehension", and `map` is not specialized for lists but it is actually what `fmap` is in Haskell. There is also other interesting shorthand syntax like `!foo` which is equivalent to something like `do x <- foo ; x`. The fact that it compiles to Chez Scheme and has a fairly easy-to-use FFI is even nicer. Would I deploy it in production yet? No. But the language is trying to be fundamentally practical and user-friendly while still being dependently- and quantitatively-typed. And in my opinion, it's succeeding so far! It also has a language server, so you can get advanced interactive editing features in pretty much any code editor that supports LSP. Oh, and there's no `return` in Idris 2, only `pure` :)

mdm12 5y ago
Your description of a monad comprehension in Idris reminds me of computation expressions in F#[1]. Looks like I have one more programming language to dive into! [1] https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/computation-expressions https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
- sullyj3 5y ago
  A closer analogue is probably do-notation, which comprehensions are syntactic sugar for. Comprehensions can be terser for simple expressions, but for anything longer, do notation is generally more readable.
kaba0 5y ago
Isn’t haskell’s list comprehension can be used for monad comprehensions as well with a language extension? I remember using that once.
wk_end 5y ago
I want to like Idris - as a language it does so much right - but I still feel a little burnt. A few years ago were exciting times; Idris 1 had hit 1.0 and was humming along nicely, there was excellent tooling available, & Type-Driven Development with Idris had been published - a real printed book about practical coding with dependent types! Could reliable software be far behind? Would I maybe get to develop somewhere that took software engineering seriously in my lifetime? And then, with the possibility of success on the horizon, the Idris folk(s) got distracted by the QTT hype and decided to abandon ship so they could start on Idris 2. And, like, don't get me wrong - the QTT stuff is cool, and I'm a Rust fan in part because getting to encode linearity in your types is a real superpower - but it's so depressing that the world of practical dependent types feels just as far away now as it did ten years ago, after getting so excited about it five years ago. And it underscores what might be a bigger problem: at the end of the day - and by the Idris FAQ's own admission - Idris is a research project into practical dependent types, and Edwin Brady is an academic. Which means that when he gets interested in some other area of research, he's free to just...do that instead, or start over on Idris n+1, and leave Idris 1, 2, 3 ... n to wither.