# type-settheory: Type-level sets and functions expressed as types

Type classes can express sets and functions on the type level, but they are not first-class citizens. Here we take the approach of expressing type-level sets and functions as *types*. The instance system is replaced by value-level proofs which can be directly manipulated. In this way the Haskell type level can support a quite expressive constructive set theory; for example, we have:

Subsets and extensional set equality

Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a kind of dependent sum and product

Functions and their composition, images, preimages, injectivity

The meaning of the proposition-types here is *not* purely by convention; it is actually grounded in GHC "reality": A proof of `A :=: B`

gives us a safe coercion operator `A -> B`

(while the logic is inconsistent *at compile-time* due to the fact that Haskell has general recursion, we still have that proofs of falsities are `undefined`

or non-terminating programs, so for example if `Refl`

is successfully pattern-matched, the proof must have been correct).

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 | BSD-3-Clause |

Author | Daniel Schüssler |

Maintainer | daniels@community.haskell.org |

Category | Math, Language |

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

Uploaded | by DanielSchuessler at Tue Oct 27 18:53:41 UTC 2009 |

Distributions | NixOS:0.1.3.1 |

Downloads | 1902 total (21 in the last 30 days) |

Rating | (no votes yet) [estimated by rule of succession] |

Your Rating | |

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

## Modules

[Index]

## Downloads

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