{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Universe (
Elem, In, Universe(..)
, Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)
, CompElem(..), SumElem(..)
, All, WitAll(..), NotAll
, Any, WitAny(..), None
, Null, NotNull
, IsJust, IsNothing, IsRight, IsLeft
, decideAny, decideAll, genAllA, genAll, igenAll
, foldMapUni, ifoldMapUni, index, pickElem
, Sing (SComp, SInL, SInR)
, (:.:)(..), sGetComp, GetComp
, allComp, compAll, anyComp, compAny
, (:+:)(..)
, anySumL, anySumR, sumLAny, sumRAny
, allSumL, allSumR, sumLAll, sumRAll
, ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1
) where
import Control.Applicative
import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Proxy
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude hiding (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not)
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Prelude hiding (any, all)
import qualified Data.Singletons.Prelude.List.NonEmpty as NE
#if MIN_VERSION_singletons(2,5,0)
import Data.Singletons.Prelude.Identity
#else
import Data.Singletons.TH
genSingletons [''Identity]
#endif
type family Elem (f :: Type -> Type) :: f k -> k -> Type
data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
type instance Apply (ElemSym0 f) as = ElemSym1 f as
type instance Apply (ElemSym1 f as) a = Elem f as a
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
data WitAny f :: (k ~> Type) -> f k -> Type where
WitAny :: Elem f as a -> p @@ a -> WitAny f p as
data Any f :: Predicate k -> Predicate (f k)
type instance Apply (Any f p) as = WitAny f p as
newtype WitAll f p (as :: f k) = WitAll { runWitAll :: forall a. Elem f as a -> p @@ a }
data All f :: Predicate k -> Predicate (f k)
type instance Apply (All f p) as = WitAll f p as
instance (Universe f, Decidable p) => Decidable (Any f p) where
decide = decideAny @f @_ @p $ decide @p
instance (Universe f, Decidable p) => Decidable (All f p) where
decide = decideAll @f @_ @p $ decide @p
instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where
instance Provable p => Provable (NotNull f ==> Any f p) where
prove _ (WitAny i s) = WitAny i (prove @p s)
instance (Universe f, Provable p) => Provable (All f p) where
prove xs = WitAll $ \i -> prove @p (index i xs)
instance Universe f => TFunctor (Any f) where
tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)
instance Universe f => TFunctor (All f) where
tmap f xs a = WitAll $ \i -> f (index i xs) (runWitAll a i)
instance Universe f => DFunctor (All f) where
dmap f xs a = idecideAll (\i x -> f x (runWitAll a i)) xs
class Universe (f :: Type -> Type) where
idecideAny
:: forall k (p :: k ~> Type) (as :: f k). ()
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> (Sing as -> Decision (Any f p @@ as))
idecideAll
:: forall k (p :: k ~> Type) (as :: f k). ()
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> (Sing as -> Decision (All f p @@ as))
igenAllA
:: forall k (p :: k ~> Type) (as :: f k) h. Applicative h
=> (forall a. Elem f as a -> Sing a -> h (p @@ a))
-> (Sing as -> h (All f p @@ as))
type Null f = (None f Evident :: Predicate (f k))
type NotNull f = (Any f Evident :: Predicate (f k))
type None f p = (Not (Any f p) :: Predicate (f k))
type NotAll f p = (Not (All f p) :: Predicate (f k))
decideAny
:: forall f k (p :: k ~> Type). Universe f
=> Decide p
-> Decide (Any f p)
decideAny f = idecideAny (const f)
decideAll
:: forall f k (p :: k ~> Type). Universe f
=> Decide p
-> Decide (All f p)
decideAll f = idecideAll (const f)
genAllA
:: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
=> (forall a. Sing a -> h (p @@ a))
-> (Sing as -> h (All f p @@ as))
genAllA f = igenAllA (const f)
igenAll
:: forall f k (p :: k ~> Type) (as :: f k). Universe f
=> (forall a. Elem f as a -> Sing a -> p @@ a)
-> (Sing as -> All f p @@ as)
igenAll f = runIdentity . igenAllA (\i -> Identity . f i)
genAll
:: forall f k (p :: k ~> Type). Universe f
=> Prove p
-> Prove (All f p)
genAll f = igenAll (const f)
index
:: forall f as a. Universe f
=> Elem f as a
-> Sing as
-> Sing a
index i = (`runWitAll` i) . splitSing
splitSing
:: forall f k (as :: f k). Universe f
=> Sing as
-> All f (TyPred Sing) @@ as
splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)
pickElem
:: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)
=> Decision (Elem f as a)
pickElem = mapDecision (\case WitAny i Refl -> i)
(\case i -> WitAny i Refl)
. decide @(Any f (TyPred ((:~:) a)))
$ sing
ifoldMapUni
:: forall f k (as :: f k) m. (Universe f, Monoid m)
=> (forall a. Elem f as a -> Sing a -> m)
-> Sing as
-> m
ifoldMapUni f = getConst . igenAllA (\i -> Const . f i)
foldMapUni
:: forall f k (as :: f k) m. (Universe f, Monoid m)
=> (forall (a :: k). Sing a -> m)
-> Sing as
-> m
foldMapUni f = ifoldMapUni (const f)
data Index :: [k] -> k -> Type where
IZ :: Index (a ': as) a
IS :: Index bs a -> Index (b ': bs) a
deriving instance Show (Index as a)
instance (SingI (as :: [k]), SDecide k) => Decidable (TyPred (Index as)) where
decide x = withSingI x $ pickElem
type instance Elem [] = Index
instance Universe [] where
idecideAny
:: forall k (p :: k ~> Type) (as :: [k]). ()
=> (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (Any [] p @@ as)
idecideAny f = \case
SNil -> Disproved $ \case
WitAny i _ -> case i of {}
x `SCons` xs -> case f IZ x of
Proved p -> Proved $ WitAny IZ p
Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of
Proved (WitAny i p) -> Proved $ WitAny (IS i) p
Disproved vs -> Disproved $ \case
WitAny IZ p -> v p
WitAny (IS i) p -> vs (WitAny i p)
idecideAll
:: forall k (p :: k ~> Type) (as :: [k]). ()
=> (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (All [] p @@ as)
idecideAll f = \case
SNil -> Proved $ WitAll $ \case {}
x `SCons` xs -> case f IZ x of
Proved p -> case idecideAll @[] @_ @p (f . IS) xs of
Proved a -> Proved $ WitAll $ \case
IZ -> p
IS i -> runWitAll a i
Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)
Disproved v -> Disproved $ \a -> v $ runWitAll a IZ
igenAllA
:: forall k (p :: k ~> Type) (as :: [k]) h. Applicative h
=> (forall a. Elem [] as a -> Sing a -> h (p @@ a))
-> Sing as
-> h (All [] p @@ as)
igenAllA f = \case
SNil -> pure $ WitAll $ \case {}
x `SCons` xs -> go <$> f IZ x <*> igenAllA (f . IS) xs
where
go :: p @@ b -> All [] p @@ bs -> All [] p @@ (b ': bs)
go p a = WitAll $ \case
IZ -> p
IS i -> runWitAll a i
data IJust :: Maybe k -> k -> Type where
IJust :: IJust ('Just a) a
deriving instance Show (IJust as a)
instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where
decide x = withSingI x $ pickElem
type instance Elem Maybe = IJust
type IsJust = (NotNull Maybe :: Predicate (Maybe k))
type IsNothing = (Null Maybe :: Predicate (Maybe k))
instance Universe Maybe where
idecideAny f = \case
SNothing -> Disproved $ \case WitAny i _ -> case i of {}
SJust x -> case f IJust x of
Proved p -> Proved $ WitAny IJust p
Disproved v -> Disproved $ \case
WitAny IJust p -> v p
idecideAll f = \case
SNothing -> Proved $ WitAll $ \case {}
SJust x -> case f IJust x of
Proved p -> Proved $ WitAll $ \case IJust -> p
Disproved v -> Disproved $ \a -> v $ runWitAll a IJust
igenAllA f = \case
SNothing -> pure $ WitAll $ \case {}
SJust x -> (\p -> WitAll $ \case IJust -> p) <$> f IJust x
data IRight :: Either j k -> k -> Type where
IRight :: IRight ('Right a) a
deriving instance Show (IRight as a)
instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where
decide x = withSingI x $ pickElem
type instance Elem (Either j) = IRight
type IsRight = (NotNull (Either j) :: Predicate (Either j k))
type IsLeft = (Null (Either j) :: Predicate (Either j k))
instance Universe (Either j) where
idecideAny f = \case
SLeft _ -> Disproved $ \case WitAny i _ -> case i of {}
SRight x -> case f IRight x of
Proved p -> Proved $ WitAny IRight p
Disproved v -> Disproved $ \case
WitAny IRight p -> v p
idecideAll f = \case
SLeft _ -> Proved $ WitAll $ \case {}
SRight x -> case f IRight x of
Proved p -> Proved $ WitAll $ \case IRight -> p
Disproved v -> Disproved $ \a -> v $ runWitAll a IRight
igenAllA f = \case
SLeft _ -> pure $ WitAll $ \case {}
SRight x -> (\p -> WitAll $ \case IRight -> p) <$> f IRight x
data NEIndex :: NonEmpty k -> k -> Type where
NEHead :: NEIndex (a ':| as) a
NETail :: Index as a -> NEIndex (b ':| as) a
deriving instance Show (NEIndex as a)
instance (SingI (as :: NonEmpty k), SDecide k) => Decidable (TyPred (NEIndex as)) where
decide x = withSingI x $ pickElem
type instance Elem NonEmpty = NEIndex
instance Universe NonEmpty where
idecideAny
:: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
=> (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (Any NonEmpty p @@ as)
idecideAny f (x NE.:%| xs) = case f NEHead x of
Proved p -> Proved $ WitAny NEHead p
Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of
Proved (WitAny i p) -> Proved $ WitAny (NETail i) p
Disproved vs -> Disproved $ \case
WitAny i p -> case i of
NEHead -> v p
NETail i' -> vs (WitAny i' p)
idecideAll
:: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
=> (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (All NonEmpty p @@ as)
idecideAll f (x NE.:%| xs) = case f NEHead x of
Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of
Proved ps -> Proved $ WitAll $ \case
NEHead -> p
NETail i -> runWitAll ps i
Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)
Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead
igenAllA
:: forall k (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h
=> (forall a. Elem NonEmpty as a -> Sing a -> h (p @@ a))
-> Sing as
-> h (All NonEmpty p @@ as)
igenAllA f (x NE.:%| xs) = go <$> f NEHead x <*> igenAllA @[] @_ @p (f . NETail) xs
where
go :: p @@ b -> All [] p @@ bs -> All NonEmpty p @@ (b ':| bs)
go p ps = WitAll $ \case
NEHead -> p
NETail i -> runWitAll ps i
data ISnd :: (j, k) -> k -> Type where
ISnd :: ISnd '(a, b) b
deriving instance Show (ISnd as a)
instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where
decide x = withSingI x $ pickElem
type instance Elem ((,) j) = ISnd
instance Universe ((,) j) where
idecideAny f (STuple2 _ x) = case f ISnd x of
Proved p -> Proved $ WitAny ISnd p
Disproved v -> Disproved $ \case WitAny ISnd p -> v p
idecideAll f (STuple2 _ x) = case f ISnd x of
Proved p -> Proved $ WitAll $ \case ISnd -> p
Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd
igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x
data IProxy :: Proxy k -> k -> Type
deriving instance Show (IProxy 'Proxy a)
instance Provable (Not (TyPred (IProxy 'Proxy))) where
prove _ = \case {}
type instance Elem Proxy = IProxy
instance Universe Proxy where
idecideAny _ _ = Disproved $ \case
WitAny i _ -> case i of {}
idecideAll _ _ = Proved $ WitAll $ \case {}
igenAllA _ _ = pure $ WitAll $ \case {}
data IIdentity :: Identity k -> k -> Type where
IId :: IIdentity ('Identity x) x
deriving instance Show (IIdentity as a)
instance (SingI (as :: Identity k), SDecide k) => Decidable (TyPred (IIdentity as)) where
decide x = withSingI x $ pickElem
type instance Elem Identity = IIdentity
instance Universe Identity where
idecideAny f (SIdentity x) = mapDecision (WitAny IId)
(\case WitAny IId p -> p)
$ f IId x
idecideAll f (SIdentity x) = mapDecision (\p -> WitAll $ \case IId -> p)
(`runWitAll` IId)
$ f IId x
igenAllA f (SIdentity x) = (\p -> WitAll $ \case IId -> p) <$> f IId x
data (f :.: g) a = Comp { getComp :: f (g a) }
deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
deriving instance (Traversable f, Traversable g) => Traversable (f :.: g)
data instance Sing (k :: (f :.: g) a) where
SComp :: Sing x -> Sing ('Comp x)
type family GetComp c where
GetComp ('Comp a) = a
sGetComp :: Sing a -> Sing (GetComp a)
sGetComp (SComp x) = x
instance SingI ass => SingI ('Comp ass) where
sing = SComp sing
data GetCompSym0 :: (f :.: g) k ~> f (g k)
type instance Apply GetCompSym0 ('Comp ass) = ass
type GetCompSym1 a = GetComp a
data CompElem :: (f :.: g) k -> k -> Type where
(:?) :: Elem f ass as
-> Elem g as a
-> CompElem ('Comp ass) a
type instance Elem (f :.: g) = CompElem
instance (Universe f, Universe g) => Universe (f :.: g) where
idecideAny
:: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
=> (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
-> Sing ass
-> Decision (Any (f :.: g) p @@ ass)
idecideAny f (SComp xss)
= mapDecision anyComp compAny
. idecideAny @f @_ @(Any g p) go
$ xss
where
go :: Elem f (GetComp ass) as
-> Sing as
-> Decision (Any g p @@ as)
go i = idecideAny $ \j -> f (i :? j)
idecideAll
:: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
=> (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
-> Sing ass
-> Decision (All (f :.: g) p @@ ass)
idecideAll f (SComp xss)
= mapDecision allComp compAll
. idecideAll @f @_ @(All g p) go
$ xss
where
go :: Elem f (GetComp ass) as
-> Sing as
-> Decision (All g p @@ as)
go i = idecideAll $ \j -> f (i :? j)
igenAllA
:: forall k (p :: k ~> Type) (ass :: (f :.: g) k) h. Applicative h
=> (forall a. Elem (f :.: g) ass a -> Sing a -> h (p @@ a))
-> Sing ass
-> h (All (f :.: g) p @@ ass)
igenAllA f (SComp ass) = allComp <$> igenAllA @f @_ @(All g p) go ass
where
go :: Elem f (GetComp ass) (as :: g k)
-> Sing as
-> h (All g p @@ as)
go i = igenAllA $ \j -> f (i :? j)
anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p
compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)
allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j
compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)
data (f :+: g) a = InL (f a)
| InR (g a)
deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
deriving instance (Traversable f, Traversable g) => Traversable (f :+: g)
data instance Sing (k :: (f :+: g) a) where
SInL :: Sing x -> Sing ('InL x)
SInR :: Sing y -> Sing ('InR y)
type family FromL s where
FromL ('InL a) = a
data SumElem :: (f :+: g) k -> k -> Type where
IInL :: Elem f as a -> SumElem ('InL as) a
IInR :: Elem f bs b -> SumElem ('InR bs) b
type instance Elem (f :+: g) = SumElem
instance (Universe f, Universe g) => Universe (f :+: g) where
idecideAny
:: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()
=> (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))
-> Sing abs
-> Decision (Any (f :+: g) p @@ abs)
idecideAny f = \case
SInL xs -> mapDecision anySumL sumLAny
$ idecideAny @f @_ @p (f . IInL) xs
SInR ys -> mapDecision anySumR sumRAny
$ idecideAny @g @_ @p (f . IInR) ys
idecideAll
:: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()
=> (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))
-> Sing abs
-> Decision (All (f :+: g) p @@ abs)
idecideAll f = \case
SInL xs -> mapDecision allSumL sumLAll
$ idecideAll @f @_ @p (f . IInL) xs
SInR xs -> mapDecision allSumR sumRAll
$ idecideAll @g @_ @p (f . IInR) xs
igenAllA
:: forall k (p :: k ~> Type) (abs :: (f :+: g) k) h. Applicative h
=> (forall ab. Elem (f :+: g) abs ab -> Sing ab -> h (p @@ ab))
-> Sing abs
-> h (All (f :+: g) p @@ abs)
igenAllA f = \case
SInL xs -> allSumL <$> igenAllA @f @_ @p (f . IInL) xs
SInR xs -> allSumR <$> igenAllA @g @_ @p (f . IInR) xs
anySumL :: Any f p @@ as -> Any (f :+: g) p @@ 'InL as
anySumL (WitAny i x) = WitAny (IInL i) x
anySumR :: Any g p @@ bs -> Any (f :+: g) p @@ 'InR bs
anySumR (WitAny j y) = WitAny (IInR j) y
sumLAny :: Any (f :+: g) p @@ 'InL as -> Any f p @@ as
sumLAny (WitAny (IInL i) x) = WitAny i x
sumRAny :: Any (f :+: g) p @@ 'InR bs -> Any g p @@ bs
sumRAny (WitAny (IInR j) y) = WitAny j y
allSumL :: All f p @@ as -> All (f :+: g) p @@ 'InL as
allSumL a = WitAll $ \case IInL i -> runWitAll a i
allSumR :: All g p @@ bs -> All (f :+: g) p @@ 'InR bs
allSumR a = WitAll $ \case IInR j -> runWitAll a j
sumLAll :: All (f :+: g) p @@ 'InL as -> All f p @@ as
sumLAll a = WitAll $ runWitAll a . IInL
sumRAll :: All (f :+: g) p @@ 'InR bs -> All g p @@ bs
sumRAll a = WitAll $ runWitAll a . IInR