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 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 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
Constructors
Instances
 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
Constructors
Instances
Constructors
Instances
 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