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

Instances

 Fact (:⊆: s Univ) Fact (:~>: Univ Univ (Graph f)) Fact (:~>: (:×: Univ Univ) (KleisliType m) (KleisliHom m)) Fact (:~>: (:×: Univ Univ) FunctionType HaskFun) Fact (:~>: (:×: Univ Univ) Univ (BiGraph f))

data FunctionType whereSource

Constructors

 FunctionType :: FunctionType (a -> b)

Instances

 Fact (:∈: (a -> b) FunctionType) Fact (:~>: (:×: Univ Univ) FunctionType HaskFun)

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

Constructors

Instances

data EqType whereSource

Constructors

 EqType :: Eq a => EqType a

Instances

 Fact (:⊆: NumType EqType) Fact (:⊆: OrdType EqType) Fact (:⊆: ExampleSet EqType) Eq a => Fact (:∈: a EqType)

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

data OrdType whereSource

Constructors

 OrdType :: Ord a => OrdType a

Instances

 Fact (:⊆: OrdType EqType) Fact (:⊆: ExampleSet OrdType) Ord a => Fact (:∈: a OrdType)

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

 Bounded a => Fact (:∈: a BoundedType)

data NumType whereSource

Constructors

 NumType :: Num a => NumType a

Instances

 Fact (:⊆: IntegralType NumType) Fact (:⊆: NumType EqType) Num a => Fact (:∈: a NumType)

data IntegralType whereSource

Constructors

 IntegralType :: Integral a => IntegralType a

Instances

 Fact (:⊆: IntegralType NumType) Integral a => Fact (:∈: a IntegralType)

data MonoidType whereSource

Constructors

 MonoidType :: Monoid a => MonoidType a

Instances

 Monoid a => Fact (:∈: a MonoidType)

data FractionalType whereSource

Constructors

 FractionalType :: Fractional a => FractionalType a

Instances

 Fractional a => Fact (:∈: a FractionalType)

data TypeableType whereSource

Constructors

 TypeableType :: Typeable a => TypeableType a

Instances

 Fact (:⊆: ExampleSet TypeableType) Typeable a => Fact (:∈: a TypeableType)

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

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

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

Constructors

Instances

Constructors

Instances

data ApplicativeType whereSource

Constructors

 ApplicativeType :: Applicative a => ApplicativeType (Lower a)

Instances

 Applicative a => Fact (:∈: (Lower a) ApplicativeType)

# 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