Facebook uses Haskell for [Haxl](https://github.com/facebook/Haxl), Standard Chartered has a their
own Haskell [compiler](https://www.reddit.com/r/haskell/comments/6im268/standard_ch...)
and a massive code base in Haskell. [Agda](https://github.com/agda/agda) and [Idris](https://github.com/idris-lang/Idris-dev)
were mostly written in Haskell as well.
In What killed Haskell, could kill Rust, tooidris-lang
Idris-dev
Haskell2014–2020
idris-lang / Idris-dev · Archived
Idris-dev
A Dependently Typed Functional Programming Language
21Distinct people
21Mentions
0Explicit recommenders
3.5KGitHub stars
What to know before exploring
What it is
A Dependently Typed Functional Programming Language
GitHub
Where it is used
No documented product use was verified in the last source check.
What people are saying
No recommendation phrase was found in the indexed comments.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 3:03:16 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year21 dated mentions
Observed mentions: 2014-04-13 21:05:19 UTC to 2020-09-12 11:50:45 UTC.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2014 | 2014-01-01 00:00:00 UTC | 2015-01-01 00:00:00 UTC | 7 | 2 | 5 |
| 2015 | 2015-01-01 00:00:00 UTC | 2016-01-01 00:00:00 UTC | 3 | 0 | 3 |
| 2016 | 2016-01-01 00:00:00 UTC | 2017-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2017 | 2017-01-01 00:00:00 UTC | 2018-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2018 | 2018-01-01 00:00:00 UTC | 2019-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2019 | 2019-01-01 00:00:00 UTC | 2020-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 5 | 0 | 5 |
From the project README
An excerpt from the repository, fetched Nov 13, 2026.
Read the project’s introduction
Idris 1
Idris (https://idris-lang.org/) is a general-purpose functional programming
language with dependent types.
Installation
This repository represents the latest development version of the
language, and may contain bugs that are being actively worked on. For
those who wish to use a more stable version of Idris please consider
installing the latest version that has been released on Hackage.
Installation instructions for various platforms can be
found on the Idris Wiki.
More information about building Idris from source has been detailed in the Installation Guide
Code Generation
Idris has support for external code generators. Supplied with the distribution
is a C code generator to compile executables, and a JavaScript code generator
with support for node.js and browser JavaScript.
More information about code generators can be found
here.
Status
This is Idris 1, implemented in Haskell. Idris 1 is not actively
worked on anymore.
Idris 2 is the next generation
of Idris, and where primary development happens.
More Information
If you would like to find out more information, or ask questions, we
currently have a Wiki;
a mailing list,
and an IRC channel #idris on libera. To join the IRC channel,
point your irc client to irc.libera.chat then /join #idris.
For those further interested in using Idris for projects, the
Idris Hackers GitHub organisation is
where some interesting projects are being hosted.
For those interested in contributing to Idris directly we kindly ask that
prospective developers please consult the Contributing Guide first.
Read the full README on GitHubWhat Hacker News says
21 sources> The book expected them to do a proof by cases, with some sort of case split on the order of a , b , and c . What they turned in was mostly pretty good, actually, but while grading it I became disgusted with the whole thing and thought there has to be a better way.
This is how it's done in the Idris standard library[1]:
total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
minimumAssociative Z c r = Refl
minimumAssociative (S k) Z r = Refl
minimumAssociative (S k) (S j) Z = Refl
minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl
[1] Or prelude, or whatever it's called. https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
In What would Dijkstra do? Proving the associativity of minIt's because `Integer` is an insufficiently specific type to ensure that the value expression is well formed. If you really wanted to, you could prove that `add` is well-formed in Haskell and Haskell-likes: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
In Implement with types, not your brain (2019)Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statements) and their terms (the expressions of that type) are proofs. It's a straightforward syntactic correspondence:
- A -> B (Function type) and A => B (Logical implication)
- A * B (Product/Tuple type) and A /\ B (Logical conjunction)
- A + B (Sum/Tagged union type) and A \/ B (Logical disjunction)
Proving that A implies B is the same thing as writing a function that takes a proof of A and returns a proof of B. Proving the logical conjunction of A and B is the same thing as pairing together a proof of A and a proof of B.
So writing a definition that has a certain type is the same thing as proving a theorem.
Dependent types [1], which Coq, Agda, and Idris have, further the Curry-Howard
Read the rest
correspondence. With dependent types, you can mention programs inside types and therefore express theorems about programs. You have:
- The dependent function type (x : A) -> B(x), where the return type B(x) is a function of the input x.
This is the same thing as universal quantification, "for all x of type A, B(x) holds."
- The dependent tuple type (x : A) B(x), where the type of the second element is a function of the first element x.
This is the same thing as existential quantification, "there exists an x of type A where B(x) holds."
So with dependent types, you can write mathematical proofs about programs. For example, you can show that a binary operation is commutative. Another good example is the "vector" type [2], which is like the functional-style linked list type, but parameterized over a length. Thus, you can prove that an index out-of-bounds error cannot happen. If you want to learn more about the theory, keywords to search up are "constructive math/proof," "intuitionalistic logic," and "Martin-Lof/intuitionalistic type theory."
[0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
[1] https://en.wikipedia.org/wiki/Dependent_type
[2] https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...
case health <= 0 of
False => pure ()
True => Output $ Death target
This ought to just be:
when (health <= 0) Output $ Death target
It takes years to learn all the general-purpose helper functions in these languages (I'm still discovering new ones after 10 years of Scala), but they can help make code so much clearer. And since they're just plain functions rather than keywords or anything, a reader who doesn't know can just jump through to the definition, which is a one-liner: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
In A game in a pure language (part 1): introduction and problems with Idrishttps://github.com/idris-lang/Idris-dev/blob/5965fb16210b184...
Idris is not a Lisp and I've never used it, but it has dependent types (types incorporating values) and encodes matrix dimensions into the type system (I think only matrix multiplications which can be proven to have matching dimensions can compile). I think the dimension parameters are erased, and generic at runtime (whereas C++ template int parameters are hard-coded at compile time). IDK if it uses dependent types for optimization.
In Show HN: BelIdris isn't imperative (Haskell-like with dependent types), but offers features like those:
http://docs.idris-lang.org/en/latest/effects/depeff.html
readInt : Eff Bool [STATE (Vect n Int), STDIO]
[STATE (Vect (S n) Int), STDIO]
http://docs.idris-lang.org/en/latest/st/machines.html
logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
They're both implemented within Idris, as libraries/modules, rather than being compiler magic:
- https://github.com/idris-lang/Idris-dev/blob/master/libs/con...
- https://github.com/idris-lang/Idris-dev/blob/master/libs/eff...
I think it'd be possible to write similar effect systems in other dependently typed languages like ATS, which is a relatively imperative language (C+ML-like).
In Why GitHub used Haskell for SemanticSo don't write quicksort in Idris. It's not going to work very well anyways. It's not at all well-suited, and isn't really even an especially important sorting algorithm in a world where linear time sorting and constant time indexed searches are a thing.
But most of the work you'd be doing to write quicksort is writing the machinery for structurally recursive sorting, which a lot of tutorials write not because you have to, but because it's a very good exercise for learning how to write total functions that are recursive in a way DT systems can prove totality on.
Most of these tools are in the contrib library (and the book mentions this). For example the preorder interface you need:
https://github.com/idris-lang/Idris-dev/blob/master/libs/con...
In The Little TyperIdris points the way to the future of programming.
A few examples that I find very intriguing:
1. type safe printf: https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr
2. compile-time evidence that a runtime check will be performed: https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...
3. Most of all, compile-time checking of state machine properties http://docs.idris-lang.org/en/latest/st/introduction.html
Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the program can only get into a "LoggedIn" state by going through the authentication protocol.
In Things that Idris improves things over HaskellI'm under the impression that SPJ made that comment thinking of adoption (for a future "regrettably popular" Haskell), since the difficulty of reasoning about laziness does put people off. I might be wrong though: maybe he was arguing that laziness doesn't warrant the user and compiler-author cost it brings. I don't remember where I picked this up from.
Idris is strict too, but optional laziness is built into the compiler with the use of a special-cased Lazy wrapper of the form
data Lazy a = Delay a
This is kind of the opposite of strictness annotations (bang-patterns) from Haskell, except one doesn't need to pattern-match on Delay or use it to wrap arguments to functions expecting Lazy values. The Idris compiler can do something like "laziness analysis" (admittedly trivial in comparison to GHC's strictness analyser) to introduce and e
Read the rest
liminate Delay constructors automatically. The laziness information is carried around in the types:
force : Lazy a -> a
force a = a
https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ#...
(purescript-lazy is also a thing, but I think it's not as seamless because of the "no compiler magic" position.)
In any case, what about -XStrict? I've never used it (or -XStrictData either), but isn't it a solution to the laziness problem, albeit a nuke-ish one at that?
And while we're thinking ahead, let's talk about the project to get linear types (something similar to Rust lifetimes, but weaker) into GHC :)
https://ghc.haskell.org/trac/ghc/wiki/LinearTypes
In fact, it checks every predicate codified by the type system. The question is how powerful your type system is, because this determines what predicates you can (conveniently) test.
Well-designed strongly typed languages naturally check some useful predicates (existence, the exact structure of the value, etc.). These alone are sufficient to eliminate null pointers, non-total functions, and most other failure modes that plague languages like C++ or Python.
Stepping it up a notch, you can use things like GADTs and kind promotion to check much more advanced predicates (like that a vector must be non-empty or even length).
With refinement types a la liquid Haskell, I can statically guarantee that e.g. my function only returns lists of even length or only returns even numbers, without even having to put this information in the type of the ret
Read the rest
urned value.
With full-blown dependent types a la Coq/Idris/Agda, you can encode pretty much whatever property you want into types. For example, Idris has `verifiedMonoid` which statically guarantees that an operation is associative and has an identity. See https://github.com/idris-lang/Idris-dev/blob/master/libs/con...
This is the chief drawback of these two libraries: they are poorly documented (and are arguably not documented at all). In general, parsers is for parsing and trifecta is for reporting errors and diagnostics. Trifecta looks especially nice for giving context to error sites, but I haven't used it much yet (only for highlighting, really).
By "error recovery," do you mean backtracking? If so, there are several ways of doing that, which can be found here:
https://hackage.haskell.org/package/parsers-0.12.2.1/docs/Te...
See the 'choice', 'option', and 'try' combinators, and also the '<|>' operator in Control.Applicative.
If you need more than that, you can extend parsers' monadic parsing to roll your own error recovery.
Currently, the best way to understand how parsers and trifecta work is to look at projects that use them. I will give you some
Read the rest
links to the ones I've used and found helpful, if a bit more complicated than the parsers I am currently writing:
https://github.com/ekmett/ermine/tree/master/src/Ermine
https://github.com/idris-lang/Idris-dev/tree/master/src/Idri...
And here is a relevant Reddit thread, which includes a link to Edward Kmett's slide deck which motivates trifecta/parsers and gives a high-level view of how they work:
https://www.reddit.com/r/haskell/comments/2uc6kp/are_there_a...
I hope this helps!
My Idris installation instructions: https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Window...
It's an example of pulling down build tools and libs (well, a lib) with msys2.
In State of the Haskell ecosystemOwnership is doable in a dynamic language, provided you are willing to tolerate aborts: C++'s std::unique_ptr is enforced at runtime. Similarly, you can emulate dynamic borrowing using something like Rust's RefCell, which aborts when you attempt to mutably borrow a value twice (though it can be quite difficult to reason about from a usability perspective).
But if you're building on top of F# you have a static type system at your disposal. Usually, languages that incorporate linear types and first-class garbage collection treat linear types as a separate kind, and allow them to interact with standard types only in limited ways. See, for example, https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Type.... I believe http://protz.github.io/mezzo/ is also exploring this design space.
In Fearless concurrency with RustShowing the 15 most recent of 21 sources. Enable JavaScript to search and browse every indexed mention.