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

Type.Set

Contents

Description

  • Sets are encoded as certain types of kind * -> *
  • A value of type S X is a proof that the type X is a member of S

Synopsis

Subsets, equality

type :∈: a set = set aSource

data set1 :⊆: set2 whereSource

Represents a proof that set1 is a subset of set2

Constructors

Subset :: (forall a. (a :∈: set1) -> a :∈: set2) -> set1 :⊆: set2 

Instances

Fact (Disjoint s t -> :⊆: t (Complement s)) 
Fact (:⊆: set1 set2 -> :∈: a set1 -> :∈: a set2) 
Fact (:⊆: s1 t -> :⊆: s2 t -> :⊆: (:∪: s1 s2) t) 
Fact (:⊆: t s1 -> :⊆: t s2 -> :⊆: t (:∩: s1 s2)) 
Fact (:⊆: u1 u2 -> ::∈: s (Powerset u1) -> ::∈: s (Powerset u2)) 
Fact (:⊆: s1 s2 -> ::∈: s2 (Powerset u) -> ::∈: s1 (Powerset u)) 
Fact (:⊆: s1 s2 -> :⊆: s2 s3 -> :⊆: s1 s3) 
Fact (:⊆: s1 t1 -> :⊆: s2 t2 -> :⊆: (:×: s1 s2) (:×: t1 t2)) 
(cod' ~ cod'_copy, Fact (:~>: dom cod f)) => Fact (:⊆: cod cod'_copy -> :~>: dom cod' f) 
Fact (:⊆: dom cod -> :~>: dom cod (Incl dom cod)) 
Fact (:∈: (Lower s) fam -> :⊆: (Inters fam) s) 
Fact (:∈: (Lower s) fam -> :⊆: s (Unions fam)) 
Fact (:~>: dom cod f -> :⊆: (Image f (Preimage f set)) set) 
Fact (:~>: dom cod f -> :⊆: set dom -> :⊆: set (Preimage f (Image f set))) 
Fact (:~>: s t f1 -> :⊆: (Equaliser f1 f2) s) 
Fact (:~>: dom cod f -> :⊆: cod cod' -> :~>: dom cod' f) 
Fact (:~>: dom cod f -> :~>: dom cod' f' -> :⊆: f f' -> :==: f f') 
Fact (:~>: dom cod f -> :⊆: f (:×: dom cod)) 
(Fact (:⊆: t s1), Fact (:⊆: t s2)) => Fact (:⊆: t (:∩: s1 s2)) 
Fact (:⊆: s2 (:∪: s1 s2)) 
Fact (:⊆: s1 (:∪: s1 s2)) 
Fact (:⊆: s Univ) 
Fact (:⊆: s s) 
Fact (:⊆: MonadPlusType MonadType) 
Fact (:⊆: IntegralType NumType) 
Fact (:⊆: NumType EqType) 
Fact (:⊆: OrdType EqType) 
Fact (:⊆: Empty s) 
Fact (:⊆: (:∩: s1 s2) s2) 
Fact (:⊆: (:∩: s1 s2) s1) 
(Fact (:⊆: s1 t), Fact (:⊆: s2 t)) => Fact (:⊆: (:∪: s1 s2) t) 
Fact (:∈: a set) => Fact (:⊆: (Singleton a) set) 
Fact (:⊆: ExampleSet TypeableType) 
Fact (:⊆: ExampleSet OrdType) 
Fact (:⊆: ExampleSet EqType) 

scoerce :: (set1 :⊆: set2) -> (a :∈: set1) -> a :∈: set2Source

Coercion from subset to superset

data set1 :==: set2 Source

Extensional equality of sets

Constructors

SetEq (set1 :⊆: set2) (set2 :⊆: set1) 

Instances

