name: type-settheory
version: 0.1
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
extra-source-files: Type/defs.h.hs
stability: Alpha
source-repository head
type: darcs
location: http://code.haskell.org/~daniels/type-settheory
Library
build-depends: base >= 4, base < 5
, syb
, category-extras, type-equality
, template-haskell
, mtl
, containers
exposed-modules: Type.Logic
Type.Set
Type.Set.Example
Type.Function
Type.Dummies
Data.Category
Data.Typeable.Extras
Control.SMonad
other-modules: Helper
ghc-options: