idris-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, 11:23:53 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
7 sourcesSome highlights:
Uniqueness types[1], which are inspired by ownership types and borrowed pointers in the Rust language, and should eventually be able to provide compile-time guarantees that critical program fragments will never allocate. If this was achieved, Idris would potentially be usable for tasks that previously necessitated using either C, C++ or Rust.
Partial evaluation[2], which can also be used to improve performance by specialising type classes and higher order functions. Another use is creating speedy interpreters/EDSLs, with the one in [3] being competitive in speed with Java in spite of only being an interpreter.
Uniqueness types can also be used for safe in-place updates of a datastructure. The following map function, for instance, where UList is a UniqueType, will be compiled to code that updates the list in-place, avoidin
Read the rest
g allocating a new list:
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
1. https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Type...
2. https://github.com/idris-lang/Idris-dev/wiki/Static-Argument...
3. http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf
You can sort of do this sometimes. Consider Idris' decidable equality module:
https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
Idris has type classes and it produces a polymorphic total function `decEq` for any type which instantiates the class DecEq.
decEq :: DecEq t => (x : t) -> y -> Dec (x = y)
where Dec denotes a decidable type, something like (but not actually)
data Dec t where
Yes : t -> Dec t
No : Not t -> Dec t
So now we have a proposition in our type-level prolog called `DecEq` and some types, the ones with decidable equality, can instantiate it
instance DecEq () where
decEq _ _ = Yes refl
-- Equality is symmetric, so is the negation of equality
total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
negEqSym p h = p (sym h)
-- Proof that z
Read the rest
ero isn't equal to any number greater than zero
total OnotS : Z = S n -> _|_
OnotS refl impossible
instance DecEq Nat where
decEq Z Z = Yes refl
decEq Z (S _) = No OnotS
decEq (S _) Z = No (negEqSym OnotS)
-- recurse on the arguments together and modify the eventual
-- decided proof so as to match the arguments actually passed.
--
-- I.e. we might find that Yes (n = m) but we need Yes (S n = S m)
--
decEq (S n) (S m) with (decEq n m)
| Yes p = Yes $ cong p
| No p = No $ \h : (S n = S m) => p $ succInjective n m h
Finally, at compile time Idris will try to infer the concrete types instantiating variables throughout the program. If any of the variables are bounded by `DecEq` then it must be able to solve the typeclass prolog to establish decidable equality for that type.
If it fails to fulfill that obligation then it'll fail at compile time.
-- this fails since functions on naturals are
-- far, far, far from decidable... Idris cannot achieve the
-- obligation to find `DecEq (Nat -> Nat)`.
decEq : (x : Nat -> Nat) -> y -> Dec (x = y)
Idris has a type class that is pretty much this: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
Here's an example interaction. There's a difference, though, since + is only for {Num instance,Fin} addition while ++ is {String,List,Vect} concatenation.
https://gist.github.com/reynir/b3d32f07d69366dd2bc3
In Brainfuck beware: JavaScript is after you (2012)Cannot edit for reason, but I thought I would mention, as this is of vital importance to me when i'm learning something new, that both Idris and F* are open source;
https://github.com/nikswamy/FStar (Apache)
https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)
In The Case for Formal Verification (2013)See this page (https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usag...) for info on erasure. Unused proof values or indices in data types used for static checking are erased at compile time via usage analysis (if you don't use it in the RHS of a function definition, it gets erased).
If you want to ensure that the indices of your data type or arguments to your function are erased, you can use the new dot notation. E.g., if you give a function called "half" the following type
half : (n : Nat) -> .(pf : Even n) -> Nat
then the compiler will complain if the proof argument is actually used.
In Try Idris