# 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, mtl, syb, template-haskell, type-equality [details] |

License | BSD3 |

Author | Daniel Schüssler |

Maintainer | daniels@community.haskell.org |

Stability | Alpha |

Category | Math, Language |

Source repository | head: darcs get http://code.haskell.org/~daniels/type-settheory |

Uploaded | Wed Sep 1 02:37:05 UTC 2010 by DanielSchuessler |

Distributions | NixOS:0.1.3.1 |

Downloads | 961 total (9 in the last 30 days) |

Votes | |

Status | Docs uploaded by user Build status unknown [no reports yet] |

## Downloads

- type-settheory-0.1.3.tar.gz [browse] (Cabal source package)
- Package description (included in the package)