--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--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 :: forall s. 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
                                     
-- | 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 :: forall x. 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
                                  
                     ])