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).

Modules

[Last Documentation]

Downloads

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

Maintainer's Corner

Package maintainers

• DanielSchuessler

For package maintainers and hackage trustees

• edit package information

Candidates

• No Candidates