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: