4 ms·

Anyone else finding this documentation is pretty hard to navigate? Makes me think this isn't a serious language, but rather an academic toy or resume builder.

andrewmcwatters 4y ago
The main repository is in the top 1% of stargazed repositories on GitHub, and the project has a mailing list, Discord server, IRC, AND Slack. It has been forked over 300 times, and has over 100 contributors. What in the world counts as "serious" to some of you people? Sometimes I read HN and ask myself if people here know at all how hard it is make something people want, and how many people know what the real-world thresholds are for understanding when you have made something that people want. I guess if everyone hasn't heard of it, people here don't think it's serious.
- bobleeswagger 4y ago
  [flagged]
  - andrewmcwatters 4y ago
    I mean you tell me, which would be bullying to you? You work for years on something and someone tells you it's not "serious" because they haven't learned to browse a source tree, or the guy telling him to read a little more? Either way, I apologize for how it came off.
    - bobleeswagger 4y ago
      > someone tells you it's not "serious" because they haven't learned to browse a source tree "Fuck this stranger for not learning something I know how to do!"
- mejutoco 4y ago
  I find Idris incredibly interesting. Specially combined with the output it can generate in other languages. The book of it is also a masterpiece, even if you never program in it. Already lots of "serious" hacked together programming languages. The only downside I see if the lack of a package manager.
- Kranar 4y ago
  >What in the world counts as "serious" to some of you people? For a programming language? Would be good to know what projects have used it. Most languages people develop are done as either a hobby or to serve some kind of research/academic purpose. Is Idris used for any production grade software?
CoastalCoder 4y ago
> Anyone else finding this documentation is pretty hard to navigate? I can't speak to these docs in particular, but I think documentation regarding type-system in general can be hard to digest. And it probably varies by reader. E.g., some people find "The Little Typer" [0] to be a wonderful intro to its topic. Personally, I find the writing style impenetrable. > Makes me think this isn't a serious language, but rather an academic toy or resume builder. If the documentation turns out to be useless to the majority of readers, then you might be right that it's a sign of under-investment. I'm not sure if that's happening here. There was a good interview on Corecursive [1] about Idris, so IMHO that's some evidence that some people are serious about the language. [0] https://mitpress.mit.edu/9780262536431/the-little-typer/ https://mitpress.mit.edu/9780262536431/the-little-typer/ [1] https://corecursive.com/006-type-driven-development-and-idris-with-edwin-brady/ https://corecursive.com/006-type-driven-development-and-idri...
wk_end 4y ago
TBH I actually think the documentation for Idris is quite good, but your overall point is correct: it's definitely somewhere between "academic toy" and "serious language". It's not really usable for anything real world at the moment, and - like I comment every time it pops up here - just as it was building up momentum the author scrapped the whole thing and started over (Idris 2), and even though I've been making that comment for years it still hasn't recovered. The book everyone recommends to read on it is based around a dead version of the language; the tooling it has you use (which is a huge part of working with a dependently-typed language) depends on Atom, which is now dead, and Idris 2 still doesn't have comparable IDE support. I find it really frustrating because I like the language a lot, and I want to be using dependent types in my real life ASAP. Right now I'd be looking more towards Lean, though, which seems to be more modern and developing rapidly.
- hjadal 4y ago
  The Atom implementation has been replicated in VSCode and works alright. It was good enough for me to learn how Idris worked and go through the book's exercises.
revskill 4y ago
I think it's the chicken-egg issue. Firstly it's not the tools'fault. But overall, the culture of using that tool made it worse. For example, most of readthedocs documentation i've seen is nothing better a wiki page, where you have a bunch of links to click on in a messy way somehow. So i guess your issue with this one, is you're missing some structured knowledge with this page.

andrewmcwatters 4y ago

The main repository is in the top 1% of stargazed repositories on GitHub, and the project has a mailing list, Discord server, IRC, AND Slack. It has been forked over 300 times, and has over 100 contributors. What in the world counts as "serious" to some of you people? Sometimes I read HN and ask myself if people here know at all how hard it is make something people want, and how many people know what the real-world thresholds are for understanding when you have made something that people want. I guess if everyone hasn't heard of it, people here don't think it's serious.

bobleeswagger 4y ago
[flagged]
- andrewmcwatters 4y ago
  I mean you tell me, which would be bullying to you? You work for years on something and someone tells you it's not "serious" because they haven't learned to browse a source tree, or the guy telling him to read a little more? Either way, I apologize for how it came off.
  - bobleeswagger 4y ago
    > someone tells you it's not "serious" because they haven't learned to browse a source tree "Fuck this stranger for not learning something I know how to do!"
mejutoco 4y ago
I find Idris incredibly interesting. Specially combined with the output it can generate in other languages. The book of it is also a masterpiece, even if you never program in it. Already lots of "serious" hacked together programming languages. The only downside I see if the lack of a package manager.
Kranar 4y ago
>What in the world counts as "serious" to some of you people? For a programming language? Would be good to know what projects have used it. Most languages people develop are done as either a hobby or to serve some kind of research/academic purpose. Is Idris used for any production grade software?

CoastalCoder 4y ago

> Anyone else finding this documentation is pretty hard to navigate? I can't speak to these docs in particular, but I think documentation regarding type-system in general can be hard to digest. And it probably varies by reader. E.g., some people find "The Little Typer" [0] to be a wonderful intro to its topic. Personally, I find the writing style impenetrable. > Makes me think this isn't a serious language, but rather an academic toy or resume builder. If the documentation turns out to be useless to the majority of readers, then you might be right that it's a sign of under-investment. I'm not sure if that's happening here. There was a good interview on Corecursive [1] about Idris, so IMHO that's some evidence that some people are serious about the language. [0] https://mitpress.mit.edu/9780262536431/the-little-typer/ https://mitpress.mit.edu/9780262536431/the-little-typer/ [1] https://corecursive.com/006-type-driven-development-and-idris-with-edwin-brady/ https://corecursive.com/006-type-driven-development-and-idri...

wk_end 4y ago

TBH I actually think the documentation for Idris is quite good, but your overall point is correct: it's definitely somewhere between "academic toy" and "serious language". It's not really usable for anything real world at the moment, and - like I comment every time it pops up here - just as it was building up momentum the author scrapped the whole thing and started over (Idris 2), and even though I've been making that comment for years it still hasn't recovered. The book everyone recommends to read on it is based around a dead version of the language; the tooling it has you use (which is a huge part of working with a dependently-typed language) depends on Atom, which is now dead, and Idris 2 still doesn't have comparable IDE support. I find it really frustrating because I like the language a lot, and I want to be using dependent types in my real life ASAP. Right now I'd be looking more towards Lean, though, which seems to be more modern and developing rapidly.

hjadal 4y ago
The Atom implementation has been replicated in VSCode and works alright. It was good enough for me to learn how Idris worked and go through the book's exercises.

revskill 4y ago

I think it's the chicken-egg issue. Firstly it's not the tools'fault. But overall, the culture of using that tool made it worse. For example, most of readthedocs documentation i've seen is nothing better a wiki page, where you have a bunch of links to click on in a messy way somehow. So i guess your issue with this one, is you're missing some structured knowledge with this page.