The type-settheory package

[Tags: bsd3, library]

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:

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


Properties

Versions0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.3.1
Dependenciesbase (==4.*), category-extras, containers, mtl, syb, template-haskell, type-equality
LicenseBSD3
AuthorDaniel Schüssler
Maintainerdaniels@community.haskell.org
StabilityAlpha
CategoryMath, Language
Source repositoryhead: darcs get http://code.haskell.org/~daniels/type-settheory
Upload dateTue Oct 27 12:46:37 UTC 2009
Uploaded byDanielSchuessler
Downloads403 total (39 in last 30 days)

Modules

Downloads

Maintainers' corner

For package maintainers and hackage trustees