Third party Libraries - idris-lang/Idris2 GitHub Wiki
This page lists third party libraries that use Idris. You can find similar listings in idris-community and idris2-pkgs. The list starts with package managers, which can be used to install other libraries.
Package Management
| Package | Description | Repository |
|---|---|---|
| pack | A package manager with curated package collections for Idris2 | stefan-hoeck/pack |
| pack-db | Curated Package Collections for Idris2 | stefan-hoeck/pack-db |
| sirdi | Package manager for idris | eayus/sirdi |
| inigo | Package manager | idris-community/inigo |
| sae | Build tool and package manager | DoctorRyner/sae |
| idris2-pkgs | An unofficial Idris2 package repository for Nix | claymager/idris2-pkgs |
Pretty Printers
| Package | Description | Repository |
|---|---|---|
| pretty-show | Port of Haskell's pretty-show library | stefan-hoeck/idris2-pretty-show |
| prettier | Bernardy style pretty printer | Z-snails/prettier |
Data
| Package | Description | Repository | Sirdi Manifest |
|---|---|---|---|
| comonad | Comonads in Idris2 | stefan-hoeck/idris2-comonad | ? |
| rhone | Arrowized functional reactive programming based on monadic stream functions | stefan-hoeck/idris2-rhone | ? |
| sop | Generic representation of data types as sums of products | stefan-hoeck/idris2-sop | ? |
| json | (Automatically derivable) JSON marshallers for Idris2 | stefan-hoeck/idris2-json | ? |
| fvect | Fin-based Vect type | mattpolzin/idris-fvect | ☑️ |
| dhall | Dhall implementation for Idris2 | alexhumphreys/idrall | ? |
| idris2-xml | XML | madman-bob/idris2-xml | ? |
| indexed | Indexed Functor, Applicative, Monad, etc. | mattpolzin/idris-indexed | ? |
| typed-containers | Verified Red-Black Tree (and hopefully others in the future) | L-as/rbtree | ? |
| dinwiddy | Dependently typed N-dimensional array type signatures for Idris (2) | bobbbay/dinwiddy | ? |
| snocvect | A vector type with reverse-vect semantics | mattpolzin/idris-snocvect | ☑️ |
Testing
| Package | Description | Repository |
|---|---|---|
| hedgehog | A property based testing library with integrated shrinking | stefan-hoeck/idris2-hedgehog |
| replica | A golden value based testing executable | berewt/replica |
JavaScript
| Package | Description | Repository |
|---|---|---|
| dom | Extensive DOM and Web bindings for Idris2 | stefan-hoeck/idris2-dom |
| dom-mvc | SPA a la TEA | stefan-hoeck/idris2-dom-mvc |
| rhone-js | Reactive single page web apps in Idris2 | stefan-hoeck/idris2-rhone-js |
| webidl | WebIDL parser and Idris2 code-generator | stefan-hoeck/idris2-webidl |
Elaborator Reflection
| Package | Description | Repository |
|---|---|---|
| elab-util | Tutorials and utilities for Idris2's new elaborator reflection | stefan-hoeck/idris2-elab-util |
Persistence
| Package | Description | Repository |
|---|---|---|
| pg | Partial Postgres bindings | mattpolzin/pg-idris |
Effect Systems
| Package | Description | Repository |
|---|---|---|
| effect | Fused algebraic effects | russoul/idris2-effect |
| freer | Stack safe, efficient freer monad implementation | stefan-hoeck/idris2-freer |
Concurrency
| Package | Description | Repository |
|---|---|---|
| coop | Simple concurrency without parallelism | buzden/idris2-coop |
Data science
| Package | Description | Repository |
|---|---|---|
| idris2-python | A python backend for Idris2 | madman-bob/idris2-python |
| idris2-python-pure | A pure python backend for Idris2 | galtys/idris2-python-pure |
| idris2-jupyter | A Jupyter kernel for Idris2 (pre-alpha!) | madman-bob/idris2-jupyter |
| idris2-json-schema | Generate Idris 2 data types from a JSON Schema (pre-alpha!) | madmanbob/idris2-json-schema |
| idris2-jupyter-vega | A Vega display plugin for the Idris 2 Jupyter kernel for displaying graphs and figures | madman-bob/idris2-jupyter-vega |
| idris-data-frame | An (incomplete) attempt to replicate the feel of R's tidyverse/dplyr | ziman/idris-data-frame |
| idris2-odf | A OpenDocument format reader library with a low-level interface for reading from/writing to spreadsheet cells | madman-bob/idris2-odf |
| spidr | Accelerated linear algebra | joelberkeley/spidr |
Misc.
| Package | Description | Repository |
|---|---|---|
| experimental | Experimenting with recent additions to the compiler | stefan-hoeck/idris2-experimental |
| ncurses | Partial NCurses bindings | mattpolzin/ncurses-idris |
| hello-idris2 | Template idris2 project with testing and CI already setup | alexhumphreys/hello-idris2 |
| sdl | Experimental bindings to libsdl2 | ShinKage/idris2-sdl |
| idrisGL | A 2D graphic library for Idris 2. | ECburx/Idris2GL |
| Graphviz/DOT Parser | Lexer+Parser for the Graphviz/DOT language (.gv files) |
CodingCellist/idris2-dot-parse |
| Collie | Command line argument parsing library | ohad/collie |
| monad-bayes | Probabilistic programming, port from the haskell library of the same name | idris-bayes/monad-bayes |
| missing-numeric | some math data types | seagull-kamome/idris2-missing-numeric |
| time-calendar-clock | port of TimeLib | seagull-kamome/idris2-time-calendar-clock |
| missing-containers | containers | seagull-kamome/idris2-missing-containers |
Network
| Package | Description | Repository |
|---|---|---|
| idris2-tls | TLS implementation in Idris2 | octeep/idris2-tls |
Web
| Package | Description | Repository |
|---|---|---|
| tyttp | A type safe experimental web framework for idris2 targeting node js | kbertalan/tyttp |