IdrisExtSTGCodegen VS Idris2

Compare IdrisExtSTGCodegen vs Idris2 and see what are their differences.


A purely functional programming language with first class types (by idris-lang)
Our great sponsors
  • InfluxDB - Access the most powerful time series database as a service
  • SonarQube - Static code analysis for 29 languages.
  • SaaSHub - Software Alternatives and Reviews
IdrisExtSTGCodegen Idris2
6 36
20 2,106
- 1.6%
5.1 9.3
7 months ago 4 days ago
Idris Idris
GNU General Public License v3.0 or later GNU General Public License v3.0 or later
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.


Posts with mentions or reviews of IdrisExtSTGCodegen. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-05-19.
  • is dependent haskell still a thing?
    4 projects | /r/haskell | 19 May 2023
    In practice we will probably have an STG backend for Idris2 before a dependent Haskell, then at least you could link together Haskell and Idris code
  • What are you hyped about today?
    2 projects | /r/haskell | 15 May 2021
    I write an Idris2 backend which compiles to STG, yesterday we achieved to run the HelloWorld using functions from GHC.Base :)
  • Transpiling to GHC Core language
    4 projects | /r/haskell | 30 Apr 2021
    There is a WIP Idris2 to Ext-STG compiler:
  • BOB 2021 Andor Penzes - STG Backend for Idris2
    3 projects | /r/Idris | 29 Mar 2021
    Ah, the repo also has the slides of the talk, which are a nice first step to video-less content.
    3 projects | /r/Idris | 29 Mar 2021
    The github repo describes the project as "Pre-alpha, compiles a HelloWorld".
  • Next-gen Haskell Compilation Techniques
    4 projects | /r/haskell | 10 Jan 2021
    | The Idris language versions have always supported easy and modular code generation. I am working on the Idris-ExtSTG backend closely collaborating with Csaba. The progress can be followed here: . I am going to give a talk about my experiences at BobKonf 2021:


