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