An open API service providing package, version and dependency metadata of many open source software ecosystems and registries.

hackage.haskell.org "dependent-types" keyword

View the packages on the hackage.haskell.org package registry that are tagged with the "dependent-types" keyword.

Agda-executable 2.3.0
8 versions - Latest release: almost 14 years ago - 9.45 thousand downloads total - 2 maintainers
agda2lagda 0.2025.9.5
Simple command line tool to convert plain Agda or Haskell files into literate files. Line commen...
6 versions - Latest release: about 23 hours ago - 7 dependent repositories - 955 downloads total - 14 stars on GitHub - 1 maintainer
type-fun 0.1.3
Fun with types
5 versions - Latest release: over 4 years ago - 1 dependent package - 25 dependent repositories - 3.93 thousand downloads total - 5 stars on GitHub - 1 maintainer
Top 9.7% on hackage.haskell.org
parameterized-utils 2.1.1
A set of utilities for using indexed types including containers, equality, and comparison.
16 versions - Latest release: about 5 years ago - 11 dependent packages - 30 dependent repositories - 11.8 thousand downloads total - 60 stars on GitHub - 6 maintainers
Top 9.0% on hackage.haskell.org
first-class-families 0.8.1.0
A library for type-level programming. See README.
11 versions - Latest release: over 1 year ago - 14 dependent packages - 23 dependent repositories - 13.3 thousand downloads total - 88 stars on GitHub - 1 maintainer
rzk 0.7.6
Please see the README on GitHub at https://github.com/rzk-lang/rzk#readme
29 versions - Latest release: 23 days ago - 2 dependent packages - 1 dependent repositories - 1.34 thousand downloads total - 247 stars on GitHub - 1 maintainer
cubical 0.2.0
Cubical implements an experimental simple type checker for type theory with univalence with an ev...
4 versions - Latest release: over 11 years ago - 3.5 thousand downloads total - 147 stars on GitHub - 1 maintainer
decidable 0.3.1.1 💰
This library provides combinators and typeclasses for working and manipulating type-level predica...
12 versions - Latest release: over 1 year ago - 1 dependent package - 4.85 thousand downloads total - 14 stars on GitHub - 1 maintainer
singleton-dict 0.1.0.0
This package provides a typelevel balanced search tree based on an ancient version of Data.Map, o...
1 version - Latest release: about 8 years ago - 948 downloads total - 0 stars on GitHub - 1 maintainer
path-sing 0.1.0.0
This library wraps the types in the path library with singleton types to allow more well-typed ha...
1 version - Latest release: almost 2 years ago - 75 downloads total - 1 maintainer
fcf-containers 0.8.2
Package fcf-containers provides type-level functions and data structures that operate on type-lev...
12 versions - Latest release: over 2 years ago - 1 dependent package - 2 dependent repositories - 2.31 thousand downloads total - 3 stars on GitHub - 1 maintainer
vec 0.5.1
Nat, Fin, Vec
10 versions - Latest release: about 1 year ago - 2 dependent packages - 12 dependent repositories - 6.35 thousand downloads total - 25 stars on GitHub - 1 maintainer
dependent-enummap 0.1.0.0
1 version - Latest release: 4 months ago - 9 downloads total - 1 maintainer
ivor 0.1.14
9 versions - Latest release: over 14 years ago - 1 dependent repositories - 8.64 thousand downloads total - 2 maintainers
agda-server 0.1.1
3 versions - Latest release: almost 12 years ago - 3.21 thousand downloads total - 1 maintainer
helf 1.0.20240318
HELF = Haskell implementation of the Edinburgh Logical Framework HELF implements only a subset o...
4 versions - Latest release: over 1 year ago - 1.55 thousand downloads total - 1 maintainer
Top 3.9% on hackage.haskell.org
reflection 2.1.9
This package addresses the configuration problem which is propagating configurations that are ava...
52 versions - Latest release: 9 months ago - 30 dependent packages - 267 dependent repositories - 219 thousand downloads total - 102 stars on GitHub - 2 maintainers
Top 4.5% on hackage.haskell.org
dependent-sum 0.6.1
Dependent sums and supporting typeclasses for comparing and displaying them
19 versions - Latest release: about 6 years ago - 34 dependent packages - 131 dependent repositories - 42 thousand downloads total - 56 stars on GitHub - 10 maintainers
show-type 0.1.1
Convert Types into String Values in Haskell
2 versions - Latest release: over 10 years ago - 1 dependent package - 5 dependent repositories - 2.24 thousand downloads total - 2 stars on GitHub - 1 maintainer
ghc-typelits-presburger 0.7.4.2 💰
Presburger arithmetic solver for built-in type-level naturals
24 versions - Latest release: about 2 months ago - 4 dependent packages - 9 dependent repositories - 8.82 thousand downloads total - 9 stars on GitHub - 1 maintainer
singletons-presburger 0.7.4.1 💰
Presburger arithmetic solver for built-in type-level naturals
12 versions - Latest release: about 2 months ago - 3 dependent packages - 8 dependent repositories - 1.68 thousand downloads total - 9 stars on GitHub - 1 maintainer
poly-rec 0.7.0.4
4 versions - Latest release: 10 months ago - 1 dependent repositories - 533 downloads total - 1 maintainer
MiniAgda 0.2025.7.23
MiniAgda is a tiny dependently-typed programming language in the style of Agda. It serves as a la...
12 versions - Latest release: about 1 month ago - 1 dependent repositories - 7.46 thousand downloads total - 1 maintainer
singleton-nats 0.4.7
Unary natural number relying on the singletons infrastructure. More information about the general...
18 versions - Latest release: almost 2 years ago - 1 dependent package - 7 dependent repositories - 10.4 thousand downloads total - 7 stars on GitHub - 2 maintainers
list-witnesses 0.1.4.1 💰
Collection of assorted inductive witnesses and functions for working with type-level lists. *Dat...
9 versions - Latest release: over 1 year ago - 2.88 thousand downloads total - 1 stars on GitHub - 1 maintainer
ral 0.2.2
Nat, Fin, Vec
4 versions - Latest release: about 1 year ago - 1 dependent package - 8 dependent repositories - 9.17 thousand downloads total - 25 stars on GitHub - 1 maintainer
prim-uniq 0.2
Opaque unique identifiers in primitive state monads and a GADT-like type using them as witnesses ...
3 versions - Latest release: over 5 years ago - 4 dependent packages - 14 dependent repositories - 7.53 thousand downloads total - 8 stars on GitHub - 3 maintainers
Sit 0.2023.8.3
Sit = Size-irrelevant types Sit is a prototypical language with an Agda-compatible syntax. It ha...
6 versions - Latest release: about 2 years ago - 1 dependent package - 7 dependent repositories - 3.2 thousand downloads total - 6 stars on GitHub - 1 maintainer
symbols 0.3.0.0
Utilities for manipulating type-level strings natively.
6 versions - Latest release: almost 6 years ago - 1 dependent package - 3 dependent repositories - 3.17 thousand downloads total - 1 maintainer
singleton-bool 0.1.8
Type level booleans
9 versions - Latest release: over 1 year ago - 6 dependent packages - 31 dependent repositories - 30.3 thousand downloads total - 6 stars on GitHub - 1 maintainer
sized-grid 0.2.0.1
`size-grid` allows you to make finite sized grids and have their size and shape confirmed at comp...
7 versions - Latest release: almost 6 years ago - 1 dependent repositories - 3.56 thousand downloads total - 5 stars on GitHub - 1 maintainer
tensor-safe 0.1.0.1
TensorSafe provides a very simple API to create deep neural networks structures which are validat...
2 versions - Latest release: over 6 years ago - 961 downloads total - 102 stars on GitHub - 1 maintainer
ral-lens 0.2.1
Nat, Fin, Vec
3 versions - Latest release: about 1 year ago - 2.18 thousand downloads total - 25 stars on GitHub - 1 maintainer
aeson-dependent-sum 0.1.0.1
Newtype wrappers around Data.Dependent.Sum.DSum, for use with -XDerivingVia. These wrappers are h...
2 versions - Latest release: about 3 years ago - 190 downloads total - 1 maintainer
idris 1.3.4
Idris is a general purpose language with full dependent types. It is compiled, with eager evaluat...
71 versions - Latest release: almost 4 years ago - 24 dependent repositories - 70.8 thousand downloads total - 2 maintainers
mezzo 0.3.1.0
A Haskell music composition library that enforces common musical rules in the type system.
6 versions - Latest release: almost 8 years ago - 1 dependent repositories - 4.11 thousand downloads total - 351 stars on GitHub - 1 maintainer
fin 0.3.2
Nat, Fin, Vec
11 versions - Latest release: 10 months ago - 6 dependent packages - 13 dependent repositories - 14 thousand downloads total - 25 stars on GitHub - 1 maintainer
matrix-sized 0.1.1
A Haskell implementation of matrices with statically known sizes. The library also comes with the...
6 versions - Latest release: about 5 years ago - 3 dependent repositories - 1.39 thousand downloads total - 0 stars on GitHub - 1 maintainer
agda-snippets 2.5.2
Library and tool to render the snippets in literate Agda files to hyperlinked HTML, leaving the r...
4 versions - Latest release: over 8 years ago - 1 dependent repositories - 4.01 thousand downloads total - 11 stars on GitHub - 1 maintainer
bin 0.1.4
Nat, Fin, Vec
5 versions - Latest release: about 1 year ago - 1 dependent package - 6 dependent repositories - 9.07 thousand downloads total - 25 stars on GitHub - 1 maintainer
hoq 0.3
Package maintainers For package maintainers and hackage trustees Candidates A language bas...
3 versions - Latest release: almost 11 years ago - 2.5 thousand downloads total - 83 stars on GitHub - 1 maintainer
eliminators 0.9.6
This library provides eliminators for inductive data types, leveraging the power of the singleton...
17 versions - Latest release: 8 months ago - 7 dependent repositories - 6.5 thousand downloads total - 28 stars on GitHub - 1 maintainer
agda-snippets-hakyll 0.1.1
Library and tool to render the snippets in literate Agda files to hyperlinked HTML, leaving the r...
6 versions - Latest release: almost 10 years ago - 1 dependent repositories - 4.68 thousand downloads total - 11 stars on GitHub - 1 maintainer
lens-typelevel 0.1.1.0 💰
Type-level lenses using singletons and its defunctionalization system, implemented using the same...
3 versions - Latest release: almost 7 years ago - 1.78 thousand downloads total - 15 stars on GitHub - 1 maintainer
constrained-some 0.1.2
This library provides utilities for working with existential types and type-level constraints. It...
3 versions - Latest release: 9 months ago - 106 downloads total - 1 stars on GitHub - 1 maintainer
type-level-bst 0.1
Type-Level Binary Search Tree in Haskell
1 version - Latest release: almost 11 years ago - 1.19 thousand downloads total - 7 stars on GitHub - 1 maintainer
vec-optics 0.4.1
Nat, Fin, Vec
3 versions - Latest release: about 1 year ago - 726 downloads total - 25 stars on GitHub - 1 maintainer
ral-optics 0.2.1
Nat, Fin, Vec
3 versions - Latest release: about 1 year ago - 742 downloads total - 25 stars on GitHub - 1 maintainer
vec-lens 0.4.1
Nat, Fin, Vec
3 versions - Latest release: about 1 year ago - 2.1 thousand downloads total - 25 stars on GitHub - 1 maintainer
pisigma 0.2.1
5 versions - Latest release: over 14 years ago - 4.03 thousand downloads total - 2 maintainers
open-typerep 0.6.1
Open type representations and dynamic types
9 versions - Latest release: over 9 years ago - 1 dependent repositories - 5.8 thousand downloads total - 4 stars on GitHub - 1 maintainer
type-indexed-queues 0.2.0.0
This library provides implementations of five different queues (binomial, pairing, skew, leftist,...
3 versions - Latest release: over 8 years ago - 1 dependent repositories - 2.14 thousand downloads total - 8 stars on GitHub - 1 maintainer
instance-map 0.1.0.0
instance-map provides Template Haskell functions that help go from serialized values with value-l...
1 version - Latest release: about 7 years ago - 805 downloads total - 2 stars on GitHub - 1 maintainer
uAgda 1.2.0.4
9 versions - Latest release: over 13 years ago - 7.09 thousand downloads total - 1 maintainer
agda-unused 0.3.0
A tool to check for unused code in an Agda project.
3 versions - Latest release: almost 3 years ago - 1 dependent package - 436 downloads total - 1 maintainer
typeparams 0.0.6
Lens-like interface for type level parameters; allows unboxed unboxed vectors and supercompilation
7 versions - Latest release: over 10 years ago - 1 dependent repositories - 5 thousand downloads total - 42 stars on GitHub - 1 maintainer
dec 0.0.6
Decidable propositions
4 versions - Latest release: over 1 year ago - 4 dependent packages - 11 dependent repositories - 21.8 thousand downloads total - 4 stars on GitHub - 1 maintainer
Top 4.2% on hackage.haskell.org
Agda 2.8.0
Agda is a dependently typed functional programming language: It has inductive families, which are...
45 versions - Latest release: 2 months ago - 6 dependent packages - 61 dependent repositories - 65.8 thousand downloads total - 4 maintainers
PandocAgda 2.3.3
Agda is a dependently typed functional programming language and a proof assistant. This package ...
3 versions - Latest release: over 12 years ago - 2.93 thousand downloads total - 1 maintainer
singletons-base-code-generator 0.1
A <code>cabal</code> code generator used in the test suite for the <code>singletons-base</code> l...
1 version - Latest release: 8 months ago - 29 downloads total - 291 stars on GitHub - 1 maintainer
singletons-th 3.1.1
singletons-th defines Template Haskell functionality that allows promotion of term-level function...
7 versions - Latest release: about 3 years ago - 7 dependent packages - 19 dependent repositories - 4.45 thousand downloads total - 286 stars on GitHub - 1 maintainer
singletons-base 3.1.1
singletons-base uses singletons-th to define promoted and singled functions from the base library...
7 versions - Latest release: about 3 years ago - 22 dependent packages - 27 dependent repositories - 3.93 thousand downloads total - 286 stars on GitHub - 1 maintainer
Top 3.1% on hackage.haskell.org
singletons 3.0.4
singletons contains the basic types and definitions needed to support dependently typed programmi...
36 versions - Latest release: 9 months ago - 47 dependent packages - 248 dependent repositories - 52.5 thousand downloads total - 286 stars on GitHub - 2 maintainers
nanoAgda 1.0.0
3 versions - Latest release: over 13 years ago - 2.51 thousand downloads total - 1 maintainer
Top 7.8% on hackage.haskell.org
some 1.0.6
Existential type.
11 versions - Latest release: almost 2 years ago - 20 dependent packages - 47 dependent repositories - 29.3 thousand downloads total - 37 stars on GitHub - 1 maintainer
compare-type 0.1.1
Compare Types of Any Kinds in Haskell
2 versions - Latest release: over 10 years ago - 1.87 thousand downloads total - 1 stars on GitHub - 1 maintainer
type-equality 1.0.1
Haskell definition of type equality, coercion/cast and other operations.
7 versions - Latest release: over 1 year ago - 5 dependent packages - 17 dependent repositories - 29.3 thousand downloads total - 11 stars on GitHub - 3 maintainers
Top 5.0% on hackage.haskell.org
dependent-map 0.1.1
Provides a type called DMap which generalizes Data.Map.Map, allowing keys to specify the type of ...
13 versions - Latest release: about 14 years ago - 26 dependent packages - 93 dependent repositories - 30.4 thousand downloads total - 66 stars on GitHub - 8 maintainers
proof-assistant-bot 0.2.2
Bridge between Telegram Bot and several proof assistants. Currently following proof assistant su...
3 versions - Latest release: over 1 year ago - 1 dependent package - 209 downloads total - 10 stars on GitHub - 1 maintainer
type-natural 1.3.0.2 💰
Type-level well-kinded natural numbers.
49 versions - Latest release: 8 months ago - 2 dependent packages - 14 dependent repositories - 29.1 thousand downloads total - 34 stars on GitHub - 1 maintainer