{-# 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(..)
, CompElem(..)
, All, WitAll(..), NotAll
, Any, WitAny(..), None
, Null, NotNull
, IsJust, IsNothing, IsRight, IsLeft
, decideAny, decideAll, genAllA, genAll, igenAll
, foldMapUni, ifoldMapUni, index, pickElem
, (:.:)(..), Sing(SComp), sGetComp, GetComp
, allComp, compAll, anyComp, compAny
, ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1
) where
import Control.Applicative
import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
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
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 :: (k ~> Type) -> (f k ~> Type)
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 :: (k ~> Type) -> (f k ~> Type)
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 (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)