Idris Feedback Cycle 0

[andrevidela]

Closing date: May 30th

---

Hi everyone,

Today is the start of the 2026 Idris Developer Meeting and for this I would like to propose a new way to move the project forward, one that serves users, contributors, and casual observers.

As of today, and as has been the case for many years, nobody works fulltime on Idris, contributors are volunteers that employ their free time to work on the compiler, libraries and language ecosystem. What is more, Idris has more and more become a community-owned project rather than one with a singular individual carrying its direction.

Both those aspects obscure the direction of Idris as a project. It is hard to know what is the project's current status, future direction, and overall plan. For language contributors it is hard to identify the needs of the community and use that information to prioritise their time effectively. For users, it is impossible to know if their issues are going to be addressed or are even acknowledged. And for external viewers, it is not clear if the project is even alive and what's the deal with it.

We need a process that recognises the limitation of the project, part time contributors, community ownership and address the visibility issues exposed above. I propose we start a new process that called the "Idris feedback cycle".

What is the Idris Feedback Cycle

Starting from today and until the end of the month, one issue will be opened title "Idris feedback cycle N". On this issue, community members can provide feedback about the idris project, not particularly about a bug in the compiler or a strange behaviour, but about some experience they have had and would like to share. Other members can reply supporting the feedback or providing help, resources and point toward areas of the ecosystem related to the feedback (documentation, issue number, project page).

A feedback cycle runs for a set amount of time, at the end of which, the issue is closed and a new one is opened with the number incremented by one. The product of the feedback cycle is the discussion thread generated during that time. With it, contributors, can get a snapshot of the community's needs and wants and make decisions upon them. We could release a distilled version on the website, make posts on social media, or use it as reference for design document. Heck someone could make a youtube channel reviewing what was discussed and why. The discussion thread is its own resource for the community to use, and my assumption is that getting multiple of them across time should give a general idea of the project's direction, regardless of any one individual's goals or aspirations.

Goals

• Provide visibility over the project's current status and future plans
• Give a space for the community to contribute ideas and project out their needs
• Give contributors a way to gauge the needs of the community

Non-goals

• Assign tasks and responsibilities to individuals
  • Individuals may express interest in contributing or participating in some developments but this is purely indicative and not prescriptive.
• Commit to a release schedule, roadmap, or promise of delivery
  • I plan to keep those feedback documents running on a regular basis but the delivery of the feedback document is detached from any form of software delivery.
• Enable authority and or authoritative statements
  • Something said or even promised here holds no grounds over anyone, e.g: "you said this would be done and it's not and I demand it is." is a no-go

Guidance for Feedback

The Idris Feedback Cycle isn't a space to vent, complain, or demand outcomes. Constructive feedback is patient and inquisitive, messages that aimlessly complain, demand something to be done, display outrage, or attack someone's character will be remove. The usual community rules apply and will be enforced.

Before providing feedback, one must understand the core values of the Idris Programming Language:

• Types to help the programmer, not impede them.
• Software to benefit the people.
• Encourage new knowledge and understanding.
• Allow verification, don't require it.

We ask anyone contributing this document to understand and adhere to those core values as a way to preserve the spirit of the language.

Example feedback

I've been trying to use Idris for education but installing idris on Windows has been very difficult, any plans to address this?

LSP is buggy but I can't figure out how to reproduce my errors anyone else has this?

I'm trying to port my library from Java to Idris but I can't find a library that handles XML the way I used to, I can't parse it auotmatically from my data types

I'm trying to use quantities but the compiler isn't letting me quantify over them like I expected, is this not a feature?

Example Responses

Windows support has been spotty but we have tutorials for how to install Idris with WSL and chocolatey. Do you have a specific class of errors that we can look into?

Hey there, LSP issues are over on the idris2-lsp project. Could you take a look and tell us which one looks the most like what you're experiencing? Unless we know exactly what the error your experiencing is, we can't narrow it down.

There is one library for XML manipulation in Idris but it's not actively maintained. There is an issue over there for using elaboration reflection with data structures but it's not implemented. Maybe I could have a go at implementing it in the next few weeks

Idris2 has quantities but it doesn't have quantity polymorphism, this is an area of research but nobody is actively implementing it in the compiler. If you're interested in quantity polymoprhism, I suggest you try Granule.

Note that some of those could be threads or questions on zulip.

Closing words

This process is a proposal, an attempt, an idea. If it does not work, then we should not use it, or change it until it suits the needs of the community. Likewise, things like core values and project goals are subject to change to serve the community. Please leave you feedback not only about the language, but also about the processes around the language such that we can keep improving. There are many meta-level questions that are currently unadressed an now is a good time to think about them and propose something, for example. Who even is a maintainer? What processes make a proposal accepted or rejected? etc. In other words, the space of topics to cover is very large and I hope we can all find a way to converge toward a common understanding.

