The type-settheory package
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).
Properties
| Versions | 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.3.1 |
|---|---|
| Dependencies | base (4.*), containers, syb, template-haskell, transformers, type-equality |
| License | BSD3 |
| Author | Daniel Schüssler |
| Maintainer | daniels@community.haskell.org |
| Stability | Alpha |
| Category | Math, Language, Type System |
| Source repository | darcs get http://code.haskell.org/~daniels/type-settheory |
| Upload date | Wed Nov 3 07:00:55 UTC 2010 |
| Uploaded by | DanielSchuessler |
| Built on | ghc-6.12, ghc-7.0 |
Modules
Downloads
- type-settheory-0.1.3.1.tar.gz (Cabal source package)
- package description (included in the package)