agda

agda-stdlib

Agda2014–2020

agda / agda-stdlib

agda-stdlib

The Agda standard library

Libraries & SDKs

Explore on GitHub Read Hacker News discussions

5Distinct people

7Mentions

0Explicit recommenders

681GitHub stars

REPOSITORY AT A GLANCE

What to know before exploring

What it is

The Agda standard library

GitHub

Where it is used

No documented product use has been verified yet.

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, 12:54:37 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 year7 dated mentions

Observed mentions: 2014-04-16 22:45:07 UTC to 2020-08-18 22:14:11 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

UTC ranges include their start and exclude their end. Select a period to filter the source evidence.
Period	Start (UTC)	End (exclusive, UTC)	Mentions	Comments
2014	2014-01-01 00:00:00 UTC	2015-01-01 00:00:00 UTC	2	2
2015	2015-01-01 00:00:00 UTC	2016-01-01 00:00:00 UTC	0	0
2016	2016-01-01 00:00:00 UTC	2017-01-01 00:00:00 UTC	1	1
2017	2017-01-01 00:00:00 UTC	2018-01-01 00:00:00 UTC	0	0
2018	2018-01-01 00:00:00 UTC	2019-01-01 00:00:00 UTC	1	1
2019	2019-01-01 00:00:00 UTC	2020-01-01 00:00:00 UTC	1	1
2020	2020-01-01 00:00:00 UTC	2021-01-01 00:00:00 UTC	2	2

What Hacker News says

7 sources

gnulinux·Aug 18, 2020

I program in Agda pretty often and community usually uses Unicode characters for most things, so I do too. The impl of AVL trees in stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Data/Tre... Some basic properties of natural numbers: https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat... It makes the code look absolutely gorgeous, readable and it's very easy to type too. I use Emacs agda-mode so it just automatically replaces e.g. \r with → or \== with ≡ etc... I don't use Agda for theorem proving, I make real life programs in Agda, I compile them to Haskell and compile with GHC to executables.

In APL386 Unicode – An APL Font

gnulinux·Jul 17, 2020

In this case it looks like `T = Maybe T` is isomorphic to a coinductive natural number type, where `suc = just` and `zero = nothing`. You can see an example implementation of it in Agda: https://github.com/agda/agda-stdlib/blob/master/src/Codata/C... As to what is the practical implications of a Conat class? You can use it pretty much anywhere you use natural numbers, except it gives you less guarantees as it can be infinite. To be honest, looking at the code again, I cannot be sure if it's coinductive or inductive. i.e. I'm unsure if you can construct: something : T something = just something which would be an infinite stream of `just`s. If that's not possible, it'd be isomorphic to natural numbers we know.

In Forbidden Haskell Types

danidiaz·Jun 8, 2019

Relatively easy in Vim with digraphs (:h digraph) Ctrl-K l* produces λ Ctrl-K L* produces Λ Unsurprisingly, Emacs also supports this when programming in Agda (\lambda) i'm not sure if it's a builtin feature or part of the Agda plugin. In Agda using Unicode identifiers is widely accepted, even in the standard library: https://github.com/agda/agda-stdlib/blob/master/src/Relation...

In Rust, Macros, λ-calculus/Church numerals, oh my

chriswarbo·Jul 5, 2018

> you could clearly change "x is even" to any "x is wholly divisible by <integer>" The tricky thing is that it's not clear, since it depends entirely upon the formal system you're using! As a simple example, let's say I have the following Java program: if (2 < 3) { return "halt"; } else { while (true) {}; return "never halts"; } This program will halt, but what if we change it? We "could clearly change" the `3` to a `1` and the resulting program would not halt. What if we changed the `3` to `"hello world"`? The result would neither halt nor not-halt, since it wouldn't even be a valid Java program in the first place, due to a type mismatch. Hence it may not at all be clear whether it's valid to swap out parts of a statement or not, let alone whether that will/won't change some property of the statement. That Java example failed du

Read the rest

