psqueues VS Agda

Compare psqueues vs Agda and see what are their differences.


Priority Search Queues in three different flavors for Haskell (by jaspervdj)


Agda is a dependently typed programming language / interactive theorem prover. (by agda)
Our great sponsors
  • SonarLint - Deliver Cleaner and Safer Code - Right in Your IDE of Choice!
  • Scout APM - Less time debugging, more time building
  • OPS - Build and Run Open Source Unikernels
psqueues Agda
1 5
60 1,719
- 2.9%
3.0 9.6
2 months ago about 20 hours ago
Haskell Haskell
BSD 3-clause "New" or "Revised" License LicenseRef-OtherLicense
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.


Posts with mentions or reviews of psqueues. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-12-14.
  • -🎄- 2021 Day 15 Solutions -🎄-
    127 projects | | 14 Dec 2021
    A super-ugly Dijkstra implementation with psqueues for priority queues. Before I took them into use the first part took ~10 sec, after that it's ~60ms, and 2.5s for the second part. I believe, there's still room for optimization, but it's enough for today.


Posts with mentions or reviews of Agda. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-10-18.
  • Integer overflow causes Russel's paradox
    1 project | | 22 Dec 2021
  • What input method would you prefer for Unicode characters in a neovim plugin?
    7 projects | | 18 Oct 2021
    My best guess is that it has not really been maintained lately, there were only 12 commits in the last 7 years, some of which are just global modifications, which include this file as well:
  • Type in type and HoTT exercises
    1 project | | 28 Aug 2021
    Also I would suggest is that you import a paradox (e.g., and see what it actually does when you construct values with it that you evaluate or proofs that you use.
  • Trouble with Proving Termination without K
    2 projects | | 20 Jan 2021
    Andrea had some code relaxing these restrictions at the last AIM (cf. "trying to make termination checker accept more definitions --without-K, fixing #4527" in the wrap-up section) but I don't know if it has been merged into master yet.
  • Road to 1.0/ Zig
    2 projects | | 22 Dec 2020
    Significant nit: this isn't true. The whole domain of "high-assurance software" is about this, with examples such as CompCert and seL4. There are tools like Frama-C that support you in proving things about your C; [proof assistants]() that let you extract Haskell, OCaml, or Scheme from proofs so the code is correct by construction; and languages like CakeML, F*, Agda, Idris, ATS... that are both programming languages and proof assistants.

What are some alternatives?

When comparing psqueues and Agda you can also consider the following projects:

lean - Lean Theorem Prover

zig - General-purpose programming language and toolchain for maintaining robust, optimal, and reusable software.

HoleyMonoid - Automatically exported from

miso - :ramen: A tasty Haskell front-end framework

agda-vim - Agda interaction in vim

open-typerep - Open type representations and dynamic types

permutation - git import of patrick perry permutations lib from darcs

map-syntax - Syntax sugar and explicit semantics for statically defined maps

containers - Assorted concrete container types

parameterized-utils - A set of utilities for using indexed types including containers, equality, and comparison.

distributive - Dual Traversable