Hacker GitHub

← All repos

idris-lang/Idris2

View on GitHub ↗ ★ 3,102 Idris

A purely functional programming language with first class types

21 mentions on Hacker News by 17 people: 5 stories, 16 comments · first 2020-05-20 · latest 2026-07-27

Mentions per year 21 mentions · busiest year 2020 (5)
20082026
AllStoriesComments NewestTopOldest
  1. …happened to Idris? Is that still being developed? Edit: Looks like they are working on Idris 2 https://github.com/idris-lang/Idris2
    comment by dmix · 2026-07-27 · in We have proof automation now
  2. …the entire bootstrap chain from GHC. sadly, it was pretty much ignored, and later abandoned: https://github.com/idris-lang/Idris2/pull/1990 )
    comment by attila-lendvai · 2025-11-23 · in Racket v9.0
  3. …that may be a bit more subtle. I'll have to look at your repo to see what you mean by that. [1]: https://github.com/idris-lang/Idris2 [2]: https://github.com/dunhamsteve/newt
    comment by dunham · 2025-05-31 · in De Bruijn notation, and why it's useful
  4. …thought it was intended to blend the strengths of proof assistants and general purpose programming: https://github.com/idris-lang/Idris2
    comment by aeonik · 2023-10-28 · in Can the language of proof assistants be used for general purpose programming?
  5. …to a general purpose language that also has a more advanced type system for the theorum proving. https://github.com/idris-lang/Idris2
    comment by aeonik · 2023-10-27 · in Lean4 helped Terence Tao discover a small bug in his recent paper
  6. …environment and the compiler checks that the manipulation of deBruin levels and indices is correct: https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...
    comment by dunham · 2023-07-08 · in How to keep lambda calculus simple
  7. …to use a trampoline-like thing. There is a nice explanation of how it works at the top of the file: https://github.com/idris-lang/Idris2/blob/main/src/Compiler/... One could argue that it's not "full" TCO, but it does cover a lot of…
    comment by dunham · 2023-02-27 · in Idris 2 0.6.0 is now available for the JVM
  8. …understanding of how it works underneath, I find that there’s a succinct clarity in everything. https://github.com/idris-lang/Idris2
    comment by AnthonBerg · 2022-10-31 · in Ask HN: What piece of code/codebase blew your mind when you saw it?
  9. …how to create a safe API around a resizable array. The example given in the paper is a LinArray ( https://github.com/idris-lang/Idris2/blob/main/libs/contrib/... ). Unfortunately, as the community discovered, a user can "leak" a non-linear…
    comment by phlip9 · 2022-01-24 · in Idris 2: Quantitative Type Theory in Practice
  10. …- idris2 is written in idris2 so that's a good example of a big program using dependent types https://github.com/idris-lang/Idris2 - we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries…
    comment by lang_agnostic · 2022-01-24 · in Idris 2: Quantitative Type Theory in Practice
  11. Idris 2 looks promising... I suggest keep an eye on it https://github.com/idris-lang/Idris2
    comment by fbn79 · 2022-01-12 · in From TypeScript to ReScript
  12. …lke like minikanren ( https://github.com/webyrd/Barliman ) where you give test cases and Idris2 ( https://github.com/idris-lang/Idris2 ) where you give type constraints as a tool for building programs.
    comment by nyberg · 2021-06-18 · in TDD from the Factorio Team
  13. Speaking of "rest of", this is the file in question: https://github.com/idris-lang/Idris2/blob/master/src/Idris/E...
    comment by ricree · 2021-03-01 · in A mundane use of dependent types
  14. …where necessary[2], at least sometimes. [0]: https://github.com/rust-lang/rfcs/issues/414 [1]: https://github.com/idris-lang/Idris2/tree/master/libs/base [2]: https://github.com/idris-lang/Idris2/blob/master/libs/base/D...
    comment by creata · 2020-10-20 · in Assorted Thoughts on Zig and Rust
  15. …the Chez Scheme code generator are located here (similar locations for the other code generators): https://github.com/idris-lang/Idris2/blob/master/src/Compile... , https://github.com/idris-lang/Idris2/blob/master/src/Compile... ,…
    comment by Zigma · 2020-09-28 · in Show HN: Erlang code generator for Idris 2
  16. …will leave a lasting impression. [1] https://idris2.readthedocs.io/en/latest/typedd/typedd.html [2] https://github.com/idris-lang/Idris2/tree/master/tests/typed...
    comment by mx00s · 2020-05-26 · in Why is Idris 2 so much faster than Idris 1?