e to type checking, but static analysis is very similar to type checking/inference, in the sense that it's calculating properties of code (or logical statements; they're equivalent via Curry-Howard) based entirely on the syntax. In this sense, we can think of any static analysis algorithm as being a (potentially very complicated and confusing) type system. It's easy to see from the syntax above that the `2` and `"hello world"` have different types, and hence that this isn't valid code. When we start getting more powerful or complicated type systems, like dependent types, Goedel numbering, or some static analysis algorithm, then it can be arbitrarily difficult to figure out whether a particular arrangement of symbols is actually a valid statement or not. This might seem petty, but consider your `is even` example, written in some dependently typed programming language (i.e. a powerful static analyser). We might say (in Agda, Idris, etc.): halt : String halt = "hello world" f : Int -> String f x = if isEven x then f (x + 1) else halt Most type systems are "conservative", meaning that they treat "dunno" as failure. Since most dependently typed languages aren't smart enough to figure out that this halts, we would have to rewrite the program in a way that provides evidence that it halts. This can get very messy very quickly (e.g. see https://github.com/agda/agda-stdlib/blob/master/src/Relation... ). So the resulting program will be a massive pile of symbols, all carefully orchestrated such that the type checker is happy with the result. In that situation, it is certainly not clear whether we can just replace one expression with another, even if they're the same type (e.g. replacing one integer with another), since that might break some of the surrounding proofs. If we think of a static analyser as a complicated type inference algorithm, which can sometimes infer such proofs and coercions, then we can think of your example as being the 'tip of the iceberg', which the static analyser can "elaborate" into a much more complicated form (this is exactly how Idris works http://docs.idris-lang.org/en/latest/reference/elaborator-re... and "tactics" in Coq are similar https://coq.inria.fr/refman/proof-engine/ltac.html ). It is this explosion of symbols which makes it difficult to talk about formal systems by using informal statements (like your example). It can be very difficult to even figure out how to represent an informal statement in a formal way, but it's only then that we can ask specific questions about algorithms (e.g. what can or can't be deduced). Often, the answers to such questions turn out to be trivial properties of the formalisation; but it may take many decades to actually come up with that formalisation!

In Why I Don't Love Gödel, Escher, Bach

pka·Sep 22, 2016

> What you are doing is claiming types into and out of functions decide if they are functioning correctly. This is not the case at all. When I say proof, I mean it in the mathematical sense. The Curry–Howard isomorphism [0] formalizes the relationship between (mathematical) logic and type theory. Unless you are saying mathematical logic is inconsistent (and thus every mathematical proof is invalid) this is absolutely the case. The same way you can construct a mathematical proof that e.g. n is prime, you can can construct a type Prime n that proves that n is prime [1]. > I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong. This is where your misunderstanding stems from. Continuing with the example from above, if you have a function: makePrime :: n -> Prime n the fun

Read the rest

ction can not construct (Prime n) if n is not a prime. > If I call `get_lottery_number` by your logic it will always provide me with the real winning lottery number since the types check out. That is absolutely incorrect. Types can't prove functionality. If you give me a specification that constructs predicted lottery numbers I could absolutely turn it into a type :) > They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case But you don't have proof that you are handling every case :) > You can't say a program will have no bugs because the types check out. Is that what you are saying? Yes, if the types correspond to the specification then there are no bugs. The specification can still have bugs though, but that's unavoidable. The thing is that you've proven the program does what you told it to do. Once you stop thinking about types in the Java sense and start thinking about them as logical propositions it will all make sense. I provided you with a couple of links in the other comments and here if you are still interested. [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...

In Hacker-Proof Code Confirmed

tel·Jul 2, 2014

It'd be more like decideValidity : (p : A -> Type) -> (a : A) -> Either (p a) (Not (p a)) and for some classes of propositions this is a really useful type, e.g. the notion of decidable equality[0]. For general propositions you're talking about unbounded proof search, however. Undecidable propositions will fail to terminate (thus causing problems in a total language). Decidable propositions may still be exponentially slow to decide. Some classes of propositions may be known to be decidable, but knowing generally whether or not a proposition is undecidable is undecidable (Halting). [0] https://github.com/agda/agda-stdlib/blob/master/src/Relation...

In Dependently Typed Programming

tel·Apr 16, 2014

I find Idris has a more computational flair while Agda is often "done after typechecking". Idris doesn't enforce termination as strictly as Agda. Idris' interactive modes are less friendly and powerful—Agda's emacs mode is best in breed. Idris has typeclasses and Agda something akin to first-class modules (as stated above). That's a fairly big difference. Idris handles laziness and strictness (or, relatedly, data/codata) a little differently than Agda, but it's not a huge concern until you get technical. Idris is also just younger than Agda and subsequently works a little wonkily. Again I find this exposed through the interactive mode which sometimes provides rather strange information. Although honestly that happens in both Agda and Idris. Idris has nice syntax for embedded DSLs which is demonstrated in its Effects library which would be

Read the rest

possible to replicate in Agda but not as nice looking. One big difference is that Agda uses universe polymorphism and Idris uses cumulative universes. This shows up in a lot of parameterization of Set in Agda. If you find Idris easy to understand than Agda will be absolutely no harder. Go take a look at the Agda standard library to get a taste: https://github.com/agda/agda-stdlib Something like Relation.Binary.Core is a good place to start: https://github.com/agda/agda-stdlib/blob/master/src/Relation...

In Agda by Example: Sorting