PRpretext·Nov 16, 2022Submission
Idris 2: a purely functional programming language with first class types
4 points · Open discussionidris-lang
Idris2
Idris2020–2026
idris-lang / Idris2
Idris2
A purely functional programming language with first class types
17Distinct people
21Mentions
1Explicit recommenders
3.1KGitHub stars
What to know before exploring
What it is
A purely functional programming language with first class types
GitHub
Where it is used
No documented product use was verified in the last source check.
What people are saying
There are some minor changes, but they are documented in detail [1]. The Idris2 repository maintains tests to detect any further divergence from the book [2]. I highly…
mx00s used a recommendation phrase. One indexed comment matches. This is a phrase match, not a verdict.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 8–Nov 15 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/15/2026, 10:01:16 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year21 dated mentions
Observed mentions: 2020-05-20 14:22:44 UTC to 2026-07-27 16:09:30 UTC.
* An incomplete calendar period is marked with an outlined bar. Its count is not directly comparable with a full period.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 5 | 2 | 3 |
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 3 | 1 | 2 |
| 2022 | 2022-01-01 00:00:00 UTC | 2023-01-01 00:00:00 UTC | 5 | 1 | 4 |
| 2023 | 2023-01-01 00:00:00 UTC | 2024-01-01 00:00:00 UTC | 5 | 1 | 4 |
| 2024 | 2024-01-01 00:00:00 UTC | 2025-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2025 | 2025-01-01 00:00:00 UTC | 2026-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2026 (partial) | 2026-01-01 00:00:00 UTC | 2027-01-01 00:00:00 UTC | 1 | 0 | 1 |
What Hacker News says
5 sourcesThe Idris codebase is quite beautiful. Given some understanding of how it works underneath, I find that there’s a succinct clarity in everything.
https://github.com/idris-lang/Idris2
In Ask HN: What piece of code/codebase blew your mind when you saw it?I was a bit disappointed with linearity in QTT as I couldn't figured out 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 binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (https://github.com/idris-lang/Idris2/issues/613)
The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type.
On the other hand, only affecting the parameter bindings makes it really easy to use run
Read the rest
time-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions.
ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).
Hi there,
I'm a phd student working on Idris and I used to work with Edwin on this, if you want more info or want to see more practical applications of idris2, Dependent types, or QTT, here are a couple links:
- 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
- my own projects in idris include a purely declarative server library where you give the API and the server is completely implemented and instantiated from your description https://gitlab.com/avidela/recombine
In Idris 2: Quantitative Type Theory in PracticeIdris 2 looks promising... I suggest keep an eye on it https://github.com/idris-lang/Idris2
In From TypeScript to ReScript