type-settheory: Sets and functions-as-relations in the type system

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

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.3.1
Dependencies base (>=4 && <5), containers, syb, template-haskell, transformers, type-equality [details]
License BSD-3-Clause
Author Daniel Schüssler
Maintainer daniels@community.haskell.org
Category Math, Language, Type System
Source repo head: darcs get http://code.haskell.org/~daniels/type-settheory
Uploaded by DanielSchuessler at 2010-11-03T07:00:55Z
Distributions NixOS:0.1.3.1
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 3529 total (8 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]