Posts with mentions or reviews of Idris2. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-05-08.
  • What are the current hot topics in type theory and static analysis?
    15 projects | /r/ProgrammingLanguages | 8 May 2023
    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.
  • New video! 2022 in Programming Languages
    8 projects | /r/contextfree | 28 Jan 2023
    Here's the full tab list: - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  • How to avoid right intendation?
    2 projects | /r/haskell | 17 Jan 2023
    Idris2 has a great syntax for this, see e.g. node018:
  • Data types with Negation
    2 projects | /r/ProgrammingLanguages | 16 Jan 2023
    I asked because it just baffles me any time I see a dependently typed language using unary numbers. I think to myself, "are these people even educated? Do they know about number systems?" I mean, cavemen were the last group using unary number system as their mainstay, and that was during the Paleolithic. Then they have issues open like this when they discuss optimizing those damn unaries. But this shouldn't even have been a problem for anyone even remotely related to programming! It's giving a terrible impression of dependently-typed languages. Getting rid of those should be the first step of popularizing them.
  • Ask HN: What piece of code/codebase blew your mind when you saw it?
    17 projects | | 31 Oct 2022
    The Idris codebase is quite beautiful. Given some understanding of how it works underneath, I find that there’s a succinct clarity in everything.

  • Least painful way to install idris2 on Windows or WSL?
    3 projects | /r/Idris | 14 Sep 2022
    is a known issue because both (+) and floating point literals are overloaded and there is no principled way of declaring that one defaulting mechanism should have priority over another one.
  • Building Idris2 for Apple silicon as of August 2022
    4 projects | /r/Idris | 26 Aug 2022
    This is an update on building Idris2 for `arm64` Apple silicon. My original guide was posted here a year ago: [Success building native Idris2 on an M1 Mac](\_building\_native\_idris2\_on\_an\_m1\_mac/) Some issues I encountered may get fixed, so these notes may best serve as guidance, as others work through this install in the future. I no longer have any Intel Apple machines in use. I am using MacOS Monterey 12.5.1, and a current homebrew installation that includes needed support such as gmp. I have successfully built idris2 on several M1 Mac minis, an M2 Macbook Air, and an M2 Ultra Mac Studio. These directions assume that you have read the install docs for Chez Scheme and Idris. ---- The official Cisco [Chez Scheme]( is still not `arm64` native. As before, one needs to install Racket's [fork](, which is `arm64` native and supports Idris2. Cloning the git repository and attempting to build, one encounters the error Source in "zuo" is missing; check out Git submodules using git submodule init git submodule update --depth 1 After these steps, the build is routine using the steps arch=tarm64osx ./configure --pb make ${arch}.bootquick ./configure --threads make sudo make install One can now confirm that `scheme` is `arm64` native using the command file $(which scheme) ---- The Idris 2 build was a delicate puzzle for me, harder than before. I got it to run by hand once, and then lost hours trying to recover what I did right by script. Here is a GitHub Gist for my install script: [Build script for Idris 2 on Apple silicon]( Here are the issues I encountered: Seven of the nine case statements involving ta6osx have had t `arm64`osx added, but not the remaining two. This threw me, as I imagined this had to be deliberate, and this was one of several problems that needed fixing. The bootstrap build creates a file `libidris2_support.dylib` but then can't find it later. One needs to attempt the bootstrap build twice, copying this file after the first attempt fails so that the second attempt will succeed. I copied this file everywhere needed, rather than to `/usr/local/lib` (homebrew doesn't like sharing a lane). The executable script itself can fail to find this `.dylib`, but the executable looks in the current working directory, so one could easily miss this during development. I also patch the executable so it changes into the executable's directory before calling it, where one of several identical copies of this `.dylib` can be found. `` included the curious note **NOTE**: If you're running macOS on Apple Silicon (arm64) you may need to run "`arch -x86_64 make ...`" instead of `make` in the following steps. The correct way to read this is that the author isn't sure. In fact, following this instruction will create `libidris2_support.dylib` with the wrong architecture, as I verified with a matrix of experiments (this or not, edit last two case statements or not). What is the status of official Apple silicon support for Chez Scheme and Idris 2? Searching Cisco [Chez Scheme]( issues for `arm64` yields several open issues, including [Pull or Backport ARM64 Support from the Racket Backend Version #545]( proposing to pull the Racket fork support for Apple Silicon. Searching pull requests for `arm64` yields [Apple Silicon support #607](, which doesn't work. The author doesn't explain why they are making this effort, rather than pulling the Racket fork changes. Others note that the author also ignores prior art in their naming conventions. Searching [Idris 2]( issues for `arm64` yields [Racket cannot find libidris2_support on Mac M1 #1032](, noting the `.dylib` issue I address, and linking to [Clarify installation instructions on macOS (M1) #2233]( asking for better Apple silicon directions, which backlinks to my first [reddit post](\_building\_native\_idris2\_on\_an\_m1\_mac/). The other backlinks I could find are automated scrapes not of interest. There are no pull requests for `arm64`. I admire the Idris project and I want it to succeed. It needs macOS users. However, I'm unlikely to rely on Idris2 for my own work until parallelism is better supported. I'd love someone to change my mind if I'm misreading the situation.
  • Programmable type systems?
    3 projects | /r/ProgrammingLanguages | 24 Jun 2022
  • Idris 2: Quantitative Type Theory in Practice
    4 projects | | 24 Jan 2022
    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 ( 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. (

    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 runtime-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).

  • From TypeScript to ReScript
    12 projects | | 12 Jan 2022
    Idris 2 looks promising... I suggest keep an eye on it

What are some alternatives?

When comparing IdrisExtSTGCodegen and Idris2 you can also consider the following projects:

purescript - A strongly-typed language that compiles to JavaScript

lang-team - Home of the Rust language design team.


rust - Empowering everyone to build reliable and efficient software.

rfcs - RFCs for changes to Rust

idris - A Dependently Typed Functional Programming Language

genType - Auto generation of idiomatic bindings between Reason and JavaScript: either vanilla or typed with TypeScript/FlowType.

bincode - A binary encoder / decoder implementation in Rust.

bs-material-ui - ReScript bindings for Material-UI

melange - A mixture of tooling combined to produce JavaScript from OCaml & Reason

lwt - OCaml promises and concurrent I/O

manual-stg-experiment - Manually constructed STG programs compiled with the standard GHC codegen backend.