type-settheory: Sets and functions-as-relations in the type system
Type classes can express sets and functions on the type level, but they are not first-class. This package expresses type-level sets and functions as types instead.
Instances are replaced by value-level proofs which can be directly manipulated; this makes quite a bit of (constructive) set theory expressible; for example, we have:
Subsets and extensional set equality
Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a sort of dependent sum and product
Functions and their composition, images, preimages, injectivity
The proposition-types (derived from the :=:
equality type) aren't meaningful purely by convention; they relate to the rest of Haskell as follows: A proof of A :=: B
gives us a safe coercion operator A -> B
(while the logic is inevitably inconsistent at compile-time since undefined
proves anything, I think that we still have the property that if the Refl
value is successfully pattern-matched, then the two parameters in its type are actually equal).
Modules
[Index]
Downloads
- type-settheory-0.1.3.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.3.1 |
---|---|
Dependencies | base (>=4 && <5), containers, syb, template-haskell, transformers, type-equality [details] |
License | BSD-3-Clause |
Author | Daniel Schüssler |
Maintainer | daniels@community.haskell.org |
Category | Math, Language, Type System |
Source repo | head: darcs get http://code.haskell.org/~daniels/type-settheory |
Uploaded | by DanielSchuessler at 2010-11-03T07:00:55Z |
Distributions | |
Reverse Dependencies | 1 direct, 0 indirect [details] |
Downloads | 3746 total (5 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs uploaded by user Build status unknown [no reports yet] |