Author here. Glad to see so many people interested.
I think people will find this useful as an example is programming in Idris. While there are many other resources around, this fills a niche as a fairly complete, self contained program.
Since I wrote it, I've noticed that my programming style is not very standard, especially my approach to proofs, so I'm still working on it.
Thanks for this - I've bookmarked it to read later. It looks like you've explained everything pretty thoroughly in the readme, and looks like an excellent example for getting started.
I'm new here. Is there a new language mentioned on Hacker News this frequently? I have skimmed the front page and seen at least a dozen or so being mentioned in the last month.
I think this past month has been a bit of an outlier with new languages, such as Avail, being posted. That said, I wouldn't count Idris as one of them - it's been around for a little while now, and in the community of people familiar with purely functional languages, it's probably about as well known as Elm or Agda: If talking to a Haskeller, there's a good chance they've at least heard of it.
Of course, it's all relative - this community does have a good number of early language adopters and people involved in programming language research. At the other end of the spectrum, just a few years ago, I met a Java developer who, at the time, hadn't even heard of C# - I'd imagine he'd've been quite shocked by the languages talked about here.
Compared to other darling languages like Go, Haskell and Rust, I think Idris has a comparatively low profile. It pops up occasionally, but not all that much. I'd be surprised if it was a dozen in a month.
I think the idea of comparing languages based on a variety of tasks is interesting. We've all seen "hello world" in many languages[1], but including other tasks (like 2048) would provide a much richer summary of the language. Thus, a language could be efficiently summarized by tuples of "complexity parameters:"
- lines of code
- number of characters
- total number of tokens
- number of blank lines (which might approximate modularity)
- ...etc
For example, using "hello world" and 2048 as code targets:
complexity("java", "num-characters") would yield: (115, 1269).
complexity("python3", "num-characters") would yield: (25, 2048).
I think people will find this useful as an example is programming in Idris. While there are many other resources around, this fills a niche as a fairly complete, self contained program.
Since I wrote it, I've noticed that my programming style is not very standard, especially my approach to proofs, so I'm still working on it.