name: type-settheory version: 0.1.2 synopsis: Type-level sets and functions expressed as types description: 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). category: Math, Language license: BSD3 license-file: LICENSE author: Daniel Schüssler maintainer: daniels@community.haskell.org build-type: Simple cabal-version: >= 1.6 stability: Alpha source-repository head type: darcs location: http://code.haskell.org/~daniels/type-settheory Library build-depends: base >= 4, base < 5 , syb , type-equality , template-haskell , mtl , containers exposed-modules: Type.Logic Type.Set Type.Set.Example Type.Function Type.Dummies Type.Nat Data.Category Data.Typeable.Extras Control.SMonad other-modules: Helper, Defs ghc-options: