--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Type.Set
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------


{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS 
 #-}
{-# OPTIONS -fwarn-missing-signatures #-}


-- |
--
-- * 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@
--
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)
    

{-----------------------------                                  
emacs snippets for the funny characters (move behind the final parenthesis, press C-x C-e)

(progn
 (yas/define 'haskell-mode "subs" ":⊆:")
 (yas/define 'haskell-mode "union" ":∪:")
 (yas/define 'haskell-mode "inter" ":∩:")
 (yas/define 'haskell-mode "times" ":×:")
 (yas/define 'haskell-mode "elt" ":∈:")
 (yas/define 'haskell-mode "elt1" "::∈:")
 (yas/define 'haskell-mode "circ" ":○:")
 (yas/define 'haskell-mode "Sigma" "Σ")
 (yas/define 'haskell-mode "Pi" "Π")
 (yas/define 'haskell-mode "-->" ":~>:")
 (yas/define 'haskell-mode "--->" ":~~>:")
)

-----------------------------}




#include "../Defs.hs"
    
    
    


-- * Subsets, equality

type a :∈: set = set a

infix 4 :∈:


-- | Represents a proof that @set1@ is a subset of @set2@
data (set1 :: SET) :⊆: (set2 :: SET) where
       Subset :: (forall a. a :∈: set1 -> a :∈: set2) -> set1 :⊆: set2
                
                

-- | Coercion from subset to superset
scoerce :: (set1 :⊆: set2) -> a :∈: set1 -> a :∈: set2 
scoerce (Subset x) = x
                   
infix 4 :⊆:
    
type Subset = (:⊆:)

-- | Extensional equality of sets
data (set1 :: (SET)) :==: (set2 :: (SET)) = SetEq (set1 :⊆: set2) (set2 :⊆: set1)
                    
infix 4 :==:

instance Fact (set1 :⊆: set2 -> a :∈: set1 -> a :∈: set2) where auto = scoerce
                                                                     
-- | Coercion using a set equality
ecoerce :: (s1 :==: s2) -> a :∈: s1 -> a :∈: s2
ecoerce (SetEq p _) = scoerce p

-- | Coercion using a set equality (flipped)
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)
                                                   
                                                   
-- * Union, intersection, difference

-- | Binary union
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


-- | Binary intersection
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)
           
                     
-- | Union of a family
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)
                                                                    
                              

-- | Dependent sum
data Σ (fam :: SET) :: SET where
        Σ :: Lower s :∈: fam -> 
            a :∈: s -> 
            Σ fam (Lower s, a)

type DependentSum = Σ

                              
             

-- | Intersection of a family
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)
                 
-- | Complement
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))))
                 
                 
-- | Set difference
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)
                 
-- * Products

-- | Binary products
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
   
    
-- | Product is monotonic wrt. subset inclusion
prodMonotonic :: s1 :⊆: t1 
              -> s2 :⊆: t2 
              -> s1 :×: s2 :⊆: t1 :×: t2;

prodMonotonic p1 p2 = Subset (\(q1 :×: q2) -> scoerce p1 q1 :×: scoerce p2 q2)
                      

-- * Particular sets
-- | Empty set (barring cheating with 'undefined')
data Empty :: SET where 
             Empty :: (forall b. b) -> Empty a

elimEmpty :: Empty a -> b
elimEmpty (Empty x) = x
    
emptySubset :: (Empty :⊆: s)
emptySubset = Subset elimEmpty
    
-- | Set of /all/ types of kind *
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
            
-- *** Sets from common typeclasses

-- (yas/define 'haskell-mode "class-set" "data $1Type :: SET where $1Type :: $1 a => $1Type a\ninstance $1 a => Fact (a :∈: $1Type) where auto = $1Type\n$0")



-- (yas/define 'haskell-mode "class-set1" "data $1Type :: SET where $1Type :: $1 a => $1Type (Lower a)\ninstance $1 a => Fact (Lower a :∈: $1Type) where auto = $1Type\n$0")

data ShowType :: SET where ShowType :: Show a => ShowType a
instance Show a => Fact (a :∈: ShowType) where auto = ShowType
                                                     
-- data ReflectShow a = ReflectShow (ShowType a) a
-- instance Show (ReflectShow a) where show (ReflectShow ShowType a) = show a

                                     
-- | Example application
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


-- ** Kind (* -> *)

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




-- * Powerset

-- | Membership of a set in a set representing a set of sets
type a ::∈: set = set (Lower a)

infix 4 ::∈:

-- (yas/define 'haskell-mode "k2" "SET -> *")



-- | Powerset
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))
                                 
-- * Misc                                  
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)
        

-- instance ( Fact1 (s1 :⊆: s2)
--          , Fact1 (s2 :⊆: s3))

--     =>      Fact (s1 :⊆: s3) where
        
--         auto = subsetTrans auto auto

-- * Unique existence of sets

-- | Unique existence, unlowered
data ExUniq1 (p :: SET -> *) where
    ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p



               
-- * From sets to the value level




-- | @V s@ is the sum of all types @x@ such that @s x@ is provable.
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
                                  
                     ])