[andrevidela]

Some things I've noticed for myself:

• I'm not sure what's the status of the website? Does the repo actually deploy to prod? https://github.com/idris-lang/idris-lang.github.io What's going on with the two opened issues and the mentions about www subdomains on zulip?
• I plan to finish implement binding application #3614 eventually but I got bogged down designing the error messages .Maybe I should simply ship it and make the error messages another PR, but this is also how we end up with half-baked features and poor UX
• I've done a good amount of work on compiler architectures using containers and I'd love to deploy some of those ideas in the Idris compiler but I'm not sure how much of this is a good idea or not. I know it's the kind of thing that we won't know until we try out, but the Idris compiler might not be the right place to try those ideas. I'd love to know what people think
• I also started working on another try at multicore module compilation here https://github.com/andrevidela/Idris2/tree/multicode-module-compilation but I couldn't finish the last 90% after the first 90%
• I've seen many discussions about moving away from Github, but haven't seen much consensus about how the transition should be handled, what goals it should achieve and who is going to do it

[Carrotstrip]

As a casual observer moving towards user; folks have been very responsive and helpful on Zulip with my beginner questions, and I'm probably not going to use these threads over Zulip for that sort of thing unless it becomes very clear that the IFC is the more active option where all you smarties are hanging out. Even then, I do prefer something like Zulip; to put it in terms that we can all get behind, I think there's value in giving a message a more precise type by putting it in a topic thread in a particular channel, rather than just appending it to a stream of untyped messages on a Github issue. Also I think keeping discourse in one place as much as possible is a good idea. From this perspective maybe Github discussions would have been best, but of course there are other considerations, and the Zulip has been great for me.

https://this-week-in-rust.org/ has got to be the gold standard for at least the "digest and present" piece of this proposal, but I imagine it's quite a lot of work to put together, especially since Rust is a much bigger project.

Finally, I'm not sure where the core values came from, but they feel a bit confused to me:

• Types to help the programmer, not impede them.
• Allow verification, don't require it.
  Clearly technical
• Software to benefit the people.
  Clearly social
• Encourage new knowledge and understanding.
  Interpretable as technical or social?

To me, "core values" suggests the social domain, and something like "design principles" or "Zen of Idris" (a la https://peps.python.org/pep-0020/) suggests the technical. I think these are both very much worth having and discussing, but they ought to be different categories.

[l-monnier]

Thank you for the initiative!

• How easy should Idris be for functional programming beginners? Is it an aspiration to be a first functional programming language to learn or is that left to other languages such as Haskell?
• Are there any ideas/long-term thoughts to have the Idris website programmed in Idris?
• I'm working on a new version of the Markdown library and hope to be able to ship it this summer.
• Once done, I'll make a pull request for a dark mode for the Idris2 Documentation Browswer.
• Then, my other project is a HTML EDSL idris2-html which works already well but isn't complete enough to be added to Pack yet.
• My ultimate goal is to have a static website generated in Idris. It's there, but it requires a lot of improvements. Once good enough, I'll publish a SSG library/app in pack, but that's really for the long-term.

[l-monnier]

• I've seen many discussions about moving away from Github, but haven't seen much consensus about how the transition should be handled, what goals it should achieve and who is going to do it

I believe what is key in your question, is "what goals it should achieve". Without a clear assessment of GitHub compared to alternatives in light of certain objectives (reliability/simplicity/philosophy/costs/independence/etc.), it is difficult to even reach the conclusion if this would actually be necessary at all.

On the other hand, it's a healthy discussion to have, as over the years, it looks like that many aspects of GitHub are getting worse. So, it's good that the community had at least some talks about it.

[andrevidela]

Are there any ideas/long-term thoughts to have the Idris website programmed in Idris?

I don't think I've heard about anything in that direction but:

My ultimate goal is to have a static website generated in Idris. It's there, but it requires a lot of improvements. Once good enough, I'll publish a SSG library/app in pack, but that's really for the long-term.

The idris website would be a perfect opportunity to dog food the project!

How easy should Idris be for functional programming beginners? Is it an aspiration to be a first functional programming language to learn or is that left to other languages such as Haskell?

This is just my opinion, but I believe Idris should be as accessible as possible for general purpose programming, not necessarily "as a functional programming language". Of course, we are light-years away from this, but the intention still matters. It has definitely guided my priorities when working on bug or features (like good error messages, catching up on industry standard features, and working on industry-ready library)

About github, I can definitely see some signs that it is time to move on like the enshittification of services (actions, private gh pages), decreasing uptime, increasing push towards AI features, etc. I'm not happy with this turn of events, but it is also not necessarily clear to me that other places would fulfil our needs better. maybe the first step would be to scope out what an alternative would need to do to be considered worth the move?