Your question is fair, and it's unfair you're being downvoted. Idris is a dependently typed programming language.
If you imagine a "cube" of fundamental language features, on one corner is "the simply typed lambda calculus" which you can think of as old-school C. Along each of three edges we add a fundamental language feature: parametric polymorphism (values that depend on their type; think 'C# generics'), type constructors (types that depend on types; something akin to C++ template types like `vector` but not like `std::sort`), and dependent types (types that depend on values; but definitely not restricted like `std::array`; something more like MacroC or `enable_if`).
There's not a lot of good analogies for this stuff in commonly used programming languages because the big languages are really basic (not simple!) compared to the advanced stuff the programming language theorists have gotten up to.
Your question is fair, and it's unfair you're being downvoted.
I agree partly; I didn't downvote but I think in this case the downvotes are not that weird; it's quite well known what Idris is in HN circles, but that's not the point; the article has links that tell you (pointing to idris-lang) and google idris edwin brady (which is on top of the article) will get you more than you want to know most likely but at least enough to know what it is. So it is the absolute bare minimum to open an article and pop in; 'what is this?' if it's not in the first line of an article which I think is not great. A little bit more I do expect from this place; like clicking on the article, immediately recognising it as a language (that's clear within seconds of scrolling the article I would say) and then maybe come back with 'what is dependently typed?' or something. But going from opening the article to hitting wikipedia explaining dependently typed languages is ... well, not much more work than doing nothing and just popping 'huh?' in here imho.
Edit: actually, just google 'idris2' and you have in the first line exactly what, who, why etc.
Comments
What is Idris?
Critical info missing.
Your question is fair, and it's unfair you're being downvoted. Idris is a dependently typed programming language.
If you imagine a "cube" of fundamental language features, on one corner is "the simply typed lambda calculus" which you can think of as old-school C. Along each of three edges we add a fundamental language feature: parametric polymorphism (values that depend on their type; think 'C# generics'), type constructors (types that depend on types; something akin to C++ template types like `vector` but not like `std::sort`), and dependent types (types that depend on values; but definitely not restricted like `std::array`; something more like MacroC or `enable_if`).
There's not a lot of good analogies for this stuff in commonly used programming languages because the big languages are really basic (not simple!) compared to the advanced stuff the programming language theorists have gotten up to.
I agree partly; I didn't downvote but I think in this case the downvotes are not that weird; it's quite well known what Idris is in HN circles, but that's not the point; the article has links that tell you (pointing to idris-lang) and google idris edwin brady (which is on top of the article) will get you more than you want to know most likely but at least enough to know what it is. So it is the absolute bare minimum to open an article and pop in; 'what is this?' if it's not in the first line of an article which I think is not great. A little bit more I do expect from this place; like clicking on the article, immediately recognising it as a language (that's clear within seconds of scrolling the article I would say) and then maybe come back with 'what is dependently typed?' or something. But going from opening the article to hitting wikipedia explaining dependently typed languages is ... well, not much more work than doing nothing and just popping 'huh?' in here imho.
Edit: actually, just google 'idris2' and you have in the first line exactly what, who, why etc.