type-settheory-0.1.2: Type-level sets and functions expressed as typesSource codeContentsIndex
Type.Set
Contents
Subsets, equality
Union, intersection, difference
Products
Particular sets
Sets from common typeclasses
Kind (* -> *)
Powerset
Misc
Unique existence of sets
From sets to the value level
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
type :∈: a set = set a
data set1 :⊆: set2 where
Subset :: (forall a. (a :∈: set1) -> a :∈: set2) -> set1 :⊆: set2
scoerce :: (set1 :⊆: set2) -> (a :∈: set1) -> a :∈: set2
type Subset = :⊆:
data set1 :==: set2 = SetEq (set1 :⊆: set2) (set2 :⊆: set1)
ecoerce :: (s1 :==: s2) -> (a :∈: s1) -> a :∈: s2
ecoerceFlip :: (s1 :==: s2) -> (a :∈: s2) -> a :∈: s1
subsetRefl :: s :⊆: s
subsetTrans :: (s1 :⊆: s2) -> (s2 :⊆: s3) -> s1 :⊆: s3
setEqRefl :: s :==: s
setEqSym :: (s1 :==: s2) -> s2 :==: s1
setEqTrans :: (s1 :==: s2) -> (s2 :==: s3) -> s1 :==: s3
type Singleton a = :=: a
data s1 :∪: s2 where
Union :: Either (a :∈: s1) (a :∈: s2) -> (s1 :∪: s2) a
elimUnion :: (a :∈: (s1 :∪: s2)) -> Either (a :∈: s1) (a :∈: s2)
type Union = :∪:
unionL :: s1 :⊆: (s1 :∪: s2)
unionR :: s2 :⊆: (s1 :∪: s2)
unionMinimal :: (s1 :⊆: t) -> (s2 :⊆: t) -> (s1 :∪: s2) :⊆: t
unionIdempotent :: (s :∪: s) :==: s
data s1 :∩: s2 where
Inter :: (a :∈: s1) -> (a :∈: s2) -> (s1 :∩: s2) a
elimInter :: (a :∈: (s1 :∩: s2)) -> (a :∈: s1, a :∈: s2)
interFst :: (s1 :∩: s2) :⊆: s1
interSnd :: (s1 :∩: s2) :⊆: s2
type Inter = :∩:
interMaximal :: (t :⊆: s1) -> (t :⊆: s2) -> t :⊆: (s1 :∩: s2)
interIdempotent :: (s :∩: s) :==: s
data Unions fam where
Unions :: (Lower s :∈: fam) -> (a :∈: s) -> Unions fam a
elimUnions :: Unions fam a -> (forall s. (Lower s :∈: fam) -> (a :∈: s) -> r) -> r
data Σ fam where
Σ :: (Lower s :∈: fam) -> (a :∈: s) -> Σ fam (Lower s, a)
type DependentSum = Σ
data Inters fam where
Inters :: (forall s. (Lower s :∈: fam) -> a :∈: s) -> Inters fam a
elimInters :: Inters fam a -> (Lower s :∈: fam) -> s a
data Complement s where
Complement :: Not (a :∈: s) -> Complement s a
elimComplement :: (a :∈: Complement s) -> Not (a :∈: s)
type Disjoint s1 s2 = (s1 :∩: s2) :⊆: Empty
complContradiction :: Not (s a, Complement s a)
complEmpty :: Disjoint s (Complement s)
complMaximal :: Disjoint s t -> t :⊆: Complement s
data Diff s t where
Diff :: (a :∈: s) -> Not (a :∈: t) -> Diff s t a
elimDiff :: (a :∈: Diff s t) -> (a :∈: s, Not (a :∈: t))
data s1 :×: s2 where
:×: :: (a :∈: s1) -> (b :∈: s2) -> (s1 :×: s2) (a, b)
type Prod = :×:
fstPrf :: ((a, b) :∈: (s1 :×: s2)) -> a :∈: s1
sndPrf :: ((a, b) :∈: (s1 :×: s2)) -> b :∈: s2
prodMonotonic :: (s1 :⊆: t1) -> (s2 :⊆: t2) -> (s1 :×: s2) :⊆: (t1 :×: t2)
data Empty where
Empty :: (forall b. b) -> Empty a
elimEmpty :: Empty a -> b
emptySubset :: Empty :⊆: s
data Univ where
Univ :: Univ a
univSubset :: s :⊆: Univ
data FunctionType where
FunctionType :: FunctionType (a -> b)
functionType :: (a -> b) :∈: FunctionType
data KleisliType m where
KleisliType :: KleisliType m (a -> m b)
kleisliType :: (a -> m b) :∈: KleisliType m
data CoKleisliType w where
CoKleisliType :: CoKleisliType w (w a -> b)
coKleisliType :: (w a -> b) :∈: CoKleisliType w
data ShowType where
ShowType :: Show a => ShowType a
getShow :: (a :∈: ShowType) -> a -> String
data ReadType where
ReadType :: Read a => ReadType a
data EqType where
EqType :: Eq a => EqType a
getEq :: (a :∈: EqType) -> a -> a -> Bool
data OrdType where
OrdType :: Ord a => OrdType a
getCompare :: (a :∈: OrdType) -> a -> a -> Ordering
data EnumType where
EnumType :: Enum a => EnumType a
data BoundedType where
BoundedType :: Bounded a => BoundedType a
data NumType where
NumType :: Num a => NumType a
data IntegralType where
IntegralType :: Integral a => IntegralType a
data MonoidType where
MonoidType :: Monoid a => MonoidType a
data FractionalType where
FractionalType :: Fractional a => FractionalType a
data TypeableType where
TypeableType :: Typeable a => TypeableType a
data DataType where
DataType :: Data a => DataType a
data FunctorType where
FunctorType :: Functor a => FunctorType (Lower a)
getFmap :: (Lower f :∈: FunctorType) -> (a -> b) -> f a -> f b
data MonadType where
MonadType :: Monad a => MonadType (Lower a)
data MonadPlusType where
MonadPlusType :: MonadPlus a => MonadPlusType (Lower a)
data ApplicativeType where
ApplicativeType :: Applicative a => ApplicativeType (Lower a)
type ::∈: a set = set (Lower a)
data Powerset u where
Powerset :: (s :⊆: u) -> Powerset u (Lower s)
powersetWholeset :: u ::∈: Powerset u
powersetEmpty :: Empty ::∈: Powerset u
powersetUnion :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∪: s2) ::∈: Powerset u
powersetInter :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∩: s2) ::∈: Powerset u
powersetMonotonic :: (u1 :⊆: u2) -> (s ::∈: Powerset u1) -> s ::∈: Powerset u2
powersetClosedDownwards :: (s1 :⊆: s2) -> (s2 ::∈: Powerset u) -> s1 ::∈: Powerset u
autosubset :: Fact (s :⊆: t) => s :⊆: t
autoequality :: Fact (s :==: t) => s :==: t
data ProofSet s where
ProofSet :: s x -> ProofSet s (s x)
data ExUniq1 p where
ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p
data V s where
V :: s x -> x -> V s
liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> V s -> V s -> Bool
liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> V s -> V s -> Ordering
liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> Int -> V s -> ShowS
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
show/hide Instances
scoerce :: (set1 :⊆: set2) -> (a :∈: set1) -> a :∈: set2Source
Coercion from subset to superset
type Subset = :⊆:Source
data set1 :==: set2 Source
Extensional equality of sets
Constructors
SetEq (set1 :⊆: set2) (set2 :⊆: set1)
show/hide Instances
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)
subsetRefl :: s :⊆: sSource
subsetTrans :: (s1 :⊆: s2) -> (s2 :⊆: s3) -> s1 :⊆: s3Source
setEqRefl :: s :==: sSource
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
elimUnion :: (a :∈: (s1 :∪: s2)) -> Either (a :∈: s1) (a :∈: s2)Source
type Union = :∪:Source
unionL :: s1 :⊆: (s1 :∪: s2)Source
unionR :: s2 :⊆: (s1 :∪: s2)Source
unionMinimal :: (s1 :⊆: t) -> (s2 :⊆: t) -> (s1 :∪: s2) :⊆: tSource
unionIdempotent :: (s :∪: s) :==: sSource
data s1 :∩: s2 whereSource
Binary intersection
Constructors
Inter :: (a :∈: s1) -> (a :∈: s2) -> (s1 :∩: s2) a
elimInter :: (a :∈: (s1 :∩: s2)) -> (a :∈: s1, a :∈: s2)Source
interFst :: (s1 :∩: s2) :⊆: s1Source
interSnd :: (s1 :∩: s2) :⊆: s2Source
type Inter = :∩:Source
interMaximal :: (t :⊆: s1) -> (t :⊆: s2) -> t :⊆: (s1 :∩: s2)Source
interIdempotent :: (s :∩: s) :==: sSource
data Unions fam whereSource
Union of a family
Constructors
Unions :: (Lower s :∈: fam) -> (a :∈: s) -> Unions fam a
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)
type DependentSum = ΣSource
data Inters fam whereSource
Intersection of a family
Constructors
Inters :: (forall s. (Lower s :∈: fam) -> a :∈: s) -> Inters fam a
elimInters :: Inters fam a -> (Lower s :∈: fam) -> s aSource
data Complement s whereSource
Complement
Constructors
Complement :: Not (a :∈: s) -> Complement s a
elimComplement :: (a :∈: Complement s) -> Not (a :∈: s)Source
type Disjoint s1 s2 = (s1 :∩: s2) :⊆: EmptySource
complContradiction :: Not (s a, Complement s a)Source
complEmpty :: Disjoint s (Complement s)Source
complMaximal :: Disjoint s t -> t :⊆: Complement sSource
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)
type Prod = :×:Source
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
elimEmpty :: Empty a -> bSource
emptySubset :: Empty :⊆: sSource
data Univ whereSource
Set of all types of kind *
Constructors
Univ :: Univ a
univSubset :: s :⊆: UnivSource
data FunctionType whereSource
Constructors
FunctionType :: FunctionType (a -> b)
show/hide Instances
functionType :: (a -> b) :∈: FunctionTypeSource
data KleisliType m whereSource
Constructors
KleisliType :: KleisliType m (a -> m b)
show/hide Instances
Fact ((a -> m b) :∈: KleisliType m)
kleisliType :: (a -> m b) :∈: KleisliType mSource
data CoKleisliType w whereSource
Constructors
CoKleisliType :: CoKleisliType w (w a -> b)
show/hide Instances
Fact ((w a -> b) :∈: CoKleisliType w)
coKleisliType :: (w a -> b) :∈: CoKleisliType wSource
Sets from common typeclasses
data ShowType whereSource
Constructors
ShowType :: Show a => ShowType a
show/hide Instances
getShow :: (a :∈: ShowType) -> a -> StringSource
Example application
data ReadType whereSource
Constructors
ReadType :: Read a => ReadType a
show/hide Instances
data EqType whereSource
Constructors
EqType :: Eq a => EqType a
show/hide Instances
Eq a => Fact (a :∈: EqType)
getEq :: (a :∈: EqType) -> a -> a -> BoolSource
data OrdType whereSource
Constructors
OrdType :: Ord a => OrdType a
show/hide Instances
getCompare :: (a :∈: OrdType) -> a -> a -> OrderingSource
data EnumType whereSource
Constructors
EnumType :: Enum a => EnumType a
show/hide Instances
data BoundedType whereSource
Constructors
BoundedType :: Bounded a => BoundedType a
show/hide Instances
data NumType whereSource
Constructors
NumType :: Num a => NumType a
show/hide Instances
data IntegralType whereSource
Constructors
IntegralType :: Integral a => IntegralType a
show/hide Instances
data MonoidType whereSource
Constructors
MonoidType :: Monoid a => MonoidType a
show/hide Instances
data FractionalType whereSource
Constructors
FractionalType :: Fractional a => FractionalType a
show/hide Instances
data TypeableType whereSource
Constructors
TypeableType :: Typeable a => TypeableType a
show/hide Instances
data DataType whereSource
Constructors
DataType :: Data a => DataType a
show/hide Instances
Kind (* -> *)
data FunctorType whereSource
Constructors
FunctorType :: Functor a => FunctorType (Lower a)
show/hide Instances
getFmap :: (Lower f :∈: FunctorType) -> (a -> b) -> f a -> f bSource
data MonadType whereSource
Constructors
MonadType :: Monad a => MonadType (Lower a)
show/hide Instances
data MonadPlusType whereSource
Constructors
MonadPlusType :: MonadPlus a => MonadPlusType (Lower a)
show/hide Instances
data ApplicativeType whereSource
Constructors
ApplicativeType :: Applicative a => ApplicativeType (Lower a)
show/hide Instances
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)
powersetWholeset :: u ::∈: Powerset uSource
powersetEmpty :: Empty ::∈: Powerset uSource
powersetUnion :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∪: s2) ::∈: Powerset uSource
powersetInter :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∩: s2) ::∈: Powerset uSource
powersetMonotonic :: (u1 :⊆: u2) -> (s ::∈: Powerset u1) -> s ::∈: Powerset u2Source
powersetClosedDownwards :: (s1 :⊆: s2) -> (s2 ::∈: Powerset u) -> s1 ::∈: Powerset uSource
Misc
autosubset :: Fact (s :⊆: t) => s :⊆: tSource
autoequality :: Fact (s :==: t) => s :==: tSource
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
show/hide 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
liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> V s -> V s -> OrderingSource
liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> Int -> V s -> ShowSSource
Produced by Haddock version 2.4.2