Fact (Ex dom -> :==: (Const dom x) (Const dom' x') -> :=: x x') 
Fact (:==: s1 s2 -> :==: s2 s3 -> :==: s1 s3) 
Fact (:==: s1 s2 -> :==: s2 s1) 
Fact (:==: s1 s2 -> :∈: a s2 -> :∈: a s1) 
Fact (:==: s1 s2 -> :∈: a s1 -> :∈: a s2) 
Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) 
Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Snd cod1 cod2) (:***: f1 f2)) f2) 
Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Fst cod1 cod2) (:***: f1 f2)) f1) 
Fact (:~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> :==: (:○: (:○: g f) f1) (:○: g (:○: f f1))) 
Fact (:~>: total base bun -> :~>: base total f -> :==: (:○: bun f) (Id base) -> Section bun f) 
Fact (:~>: total base bun -> :~>: base total f -> Section bun f -> :==: (:○: bun f) (Id base)) 
Fact (:~>: d c f -> :==: (:○: f (Id d)) f) 
Fact (:~>: d c f -> :==: (:○: (Id c) f) f) 
Fact (:~>: dom cod f -> :==: (Image f (:∪: s1 s2)) (:∪: (Image f s1) (Image f s2))) 
Fact (:~>: dom cod f -> :~>: dom2 cod f -> :==: dom dom2) 
Fact (:~>: d c f' -> :==: f f' -> :∈: (x, y) f -> :∈: (x, y') f' -> :=: y y') 
Fact (:~>: s0 s g -> :~>: s t f1 -> :==: (:○: f1 g) (:○: f2 g) -> :~>: s0 (Equaliser f1 f2) g) 
Fact (:~>: dom cod f -> :~>: dom cod' f' -> :⊆: f f' -> :==: f f') 
Fact (:==: s s) 
Fact (:==: (Inv (Id dom)) (Id dom)) 

ecoerce :: (s1 :==: s2) -> (a :∈: s1) -> a :∈: s2Source

Coercion using a set equality

ecoerceFlip :: (s1 :==: s2) -> (a :∈: s2) -> a :∈: s1Source

Coercion using a set equality (flipped)

subsetTrans :: (s1 :⊆: s2) -> (s2 :⊆: s3) -> s1 :⊆: s3Source

setEqSym :: (s1 :==: s2) -> s2 :==: s1Source

setEqTrans :: (s1 :==: s2) -> (s2 :==: s3) -> s1 :==: s3Source

type Singleton a = :=: aSource

Union, intersection, difference

data s1 :∪: s2 whereSource

Binary union

Constructors

Union :: Either (a :∈: s1) (a :∈: s2) -> (s1 :∪: s2) a 

Instances

Fact (:⊆: s1 t -> :⊆: s2 t -> :⊆: (:∪: s1 s2) t) 
Fact (:~>: dom cod f -> :==: (Image f (:∪: s1 s2)) (:∪: (Image f s1) (Image f s2))) 
Fact (:⊆: s2 (:∪: s1 s2)) 
Fact (:⊆: s1 (:∪: s1 s2)) 
(Fact (:⊆: s1 t), Fact (:⊆: s2 t)) => Fact (:⊆: (:∪: s1 s2) t) 

elimUnion :: (a :∈: (s1 :∪: s2)) -> Either (a :∈: s1) (a :∈: s2)Source

unionL :: s1 :⊆: (s1 :∪: s2)Source

unionR :: s2 :⊆: (s1 :∪: s2)Source

unionMinimal :: (s1 :⊆: t) -> (s2 :⊆: t) -> (s1 :∪: s2) :⊆: tSource

data s1 :∩: s2 whereSource

Binary intersection

Constructors

Inter :: (a :∈: s1) -> (a :∈: s2) -> (s1 :∩: s2) a 

Instances

Fact (:⊆: t s1 -> :⊆: t s2 -> :⊆: t (:∩: s1 s2)) 
(Fact (:⊆: t s1), Fact (:⊆: t s2)) => Fact (:⊆: t (:∩: s1 s2)) 
Fact (:⊆: (:∩: s1 s2) s2) 
Fact (:⊆: (:∩: s1 s2) s1) 

elimInter :: (a :∈: (s1 :∩: s2)) -> (a :∈: s1, a :∈: s2)Source

interFst :: (s1 :∩: s2) :⊆: s1Source

interSnd :: (s1 :∩: s2) :⊆: s2Source

interMaximal :: (t :⊆: s1) -> (t :⊆: s2) -> t :⊆: (s1 :∩: s2)Source

data Unions fam whereSource

Union of a family

Constructors

Unions :: (Lower s :∈: fam) -> (a :∈: s) -> Unions fam a 

Instances

Fact (:∈: (Lower s) fam -> :⊆: s (Unions fam)) 

elimUnions :: Unions fam a -> (forall s. (Lower s :∈: fam) -> (a :∈: s) -> r) -> rSource

data Σ fam whereSource

Dependent sum

Constructors

Σ :: (Lower s :∈: fam) -> (a :∈: s) -> Σ fam (Lower s, a) 

data Inters fam whereSource

Intersection of a family

Constructors

Inters :: (forall s. (Lower s :∈: fam) -> a :∈: s) -> Inters fam a 

Instances

Fact (:∈: (Lower s) fam -> :⊆: (Inters fam) s) 

elimInters :: Inters fam a -> (Lower s :∈: fam) -> s aSource

data Complement s whereSource

Complement

Constructors

Complement :: Not (a :∈: s) -> Complement s a 

Instances

Fact (Not (s a, Complement s a)) 
Fact (Disjoint s t -> :⊆: t (Complement s)) 
Fact (Disjoint s (Complement s)) 

type Disjoint s1 s2 = (s1 :∩: s2) :⊆: EmptySource

data Diff s t whereSource

Set difference

Constructors

Diff :: (a :∈: s) -> Not (a :∈: t) -> Diff s t a 

elimDiff :: (a :∈: Diff s t) -> (a :∈: s, Not (a :∈: t))Source

Products

data s1 :×: s2 whereSource

Binary products

Constructors

:×: :: (a :∈: s1) -> (b :∈: s2) -> (s1 :×: s2) (a, b) 

Instances

Fact (:⊆: s1 t1 -> :⊆: s2 t2 -> :⊆: (:×: s1 s2) (:×: t1 t2)) 
Fact (:∈: (a, b) (:×: s1 s2) -> :∈: b s2) 
Fact (:∈: (a, b) (:×: s1 s2) -> :∈: a s1) 
Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) 
Fact (:~>: dom cod f -> :∈: pair f -> :∈: pair (:×: dom cod)) 
Fact (:~>: dom cod f -> :⊆: f (:×: dom cod)) 
Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :~>: dom (:×: cod1 cod2) (:***: f1 f2)) 
(Fact (:~>: dom cod1 f1), Fact (:~>: dom cod2 f2)) => Fact (:~>: dom (:×: cod1 cod2) (:***: f1 f2)) 
Fact (:~>: (:×: s1 s2) s2 (Snd s1 s2)) 
Fact (:~>: (:×: s1 s2) s1 (Fst s1 s2)) 
Fact (:~>: (:×: Univ Univ) (KleisliType m) (KleisliHom m)) 
Fact (:~>: (:×: Univ Univ) FunctionType HaskFun) 
Fact (:~>: (:×: Univ Univ) Univ (BiGraph f)) 

