module Type.Set where
import Data.Type.Equality
import Type.Logic
import Type.Dummies
import Data.Monoid
import Control.Monad
import Helper
import Control.Applicative
import Data.Typeable.Extras
import Data.Data hiding (DataType)
#include "../Defs.hs"
type a :∈: set = set a
infix 4 :∈:
data (set1 :: SET) :⊆: (set2 :: SET) where
Subset :: (forall a. a :∈: set1 -> a :∈: set2) -> set1 :⊆: set2
scoerce :: (set1 :⊆: set2) -> a :∈: set1 -> a :∈: set2
scoerce (Subset x) = x
infix 4 :⊆:
type Subset = (:⊆:)
data (set1 :: (SET)) :==: (set2 :: (SET)) = SetEq (set1 :⊆: set2) (set2 :⊆: set1)
infix 4 :==:
instance Fact (set1 :⊆: set2 -> a :∈: set1 -> a :∈: set2) where auto = scoerce
ecoerce :: (s1 :==: s2) -> a :∈: s1 -> a :∈: s2
ecoerce (SetEq p _) = scoerce p
ecoerceFlip :: (s1 :==: s2) -> a :∈: s2 -> a :∈: s1
ecoerceFlip (SetEq _ q) = scoerce q
subsetRefl :: s :⊆: s
subsetRefl = Subset id
subsetTrans :: (s1 :⊆: s2 -> s2 :⊆: s3 -> s1 :⊆: s3);
subsetTrans p1 p2 = Subset (scoerce p2 . scoerce p1)
setEqRefl :: s :==: s;
setEqRefl = SetEq subsetRefl subsetRefl
setEqSym :: s1 :==: s2 -> s2 :==: s1;
setEqSym (SetEq p1 p2) = SetEq p2 p1
setEqTrans :: (s1 :==: s2 -> s2 :==: s3 -> s1 :==: s3);
setEqTrans (SetEq p1 p2) (SetEq q1 q2) = SetEq
(p1 `subsetTrans` q1)
(q2 `subsetTrans` p2)
type Singleton a = (:=:) a
instance Fact (Singleton a a) where auto = Refl
instance (Fact (a :∈: set)) => (Fact (Singleton a :⊆: set)) where
auto = Subset (\Refl -> auto)
data (s1 :: SET) :∪: (s2 :: SET) :: SET where
Union :: Either (a :∈: s1) (a :∈: s2) -> (s1 :∪: s2) a
elimUnion :: a :∈: (s1 :∪: s2) -> Either (a :∈: s1) (a :∈: s2)
elimUnion (Union x) = x
infixr 5 :∪:
type Union = (:∪:)
unionL :: s1 :⊆: (s1 :∪: s2)
unionL = Subset (Union . Left)
unionR :: s2 :⊆: (s1 :∪: s2)
unionR = Subset (Union . Right)
unionMinimal :: s1 :⊆: t -> s2 :⊆: t -> (s1 :∪: s2) :⊆: t
unionMinimal p1 p2 = Subset (\(Union q) -> case q of
Left q1 -> scoerce p1 q1
Right q2 -> scoerce p2 q2)
unionIdempotent :: s :∪: s :==: s
unionIdempotent = SetEq (unionMinimal auto auto) unionL
instance (Fact (s1 :⊆: t), Fact (s2 :⊆: t)) => Fact (s1 :∪: s2 :⊆: t) where
auto = unionMinimal auto auto
data ((s1 :: SET) :∩: (s2 :: SET)) :: SET where
Inter :: a :∈: s1 -> a :∈: s2 -> (s1 :∩: s2) a
elimInter :: a :∈: (s1 :∩: s2) -> (a :∈: s1, a :∈: s2)
elimInter (Inter x y) = (x,y)
interFst :: (s1 :∩: s2) :⊆: s1
interFst = Subset (fst . elimInter)
interSnd :: (s1 :∩: s2) :⊆: s2
interSnd = Subset (snd . elimInter)
infixr 6 :∩:
type Inter = (:∩:)
interMaximal :: (t :⊆: s1 -> t :⊆: s2 -> t :⊆: (s1 :∩: s2))
interMaximal p1 p2 = Subset (\q -> Inter (scoerce p1 q) (scoerce p2 q))
instance (Fact (t :⊆: s1), Fact (t :⊆: s2)) => Fact (t :⊆: (s1 :∩: s2)) where
auto = interMaximal auto auto
interIdempotent :: s :∩: s :==: s
interIdempotent = SetEq interFst (interMaximal auto auto)
data Unions (fam :: SET) :: SET where
Unions :: Lower s :∈: fam -> a :∈: s -> Unions fam a
elimUnions :: Unions fam a -> (forall s. Lower s :∈: fam -> a :∈: s -> r) -> r
elimUnions (Unions p1 p2) k = k p1 p2
instance Fact (Lower s :∈: fam -> s :⊆: (Unions fam)) where auto p = Subset (Unions p)
data Σ (fam :: SET) :: SET where
Σ :: Lower s :∈: fam ->
a :∈: s ->
Σ fam (Lower s, a)
type DependentSum = Σ
data Inters (fam :: SET) :: SET where
Inters :: (forall s. (Lower s) :∈: fam -> a :∈: s) -> Inters fam a
elimInters :: Inters fam a -> (Lower s) :∈: fam -> s a
elimInters (Inters x) = x
instance Fact ((Lower s) :∈: fam -> (Inters fam) :⊆: s ) where
auto p = Subset (($ p) . elimInters)
data Complement (s :: SET) :: SET where
Complement :: Not (a :∈: s) -> Complement s a
elimComplement :: a :∈: Complement s -> Not (a :∈: s)
elimComplement (Complement x) = x
type Disjoint s1 s2 = (s1 :∩: s2) :⊆: Empty
complContradiction :: Not (s a, Complement s a)
complContradiction (p, Complement q) = q p
complEmpty :: Disjoint s (Complement s)
complEmpty = Subset (elimFalsity . complContradiction . elimInter)
complMaximal :: Disjoint s t -> (t :⊆: Complement s)
complMaximal p = Subset (\q -> Complement (\r -> elimEmpty (p `scoerce` (Inter r q))))
data Diff (s :: SET) (t :: SET) :: SET where
Diff :: a :∈: s -> Not (a :∈: t) -> Diff s t a
elimDiff :: a :∈: Diff s t -> (a :∈: s, Not (a :∈: t))
elimDiff (Diff x y) = (x,y)
data (s1 :: SET) :×: (s2 :: SET) :: SET where
(:×:) :: a :∈: s1 -> b :∈: s2 -> (s1 :×: s2) (a, b)
infixr 6 :×:
type Prod = (:×:)
fstPrf :: (a, b) :∈: (s1 :×: s2) -> a :∈: s1;
fstPrf (p :×: _) = p
sndPrf :: (a, b) :∈: (s1 :×: s2) -> b :∈: s2;
sndPrf (_ :×: q) = q
prodMonotonic :: s1 :⊆: t1
-> s2 :⊆: t2
-> s1 :×: s2 :⊆: t1 :×: t2;
prodMonotonic p1 p2 = Subset (\(q1 :×: q2) -> scoerce p1 q1 :×: scoerce p2 q2)
data Empty :: SET where
Empty :: (forall b. b) -> Empty a
elimEmpty :: Empty a -> b
elimEmpty (Empty x) = x
emptySubset :: (Empty :⊆: s)
emptySubset = Subset elimEmpty
data Univ :: SET where Univ :: Univ a
univSubset :: (s :⊆: Univ)
univSubset = Subset (const Univ)
data FunctionType :: SET where
FunctionType :: FunctionType (a -> b)
functionType :: (a -> b) :∈: FunctionType
functionType = FunctionType
data KleisliType m :: SET where
KleisliType :: KleisliType m (a -> m b)
kleisliType :: (a -> m b) :∈: (KleisliType m)
kleisliType = KleisliType
data CoKleisliType w :: SET where
CoKleisliType :: CoKleisliType w (w a -> b)
coKleisliType :: (w a -> b) :∈: (CoKleisliType w)
coKleisliType = CoKleisliType
data ShowType :: SET where ShowType :: Show a => ShowType a
instance Show a => Fact (a :∈: ShowType) where auto = ShowType
getShow :: a :∈: ShowType -> a -> String
getShow ShowType = show
data ReadType :: SET where ReadType :: Read a => ReadType a
instance Read a => Fact (a :∈: ReadType) where auto = ReadType
data EqType :: SET where EqType :: Eq a => EqType a
instance Eq a => Fact (a :∈: EqType) where auto = EqType
getEq :: a :∈: EqType -> a -> a -> Bool
getEq EqType = (==)
data OrdType :: SET where OrdType :: Ord a => OrdType a
instance Ord a => Fact (a :∈: OrdType) where auto = OrdType
getCompare :: a :∈: OrdType -> a -> a -> Ordering
getCompare OrdType = compare
data EnumType :: SET where EnumType :: Enum a => EnumType a
instance Enum a => Fact (a :∈: EnumType) where auto = EnumType
data BoundedType :: SET where BoundedType :: Bounded a => BoundedType a
instance Bounded a => Fact (a :∈: BoundedType) where auto = BoundedType
data NumType :: SET where NumType :: Num a => NumType a
instance Num a => Fact (a :∈: NumType) where auto = NumType
data IntegralType :: SET where IntegralType :: Integral a => IntegralType a
instance Integral a => Fact (a :∈: IntegralType) where auto = IntegralType
data MonoidType :: SET where MonoidType :: Monoid a => MonoidType a
instance Monoid a => Fact (a :∈: MonoidType) where auto = MonoidType
data FractionalType :: SET where FractionalType :: Fractional a => FractionalType a
instance Fractional a => Fact (a :∈: FractionalType) where auto = FractionalType
data TypeableType :: SET where TypeableType :: Typeable a => TypeableType a
instance Typeable a => Fact (a :∈: TypeableType) where auto = TypeableType
data DataType :: SET where DataType :: Data a => DataType a
instance Data a => Fact (a :∈: DataType) where auto = DataType
data FunctorType :: SET where FunctorType :: Functor a => FunctorType (Lower a)
instance Functor a => Fact (Lower a :∈: FunctorType) where auto = FunctorType
getFmap :: Lower f :∈: FunctorType -> (a -> b) -> (f a -> f b)
getFmap FunctorType = fmap
data MonadType :: SET where MonadType :: Monad a => MonadType (Lower a)
instance Monad a => Fact (Lower a :∈: MonadType) where auto = MonadType
data MonadPlusType :: SET where MonadPlusType :: MonadPlus a => MonadPlusType (Lower a)
instance MonadPlus a => Fact (Lower a :∈: MonadPlusType) where auto = MonadPlusType
data ApplicativeType :: SET where ApplicativeType :: Applicative a => ApplicativeType (Lower a)
instance Applicative a => Fact (Lower a :∈: ApplicativeType) where auto = ApplicativeType
type a ::∈: set = set (Lower a)
infix 4 ::∈:
data (Powerset (u :: SET)) :: SET where
Powerset :: s :⊆: u -> Powerset u (Lower s)
powersetWholeset :: u ::∈: Powerset u
powersetWholeset = Powerset subsetRefl
powersetEmpty :: Empty ::∈: Powerset u
powersetEmpty = Powerset emptySubset
powersetUnion :: s1 ::∈: Powerset u -> s2 ::∈: Powerset u -> (s1 :∪: s2) ::∈: Powerset u
powersetUnion (Powerset p1) (Powerset p2) = Powerset (unionMinimal p1 p2)
powersetInter :: s1 ::∈: Powerset u -> s2 ::∈: Powerset u -> (s1 :∩: s2) ::∈: Powerset u
powersetInter (Powerset p1) (Powerset _) = Powerset (subsetTrans auto p1)
powersetMonotonic :: (u1 :⊆: u2) -> s ::∈: Powerset u1 -> s ::∈: Powerset u2
powersetMonotonic p (Powerset q) = Powerset (Subset (scoerce p . scoerce q))
powersetClosedDownwards :: (s1 :⊆: s2) -> s2 ::∈: Powerset u -> s1 ::∈: Powerset u
powersetClosedDownwards p (Powerset q) = Powerset (Subset (scoerce q . scoerce p))
autosubset :: Fact (s :⊆: t) => s :⊆: t
autosubset = auto
autoequality :: Fact (s :==: t) => s :==: t
autoequality = auto
data ProofSet (s :: SET) :: SET where
ProofSet :: s x -> ProofSet s (s x)
#define SUBCLASS(X,Y)\
instance Fact (X :⊆: Y) where\
auto = Subset (\ X -> Y )
SUBCLASS(OrdType,EqType)
SUBCLASS(NumType,EqType)
SUBCLASS(IntegralType,NumType)
SUBCLASS(MonadPlusType,MonadType)
data ExUniq1 (p :: SET -> *) where
ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p
data V (s :: SET) where
V :: s x -> x -> V s
liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> (V s -> V s -> Bool)
liftEq s s2 (V px x) (V py y) =
case ( s `scoerce` px
, s `scoerce` py
, s2 `scoerce` px
, s2 `scoerce` py) of
(EqType, EqType, TypeableType, TypeableType) -> dynEq x y
instance ( ( Fact (s :⊆: EqType)
, Fact (s :⊆: TypeableType) )
=> Eq (V s) )
where
(==) = liftEq auto auto
liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> (V s -> V s -> Ordering)
liftCompare s s2 (V px x) (V py y) =
case ( s `scoerce` px
, s `scoerce` py
, s2 `scoerce` px
, s2 `scoerce` py) of
(OrdType, OrdType, TypeableType, TypeableType) -> dynCompare x y
instance ( ( Fact (s :⊆: OrdType)
, Fact (s :⊆: TypeableType)
, Eq (V s) )
=> Ord (V s) )
where
compare = liftCompare auto auto
liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> (Int -> V s -> ShowS)
liftShowsPrec s s2 prec (V px x) =
case ( s `scoerce` px
, s2 `scoerce` px ) of
(ShowType, TypeableType) ->
showParen (prec > 10)
(showString "V " .
showString "<< proof of " . shows (typeOf px) .
showString " >> " .
showsPrec 11 x)
$(lemmata ''Fact
[ 'fstPrf,'sndPrf,'prodMonotonic
, 'complEmpty, 'complContradiction
, 'elimEmpty, 'emptySubset
, 'ecoerce,'ecoerceFlip
, 'subsetRefl
, 'subsetTrans,'setEqRefl,'setEqSym,'setEqTrans
, 'univSubset, 'complMaximal
, 'powersetClosedDownwards
, 'powersetMonotonic
, 'interMaximal, 'unionMinimal
, 'functionType, 'kleisliType, 'coKleisliType
, 'interFst, 'interSnd
,'unionL,'unionR
])