[[
wikihub
]]
Search
⌘K
Explore
People
For Agents
Sign in
Explore
People
For Agents
Sign in
@harrisonqian / Awesome / wiki/programming-languages/idris.md
Suggest edit
Cancel
Submit suggestion
Title
Name
Note
--- visibility: public --- # Idris **repo:** [joaomilho/awesome-idris](https://github.com/joaomilho/awesome-idris) **category:** [[programming-languages|Programming Languages]] **related:** [[haskell|Haskell]] --- # Awesome Idris [](https://github.com/sindresorhus/awesome) [<img src="https://www.idris-lang.org/logo/logo.png" align="right" width="160">](https://www.idris-lang.org/) > An auxiliary list of awesome [Idris](https://www.idris-lang.org/) resources. Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML. ## Contents - [Official resources](#official-resources) - [Articles](#articles) - [Books](#books) - [Papers](#papers) - [Presentations](#presentations) - [Projects](#projects) ### Official resources * [Official website](https://www.idris-lang.org/) * [Official repo](https://github.com/idris-lang/Idris-dev) ### Articles * [10 things Idris improved over Haskell](https://deque.blog/2017/06/14/10-things-idris-improved-over-haskell/) * [Meet Idris, a language that will change the way you think about programming](https://crufter.com/idris-a-language-that-will-change-the-way-you-think-about-programming) * [Tests vs. Types](http://kevinmahoney.co.uk/articles/tests-vs-types/) ### Books * [Type Driven Development With Idris](https://www.manning.com/books/type-driven-development-with-idris) - Most important book published so far. * [Type Theory and Functional Programming](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/) * [Programming in Martin-Löf's Type Theory](http://www.cse.chalmers.se/research/group/logic/book/book.pdf) * [Software Foundations](https://idris-hackers.[github](/@harrisonqian/awesome/wiki/development-environment/github).io/software-foundations/pdf/sf-idris-2018.pdf) - Repo is [here](https://github.com/idris-hackers/software-foundations). * [Gentle Introduction to Dependent Types with Idris](https://leanpub.com/gidti) ### Papers * [Elaborator Reflection: Extending Idris in Idris](https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf) - David Christiansen and Edwin Brady, 2016. * [Cross-platform Compilers for Functional Languages](https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf) - Edwin Brady, 2015. * [Programming and Reasoning with Side-Effects in Idris](https://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf) - Edwin Brady, 2014. * [Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation](https://pdfs.semanticscholar.org/1407/220ca09070233dca256433430d29e5321dc2.pdf) - Edwin Brady, 2013. * [Programming and Reasoning with Algebraic Effects and Dependent Types](https://eb.host.cs.st-andrews.ac.uk/drafts/effects.pdf) - Edwin Brady, 2013. * [Sequential decision problems, dependently typed solutions](http://eb.host.cs.st-andrews.ac.uk/writings/plmms13.pdf) - Nicola Botta, Cezar Ionescu and Edwin Brady, 2013. * [Programming in Idris: a tutorial](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf) - Edwin Brady, 2012. * [Idris — Systems Programming Meets Full Dependent Types](https://eb.host.cs.st-andrews.ac.uk/writings/plpv11.pdf) - Edwin Brady, 2011. * [Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation](http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf) - Edwin Brady and Kevin Hammond, 2010. * [Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols](http://eb.host.cs.st-andrews.ac.uk/writings/fi-cbc.pdf) - Edwin Brady and Kevin Hammond, 2010. * [Domain Specific Languages (DSLs) for Network Protocols](http://eb.host.cs.st-andrews.ac.uk/drafts/ngna2009-dsl.pdf) - Saleem Bhatti, Edwin Brady, Kevin Hammond and James McKinna, 2009. * [Lightweight Invariants with Full Dependent Types](http://eb.host.cs.st-andrews.ac.uk/drafts/tfp08.pdf) - Edwin Brady, Christoph Herrmann and Kevin Hammond, 2008. ### Presentations * [Idris: General Purpose Programming with Dependent Types](https://www.youtube.com/watch?v=vkIlW797JN8) - Presentation by Edwin Brady, Idris' creator. ### Projects * [GitHub's trending Idris repos](https://github.com/trending/idris) * [iridium](https://github.com/puffnfresh/iridium) - xmonad with the X11 abstracted and configured with Idris. * [lightyear](https://github.com/ziman/lightyear) - Parser combinators for Idris. * [quantities](https://github.com/timjb/quantities) Type-safe physical computations and unit conversions in Idris. * [idris-type-providers](https://github.com/david-christiansen/idris-type-providers) - Type provider library for Idris. * [IdrisScript](https://github.com/idris-hackers/IdrisScript) - FFI Bindings to interact with the unsafe world of [JavaScript](/@harrisonqian/awesome/wiki/programming-languages/javascript). * [idris-containers](https://github.com/jfdm/idris-containers) - Various data structures for use in the Idris Language. * [IdrisSqlite](https://github.com/david-christiansen/IdrisSqlite) - Effectful bindings for SQLite. * [idris-http](https://github.com/uwap/idris-http) - HTTP library for Idris. * [RingIdris](https://github.com/FranckS/RingIdris) - Ring solver for Idris. * [specdris](https://github.com/pheymann/specdris) - Test framework for Idris. * [idris-config](https://github.com/jfdm/idris-config) - Parsers for various configuration files written in Idris. * [probability](https://github.com/BlackBrane/probability) - Probabilistic computation in Idris. * [idris-protobuf](https://github.com/google/idris-protobuf) - Partial implementation of Protocol Buffers in Idris. * [idris-free](https://github.com/idris-hackers/idris-free) - Free Monads and useful constructions to work with them. * [idris-ct](https://github.com/statebox/idris-ct) - Formally verified category theory library * [typedefs](https://github.com/typedefs/typedefs) - Programming language-agnostic, algebraic data type definition language ### Backends * [idris-jvm](https://github.com/mmhelloworld/idris-jvm) - JVM bytecode backend for Idris. * [idris-llvm](https://github.com/idris-hackers/idris-llvm) - LLVM backend. * [idris-erlang](https://github.com/lenary/idris-erlang) - [Erlang](/@harrisonqian/awesome/wiki/programming-languages/erlang) backend. * [idris-malfunction](https://github.com/stedolan/idris-malfunction) - Experimental Malfunction (OCaml internal representation) backend. ### Build tools | Package managers - [Idris Rules](http://idris.build) - Idris rules for Bazel - [Ikan](https://github.com/idris-industry/ikan) - A package manager for idris, in idris - [Elba](https://github.com/elba/elba) - A package manager for Idris - [idream](https://github.com/idream-build/idream) - A simple build system for Idris ### Community * [Mailing list](http://groups.google.com/group/idris-lang) * IRC: #idris on [freenode.net](https://webchat.freenode.net/) * [GitHub organization](https://github.com/idris-hackers) * [Community Standards](https://www.idris-lang.org/documentation/community-standards/) ## License [](https://creativecommons.org/publicdomain/zero/1.0/)