The type-settheory package

[ Tags: bsd3, language, library, math, type-system ] [ Propose Tags ]

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


Versions 0.1, 0.1.1, 0.1.2, 0.1.3,
Dependencies base (==4.*), category-extras, containers, mtl, syb, template-haskell, type-equality [details]
License BSD3
Author Daniel Schüssler
Category Math, Language
Source repo head: darcs get
Uploaded Tue Oct 27 12:46:37 UTC 2009 by DanielSchuessler
Distributions NixOS:
Downloads 1684 total (15 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-31 [all 6 reports]
Hackage Matrix CI


  • Control
    • Control.SMonad
  • Data
    • Data.Category
    • Typeable
      • Data.Typeable.Extras
  • Type
    • Type.Dummies
    • Type.Function
    • Type.Logic
    • Type.Set
      • Type.Set.Example


Maintainer's Corner

For package maintainers and hackage trustees