type-settheory-0.1.2: Type-level sets and functions expressed as types Source code Contents Index

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 a Source

data set1 :⊆: set2 where Source

Represents a proof that set1 is a subset of set2 Constructors Subset :: (forall a. (a :∈: set1) -> a :∈: set2) -> set1 :⊆: set2 Instances Fact (Disjoint s (Complement s)) (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 :∈: set2 Source

Coercion from subset to superset

type Subset = :⊆: Source

data set1 :==: set2 Source

Extensional equality of sets Constructors SetEq (set1 :⊆: set2) (set2 :⊆: set1) Instances Fact (s :==: s) Fact (Inv (Id dom) :==: Id dom)

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

Coercion using a set equality

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

Coercion using a set equality (flipped)

subsetRefl :: s :⊆: s Source

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

setEqRefl :: s :==: s Source

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

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

type Singleton a = :=: a Source

Union, intersection, difference

data s1 :∪: s2 where Source

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) :⊆: t Source

unionIdempotent :: (s :∪: s) :==: s Source

data s1 :∩: s2 where Source

Binary intersection Constructors Inter :: (a :∈: s1) -> (a :∈: s2) -> (s1 :∩: s2) a

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

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

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

type Inter = :∩: Source

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

interIdempotent :: (s :∩: s) :==: s Source

data Unions fam where Source

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) -> r Source

data Σ fam where Source

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

type DependentSum = Σ Source

data Inters fam where Source

Intersection of a family Constructors Inters :: (forall s. (Lower s :∈: fam) -> a :∈: s) -> Inters fam a

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

data Complement s where Source

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

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

type Disjoint s1 s2 = (s1 :∩: s2) :⊆: Empty Source

complContradiction :: Not (s a, Complement s a) Source

complEmpty :: Disjoint s (Complement s) Source

complMaximal :: Disjoint s t -> t :⊆: Complement s Source

data Diff s t where Source

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 where Source

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

type Prod = :×: Source

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

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

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

Product is monotonic wrt. subset inclusion

Particular sets

data Empty where Source

Empty set (barring cheating with undefined) Constructors Empty :: (forall b. b) -> Empty a

elimEmpty :: Empty a -> b Source

emptySubset :: Empty :⊆: s Source

data Univ where Source

Set of all types of kind * Constructors Univ :: Univ a

univSubset :: s :⊆: Univ Source

data FunctionType where Source

Constructors FunctionType :: FunctionType (a -> b) Instances Fact ((a -> b) :∈: FunctionType)

functionType :: (a -> b) :∈: FunctionType Source

data KleisliType m where Source

Constructors KleisliType :: KleisliType m (a -> m b) Instances Fact ((a -> m b) :∈: KleisliType m)

kleisliType :: (a -> m b) :∈: KleisliType m Source

data CoKleisliType w where Source

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

coKleisliType :: (w a -> b) :∈: CoKleisliType w Source

Sets from common typeclasses

data ShowType where Source

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

getShow :: (a :∈: ShowType) -> a -> String Source

Example application

data ReadType where Source

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

data EqType where Source

Constructors EqType :: Eq a => EqType a Instances Eq a => Fact (a :∈: EqType)

getEq :: (a :∈: EqType) -> a -> a -> Bool Source

data OrdType where Source

Constructors OrdType :: Ord a => OrdType a Instances SMonad OrdType Set SApplicative OrdType Set SFunctor OrdType Set Ord a => Fact (a :∈: OrdType)

getCompare :: (a :∈: OrdType) -> a -> a -> Ordering Source

data EnumType where Source

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

data BoundedType where Source

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

data NumType where Source

Constructors NumType :: Num a => NumType a Instances Num a => Fact (a :∈: NumType)

data IntegralType where Source

Constructors IntegralType :: Integral a => IntegralType a Instances Integral a => Fact (a :∈: IntegralType)

data MonoidType where Source

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

data FractionalType where Source

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

data TypeableType where Source

Constructors TypeableType :: Typeable a => TypeableType a Instances Typeable a => Fact (a :∈: TypeableType)

data DataType where Source

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

Kind (* -> *)

data FunctorType where Source

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

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

data MonadType where Source

Constructors MonadType :: Monad a => MonadType (Lower a) Instances Monad a => Fact (Lower a :∈: MonadType)

data MonadPlusType where Source

Constructors MonadPlusType :: MonadPlus a => MonadPlusType (Lower a) Instances MonadPlus a => Fact (Lower a :∈: MonadPlusType)

data ApplicativeType where Source

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 where Source

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

powersetWholeset :: u ::∈: Powerset u Source

powersetEmpty :: Empty ::∈: Powerset u Source

powersetUnion :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∪: s2) ::∈: Powerset u Source

powersetInter :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∩: s2) ::∈: Powerset u Source

powersetMonotonic :: (u1 :⊆: u2) -> (s ::∈: Powerset u1) -> s ::∈: Powerset u2 Source

powersetClosedDownwards :: (s1 :⊆: s2) -> (s2 ::∈: Powerset u) -> s1 ::∈: Powerset u Source

Misc

autosubset :: Fact (s :⊆: t) => s :⊆: t Source

autoequality :: Fact (s :==: t) => s :==: t Source

data ProofSet s where Source

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

Unique existence of sets

data ExUniq1 p where Source

Unique existence, unlowered Constructors ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p

From sets to the value level

data V s where Source

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 -> Bool Source

liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> V s -> V s -> Ordering Source

liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> Int -> V s -> ShowS Source

Produced by Haddock version 2.4.2