name:                type-settheory
version:             0.1.3
synopsis:            
 Sets and functions-as-relations in the type system
description:         
 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). 
 
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.Typeable.Extras
 other-modules:       Helper, Defs
 ghc-options: