Packages tagged dependent-types
62 packages have this tag.
[Merge tag] (trustees only)Related tags: library (53), bsd3 (40), data (22), program (20), gpl (7), mit (7), deprecated (6), singletons (5), data-structures (3), development (2), language (2), lens (2), math (2), optics (2), public-domain (2), ai (1), compilers-interpreters (1), configuration (1), ...
Name |
DLs |
Rating |
Rev Deps |
Description |
Tags |
Last U/L |
Last Version |
Maintainers |
|---|---|---|---|---|---|---|---|---|
| Agda | 92 | 2.75 | 8 | A dependently typed functional programming language and proof assistant | (dependent-types, library, mit, program) | 2025-07-05 | 2.8.0 | AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell |
| Agda-executable (deprecated in favor of Agda) | 12 | 0.0 | 1 | Command-line program for type-checking and compiling Agda programs | (dependent-types, deprecated, program) | 2012-03-12 | 2.3.0.1 | NilsAndersDanielsson, UlfNorell |
| MiniAgda | 38 | 2.0 | 1 | A toy dependently typed programming language with type-based termination. | (dependent-types, library, mit, program) | 2025-07-23 | 0.2025.7.23 | AndreasAbel |
| PandocAgda (deprecated) | 5 | 0.0 | 1 | Pandoc support for literate Agda | (bsd3, dependent-types, deprecated, library, program) | 2013-03-11 | 2.3.3.0.2 | PeterDivianszky |
| Sit | 14 | 0.0 | 1 | Prototypical type checker for Type Theory with Sized Natural Numbers | (dependent-types, library, program) | 2023-08-03 | 0.2023.8.3 | AndreasAbel |
| aeson-dependent-sum | 3 | 0.0 | 0 | JSON encoding/decoding for dependent-sum | (data, dependent-types, gpl, json, library) | 2022-08-27 | 0.1.0.1 | jack |
| agda-server (deprecated) | 4 | 0.0 | 1 | Http server for Agda (prototype) | (bsd3, dependent-types, deprecated, program) | 2013-10-03 | 0.1.1 | PeterDivianszky |
| agda-snippets (deprecated in favor of Agda) | 6 | 0.0 | 1 | Render just the Agda snippets of a literate Agda file to HTML | (bsd3, dependent-types, deprecated, library, program) | 2017-06-04 | 2.5.2 | LiamOConnorDavis |
| agda-snippets-hakyll (deprecated in favor of Agda) | 13 | 0.0 | 1 | Literate Agda support using agda-snippets, for Hakyll pages. | (bsd3, dependent-types, deprecated, library) | 2017-06-04 | 0.1.2.2 | LiamOConnorDavis |
| agda-unused | 5 | 0.0 | 0 | Check for unused code in an Agda project. | (dependent-types, library, mit, program) | 2022-11-26 | 0.3.0 | msuperdock |
| agda2lagda | 24 | 0.0 | 0 | Translate .agda files into .lagda.tex files. | (dependent-types, development, program) | 2025-09-05 | 0.2025.9.5 | AndreasAbel |
| bin | 15 | 0.0 | 5 | Bin: binary natural numbers. | (data, dependent-types, gpl, library, math, singletons) | 2024-06-08 | 0.1.4 | phadej |
| compare-type | 4 | 0.0 | 1 | compare types of any kinds in haskell | (bsd3, dependent-types, library) | 2015-01-10 | 0.1.1 | Kinokkory |
| constrained-some | 6 | 0.0 | 2 | Existential type that can be constrained | (data, dependent-types, library, mit) | 2024-11-29 | 0.1.2 | bruderj15 |
| cubical | 6 | 0.0 | 1 | Implementation of Univalence in Cubical Sets | (dependent-types, mit, program) | 2014-04-27 | 0.2.0 | AndersMortberg |
| dec | 14 | 0.0 | 4 | Decidable propositions. | (bsd3, data, dependent-types, library) | 2024-05-17 | 0.0.6 | phadej |
| decidable | 19 | 0.0 | 2 | Combinators for manipulating dependently-typed predicates. | (bsd3, dependent-types, library) | 2024-02-28 | 0.3.1.1 | jle |
| dependent-enummap | 3 | 0.0 | 1 | A generalisation of EnumMap to dependent types | (bsd3, data, dependent-types, library) | 2025-05-13 | 0.1.0.0 | tomsmeding |
| dependent-map | 29 | 2.5 | 40 | Dependent finite maps (partial dependent products) | (bsd3, data, dependent-types, library) | 2025-10-19 | 0.4.0.1 | BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch, alexfmpe, maralorn, ymeister |
| dependent-sum | 64 | 2.25 | 65 | Dependent sum type | (data, dependent-types, library, public-domain) | 2022-12-22 | 0.7.2.0 | BertramFelgenhauer, JamesCook, JohnEricson, RyanTrinkle, abrar, 3noch, alexfmpe, maralorn, DanBornside, ymeister |
| eliminators | 45 | 0.0 | 1 | Dependently typed elimination functions using singletons | (bsd3, dependent-types, library) | 2026-01-11 | 0.9.7 | ryanglscott |
| fin | 28 | 2.0 | 16 | Nat and Fin: peano naturals and finite numbers | (bsd3, data, dependent-types, library, math, singletons) | 2024-11-09 | 0.3.2 | phadej |
| helf | 7 | 0.0 | 1 | Typechecking terms of the Edinburgh Logical Framework (LF). | (dependent-types, mit, program) | 2024-03-18 | 1.0.20240318 | AndreasAbel |
| hoq | 3 | 0.0 | 1 | A language based on homotopy type theory with an interval type | (dependent-types, gpl, program) | 2014-09-27 | 0.3 | valis |
| idris | 130 | 2.25 | 1 | Functional Programming Language with Dependent Types | (bsd3, compilers-interpreters, dependent-types, library, program) | 2021-10-22 | 1.3.4 | EdwinBrady, niklasl |
| instance-map | 2 | 0.0 | 1 | Template haskell utilities for helping with deserialization etc. of existential types | (bsd3, dependent-types, library) | 2018-07-23 | 0.1.0.0 | rwarfield |
| ivor (deprecated in favor of idris) | 13 | 0.0 | 2 | Theorem proving library based on dependent type theory | (bsd3, dependent-types, deprecated, library, theorem-provers) | 2011-06-16 | 0.1.14.1 | EdwinBrady, GwernBranwen |
| known-lists | 2 | 0.0 | 0 | Easy type-level lists with term-level membership proofs. | (bsd3, data-structures, dependent-types, library, type-system) | 2026-01-30 | 0.1.0.0 | ShapeOfMatter |
| lens-typelevel | 3 | 0.0 | 1 | Type-level lenses using singletons | (bsd3, dependent-types, lenses, library) | 2018-10-29 | 0.1.1.0 | jle |
| list-witnesses | 17 | 0.0 | 0 | Witnesses for working with type-level lists | (bsd3, dependent-types, library) | 2024-02-28 | 0.1.4.1 | jle |
| nanoAgda | 6 | 0.0 | 1 | A toy dependently-typed language | (dependent-types, program) | 2012-03-20 | 1.0.0 | JeanPhilippeBernardy |
| open-typerep | 9 | 0.0 | 2 | Open type representations and dynamic types | (bsd3, dependent-types, library) | 2016-05-27 | 0.6.1 | EmilAxelsson |
| parameterized-utils | 28 | 2.0 | 16 | Classes and data structures for working with data-kind indexed types | (bsd3, data-structures, dependent-types, library) | 2026-01-22 | 2.2.0.0 | KevinQuick, RobertDockins, ryanglscott, galoisinc, mccleeary, sauclovian_g, aschwerdfeger_galois |
| path-sing | 4 | 0.0 | 0 | A singleton wrapper for the `path` library. | (dependent-types, filesystem, library, mpl, system) | 2023-09-18 | 0.1.0.0 | YamadaRyo |
| pisigma | 7 | 0.0 | 1 | A dependently typed core language | (bsd3, dependent-types, development, language, library, program) | 2011-05-18 | 0.2.1 | AndresLoeh, DarinMorrison |
| poly-rec | 9 | 0.0 | 1 | Polykinded extensible records | (data, dependent-types, gpl, library) | 2024-11-08 | 0.7.0.4 | jpgarcia |
| prim-uniq | 5 | 0.0 | 4 | Opaque unique identifiers in primitive state monads | (data, dependent-types, library, public-domain) | 2020-04-15 | 0.2 | BertramFelgenhauer, JamesCook, RyanTrinkle |
| proof-assistant-bot | 6 | 0.0 | 0 | Telegram bot for proof assistants | (dependent-types, library, mit, program) | 2024-02-07 | 0.2.2 | swamp_agr |
| ral | 7 | 0.0 | 4 | Random access lists | (data, dependent-types, gpl, library, singletons) | 2024-06-08 | 0.2.2 | phadej |
| ral-lens | 13 | 0.0 | 0 | Length-indexed random access lists: lens utilities. | (data, dependent-types, gpl, lens, library, singletons) | 2024-06-08 | 0.2.1 | phadej |
| ral-optics | 9 | 0.0 | 0 | Length-indexed random access lists: optics utilities. | (data, dependent-types, gpl, library, optics, singletons) | 2024-06-08 | 0.2.1 | phadej |
| reflection | 180 | 2.25 | 98 | Reifies arbitrary terms into types that can be reflected back into terms | (bsd3, data, dependent-types, library, reflection) | 2024-12-04 | 2.1.9 | EdwardKmett, ryanglscott |
| rzk | 73 | 2.0 | 1 | An experimental proof assistant for synthetic ∞-categories | (bsd3, dependent-types, library, program) | 2025-11-05 | 0.7.7 | NickolayKudasov |
| show-type | 6 | 0.0 | 4 | convert types into string values in haskell | (bsd3, dependent-types, library) | 2015-01-08 | 0.1.1 | Kinokkory |
| singleton-bool | 52 | 0.0 | 7 | Type level booleans | (bsd3, dependent-types, library) | 2024-06-04 | 0.1.8 | phadej |
| singleton-dict | 2 | 0.0 | 1 | Typelevel balanced search trees via a singletonized Data.Map | (bsd3, data, dependent-types, library) | 2017-06-09 | 0.1.0.0 | ArieMiddelkoop |
| singleton-nats | 26 | 0.0 | 2 | Unary natural numbers relying on the singletons infrastructure. | (bsd3, data, dependent-types, library) | 2023-10-13 | 0.4.7 | AndrasKovacs, ryanglscott |
| singletons | 125 | 2.75 | 124 | Basic singleton types and definitions | (bsd3, dependent-types, library) | 2024-12-11 | 3.0.4 | RichardEisenberg, ryanglscott |
| singletons-base | 9 | 0.0 | 28 | A promoted and singled version of the base library | (bsd3, dependent-types, library) | 2026-01-11 | 3.5.1 | ryanglscott |
| singletons-base-code-generator | 2 | 0.0 | 0 | Code generator for the singletons-base test suite | (bsd3, dependent-types, program) | 2024-12-30 | 0.1 | ryanglscott |
| singletons-th | 20 | 0.0 | 10 | A framework for generating singleton types | (bsd3, dependent-types, library) | 2026-01-11 | 3.5.1 | ryanglscott |
| some | 51 | 0.0 | 37 | Existential type: Some | (bsd3, data, dependent-types, library) | 2023-10-24 | 1.0.6 | phadej |
| symbols | 15 | 0.0 | 3 | Symbol manipulation | (bsd3, dependent-types, library) | 2019-09-10 | 0.3.0.0 | kcsongor |
| tensor-safe | 4 | 2.0 | 0 | Create valid deep neural network architectures | (ai, bsd3, dependent-types, language, library, program) | 2019-05-03 | 0.1.0.1 | leopiney |
| type-equality | 10 | 0.0 | 14 | Data.Type.Equality compat package | (bsd3, data, dependent-types, library) | 2024-05-12 | 1.0.1 | ErikHesselink, phadej, ryanglscott |
| type-fun | 9 | 0.0 | 5 | Collection of widely reimplemented type families | (bsd3, dependent-types, library) | 2021-06-04 | 0.1.3 | AlekseyUymanov |
| type-level-bst | 2 | 0.0 | 1 | type-level binary search trees in haskell | (bsd3, data-structures, dependent-types, library) | 2014-10-28 | 0.1 | Kinokkory |
| typeparams | 4 | 0.0 | 1 | Lens-like interface for type level parameters; allows unboxed unboxed vectors and supercompilation | (bsd3, configuration, data, dependent-types, library, optimization) | 2015-01-26 | 0.0.6 | MikeIzbicki |
| uAgda | 11 | 0.0 | 1 | A simplistic dependently-typed language with parametricity. | (dependent-types, program) | 2012-03-10 | 1.2.0.4 | JeanPhilippeBernardy |
| vec | 38 | 0.0 | 7 | Vec: length-indexed (sized) list | (bsd3, data, dependent-types, library) | 2024-06-08 | 0.5.1 | phadej |
| vec-lens | 5 | 0.0 | 0 | Vec: length-indexed (sized) list: lens support | (bsd3, data, dependent-types, lens, library) | 2024-06-08 | 0.4.1 | phadej |
| vec-optics | 6 | 0.0 | 0 | Vec: length-indexed (sized) list: optics support | (bsd3, data, dependent-types, library, optics) | 2024-06-08 | 0.4.1 | phadej |