The type-settheory package

[Tags: bsd3, library]

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:

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

Versions0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.3.1
Dependenciesbase (==4.*), 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 dateWed Sep 1 02:37:05 UTC 2010
Uploaded byDanielSchuessler
Downloads319 total (21 in last 30 days)

Modules

[Index]

Downloads

Maintainers' corner

For package maintainers and hackage trustees