fstPrf :: ((a, b) :∈: (s1 :×: s2)) -> a :∈: s1Source

sndPrf :: ((a, b) :∈: (s1 :×: s2)) -> b :∈: s2Source

prodMonotonic :: (s1 :⊆: t1) -> (s2 :⊆: t2) -> (s1 :×: s2) :⊆: (t1 :×: t2)Source

Product is monotonic wrt. subset inclusion

Particular sets

data Empty whereSource

Empty set (barring cheating with undefined)

Constructors

Empty :: (forall b. b) -> Empty a 

Instances

Fact (Empty a -> b) 
Fact (:⊆: Empty s) 

data Univ whereSource

Set of all types of kind *

Constructors

Univ :: Univ a 

data FunctionType whereSource

Constructors

FunctionType :: FunctionType (a -> b) 

data KleisliType m whereSource

Constructors

KleisliType :: KleisliType m (a -> m b) 

Instances

Fact (:∈: (a -> m b) (KleisliType m)) 
Fact (:~>: (:×: Univ Univ) (KleisliType m) (KleisliHom m)) 

data CoKleisliType w whereSource

Constructors

CoKleisliType :: CoKleisliType w (w a -> b) 

Instances

Fact (:∈: (w a -> b) (CoKleisliType w)) 

Sets from common typeclasses

data ShowType whereSource

Constructors

ShowType :: Show a => ShowType a 

Instances

Show a => Fact (:∈: a ShowType) 

getShow :: (a :∈: ShowType) -> a -> StringSource

Example application

data ReadType whereSource

Constructors

ReadType :: Read a => ReadType a 

Instances

Read a => Fact (:∈: a ReadType) 

data EqType whereSource

Constructors

EqType :: Eq a => EqType a 

getEq :: (a :∈: EqType) -> a -> a -> BoolSource

data OrdType whereSource

Constructors

OrdType :: Ord a => OrdType a 

data EnumType whereSource

Constructors

EnumType :: Enum a => EnumType a 

Instances

Enum a => Fact (:∈: a EnumType) 

data BoundedType whereSource

Constructors

BoundedType :: Bounded a => BoundedType a 

Instances

data NumType whereSource

Constructors

NumType :: Num a => NumType a 

data MonoidType whereSource

Constructors

MonoidType :: Monoid a => MonoidType a 

Instances

data DataType whereSource

Constructors

DataType :: Data a => DataType a 

Instances

Data a => Fact (:∈: a DataType) 

Kind (* -> *)

data FunctorType whereSource

Constructors

FunctorType :: Functor a => FunctorType (Lower a) 

Instances

getFmap :: (Lower f :∈: FunctorType) -> (a -> b) -> f a -> f bSource

data MonadType whereSource

Constructors

MonadType :: Monad a => MonadType (Lower a) 

Powerset

type ::∈: a set = set (Lower a)Source

Membership of a set in a set representing a set of sets

data Powerset u whereSource

Powerset

Constructors

Powerset :: (s :⊆: u) -> Powerset u (Lower s) 

Instances

Fact (:⊆: u1 u2 -> ::∈: s (Powerset u1) -> ::∈: s (Powerset u2)) 
Fact (:⊆: s1 s2 -> ::∈: s2 (Powerset u) -> ::∈: s1 (Powerset u)) 

Misc

data ProofSet s whereSource

Constructors

ProofSet :: s x -> ProofSet s (s x) 

Unique existence of sets

data ExUniq1 p whereSource

Unique existence, unlowered

Constructors

ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p 

From sets to the value level

data V s whereSource

V s is the sum of all types x such that s x is provable.

Constructors

V :: s x -> x -> V s 

Instances

(Fact (:⊆: s EqType), Fact (:⊆: s TypeableType)) => Eq (V s) 
(Fact (:⊆: s OrdType), Fact (:⊆: s TypeableType), Eq (V s)) => Ord (V s) 

liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> V s -> V s -> BoolSource