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

Package maintainers

• DanielSchuessler

For package maintainers and hackage trustees

• edit package information

Candidates

• No Candidates