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` :)
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.
[1] https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
GHC has an enormous amount of machinery to infer types and check equality automatically. I wonder if Idris has anywhere near that much. Automatic inference is why Haskell resisted dependent types until quite recently, though there were already some cases that it couldn't do automatically.
As for pure vs return, that's because the typeclass system was rearranged pretty recently. Before that, Monad instances weren't necessarily also Applicative. "return" was kind of cool in that you could write what looked like imperative subroutines that returned values.
!foo in Idris sounds like foo >>= whatever or whatever =<< foo in Haskell.
Idris 2 has more or less no type inference at all. I think maybe type inference for dependent types isn't decidable, or something like that?
But I know that they are interested in adding inference to Idris 2 in certain cases that can be proven to work correctly.
It's definitely a deficiency in the Idris user experience vs the Haskell user experience.
> !foo in Idris sounds like foo >>= whatever or whatever =<< foo in Haskell.
Idris has >>= as well. But see here for a nice demo of ! and other "do"-related syntax: https://idris2.readthedocs.io/en/latest/tutorial/interfaces....
Imo inference is a bit overrated anyway. I find annotations to be very useful.
There's a series of steps here:
- "Static type annotations are too verbose, dynamic languages allow you to avoid the ceremony." - "But Hindler Milner type systems can infer the types, so you usually don't have to write the type annotations!" - "Writing type annotations is useful anyway, because it serves as valuable documentation, makes reasoning about the program easier, and results in more useful type errors."
Thinking about it more now, there's another step: - "If you have good type inference, you can use editor tooling (eg the LSP) to automatically insert the type signatures for you!"
Part of the usefulness of top level annotations in Haskell is that if your program has a type error, inference can fail in multiple ways. I.e. the unification algorithm might assign type T to your function F and chug along happily until it runs into a conflict in some unrelated part of the program, then throw an unhelpful error message in the case where T wasn't the type that you intended for F. By annotating F with the type you really want, you get an error message that does a better job pinpointing the problem.
This is less of an issue in ML, since ML's type system is less general than Haskell's, so the inference algorithm can't go as crazy, and you usually get good error messages even without annotations.
I'm more saying that I'm fine with type system features that break global inference, as long as there's still local inference that's usually good enough in practice.
What does affect the usability of the language is when (a) the line in the sand isn't very clear from an end-user point of view [see simplified subsumption in GHC 9, for example], or (b) the line is on the wrong side of simple features [see monomorphic local bindings, for example].
I guess what I'm saying is that Idris having minimal type inference is kind of terrible, and the excuse that it's not decidable for dependent types is a flimsy one.
Part of the fun of being a research language is that you don't know everything up-front!
We made Applicative a superclass of Monad around 2015, and since then return has been a historical artifact (with a dangerously misleading name).
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.