<div class="github-widget" data-repo="joaomilho/awesome-idris"></div>



## Awesome Idris [![Awesome](https://cdn.rawgit.com/sindresorhus/awesome/d7305f38d29fed78fa85652e3a63e154dd8e8829/media/badge.svg)](https://github.com/sindresorhus/awesome)

[<img src="https://www.idris-lang.org/logo/logo.png" align="right" width="160">](https://www.idris-lang.org/)

&gt; awesome辅助列表 [Idris](https://www.idris-lang.org/) 资源.

 Idris 是一种具有依赖类型的通用纯函数式编程语言. 从属类型允许类型基于值，这意味着可以在类型中精确指定程序行为的某些方面. 它是编译的，带有急切的评价. 它的特性受到 Haskell 和 ML 的影响.



### 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) - 迄今为止出版的最重要的书.
* [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.io/software-foundations/pdf/sf-idris-2018.pdf) -回购是 [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) - 大卫·克里斯蒂安森和埃德温·布雷迪，2016 年.
* [Cross-platform Compilers for Functional Languages](https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf) - 埃德温布雷迪，2015 年.
* [Programming and Reasoning with Side-Effects in Idris](https://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf) - 埃德温布雷迪，2014 年.
* [Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation](https://pdfs.semanticscholar.org/1407/220ca09070233dca256433430d29e5321dc2.pdf) - 埃德温布雷迪，2013 年.
* [Programming and Reasoning with Algebraic Effects and Dependent Types](https://eb.host.cs.st-andrews.ac.uk/drafts/effects.pdf) - 埃德温布雷迪，2013 年.
* [Sequential decision problems, dependently typed solutions](http://eb.host.cs.st-andrews.ac.uk/writings/plmms13.pdf) - Nicola Botta、Cezar Ionescu 和 Edwin Brady，2013 年.
* [Programming in Idris: a tutorial](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf) - 埃德温布雷迪，2012 年.
* [Idris — Systems Programming Meets Full Dependent Types](https://eb.host.cs.st-andrews.ac.uk/writings/plpv11.pdf) - 埃德温布雷迪，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) - 埃德温·布雷迪和凯文·哈蒙德，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) - 埃德温·布雷迪和凯文·哈蒙德，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 和 James McKinna，2009 年.
* [Lightweight Invariants with Full Dependent Types](http://eb.host.cs.st-andrews.ac.uk/drafts/tfp08.pdf) - Edwin Brady、Christoph Herrmann 和 Kevin Hammond，2008 年.

### Presentations

* [Idris: General Purpose Programming with Dependent Types](https://www.youtube.com/watch?v=vkIlW797JN8) - Idris 的创造者 Edwin Brady 的演讲.

### Projects

* [GitHub's trending Idris repos](https://github.com/trending/idris)
* [iridium](https://github.com/puffnfresh/iridium) - xmonad 与 X11 抽象和配置与 Idris.
* [lightyear](https://github.com/ziman/lightyear) - Idris 的解析器组合器.
* [quantities](https://github.com/timjb/quantities) Idris 中类型安全的物理计算和单位转换.
* [idris-type-providers](https://github.com/david-christiansen/idris-type-providers) - Idris 的类型提供程序库.
* [IdrisScript](https://github.com/idris-hackers/IdrisScript) - FFI 绑定与不安全的 JavaScript 世界交互.
* [idris-containers](https://github.com/jfdm/idris-containers) - 用于 Idris 语言的各种数据结构.
* [IdrisSqlite](https://github.com/david-christiansen/IdrisSqlite) - SQLite 的有效绑定.
* [idris-http](https://github.com/uwap/idris-http) - Idris 的 HTTP 库.
* [RingIdris](https://github.com/FranckS/RingIdris) - Idris 的环形求解器.
* [specdris](https://github.com/pheymann/specdris) - Idris 的测试框架.
* [idris-config](https://github.com/jfdm/idris-config) - 用 Idris 编写的各种配置文件的解析器.
* [probability](https://github.com/BlackBrane/probability) - Idris 中的概率计算.
* [idris-protobuf](https://github.com/google/idris-protobuf) - 在 Idris 中部分实现 Protocol Buffers.
* [idris-free](https://github.com/idris-hackers/idris-free) - 免费的 Monads 和有用的结构来使用它们.
* [idris-ct](https://github.com/statebox/idris-ct) - 形式化验证的范畴论库
* [typedefs](https://github.com/typedefs/typedefs) - 与编程语言无关的代数数据类型定义语言

### Backends

* [idris-jvm](https://github.com/mmhelloworld/idris-jvm) - Idris 的 JVM 字节码后端.
* [idris-llvm](https://github.com/idris-hackers/idris-llvm) - LLVM 后端.
* [idris-erlang](https://github.com/lenary/idris-erlang) - Erlang 后端.
* [idris-malfunction](https://github.com/stedolan/idris-malfunction) - 实验性故障（OCaml 内部表示）后端.

### Build tools | Package managers

- [Idris Rules](http://idris.build) - Bazel 的 Idris 规则
- [Ikan](https://github.com/idris-industry/ikan) - idris 的包管理器，在 idris 中
- [Elba](https://github.com/elba/elba) - Idris 的包管理器
- [idream](https://github.com/idream-build/idream) - 一个简单的 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

[![CC0](http://mirrors.creativecommons.org/presskit/buttons/88x31/svg/cc-zero.svg)](https://creativecommons.org/publicdomain/zero/1.0/)
