{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Universe (
Elem, In, Universe(..)
, Index(..), IsJust(..), IsRight(..), NEIndex(..), Snd(..)
, All, WitAll(..)
, Any, WitAny(..), None
, Null, NotNull
, decideAny, decideAll, genAllA, genAll, igenAll
, foldMapUni, ifoldMapUni, index, pickElem
, ElemSym0, ElemSym1, ElemSym2
) where
import Data.Type.Predicate.Logic
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, Snd, Null, Not)
import Data.Type.Predicate
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))
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 IsJust :: Maybe k -> k -> Type where
IsJust :: IsJust ('Just a) a
deriving instance Show (IsJust as a)
instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IsJust as)) where
decide x = withSingI x $ pickElem
type instance Elem Maybe = IsJust
instance Universe Maybe where
idecideAny f = \case
SNothing -> Disproved $ \case WitAny i _ -> case i of {}
SJust x -> case f IsJust x of
Proved p -> Proved $ WitAny IsJust p
Disproved v -> Disproved $ \case
WitAny IsJust p -> v p
idecideAll f = \case
SNothing -> Proved $ WitAll $ \case {}
SJust x -> case f IsJust x of
Proved p -> Proved $ WitAll $ \case IsJust -> p
Disproved v -> Disproved $ \a -> v $ runWitAll a IsJust
igenAllA f = \case
SNothing -> pure $ WitAll $ \case {}
SJust x -> (\p -> WitAll $ \case IsJust -> p) <$> f IsJust x
data IsRight :: Either j k -> k -> Type where
IsRight :: IsRight ('Right a) a
deriving instance Show (IsRight as a)
instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IsRight as)) where
decide x = withSingI x $ pickElem
type instance Elem (Either j) = IsRight
instance Universe (Either j) where
idecideAny f = \case
SLeft _ -> Disproved $ \case WitAny i _ -> case i of {}
SRight x -> case f IsRight x of
Proved p -> Proved $ WitAny IsRight p
Disproved v -> Disproved $ \case
WitAny IsRight p -> v p
idecideAll f = \case
SLeft _ -> Proved $ WitAll $ \case {}
SRight x -> case f IsRight x of
Proved p -> Proved $ WitAll $ \case IsRight -> p
Disproved v -> Disproved $ \a -> v $ runWitAll a IsRight
igenAllA f = \case
SLeft _ -> pure $ WitAll $ \case {}
SRight x -> (\p -> WitAll $ \case IsRight -> p) <$> f IsRight 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 Snd :: (j, k) -> k -> Type where
Snd :: Snd '(a, b) b
deriving instance Show (Snd as a)
instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (Snd as)) where
decide x = withSingI x $ pickElem
type instance Elem ((,) j) = Snd
instance Universe ((,) j) where
idecideAny f (STuple2 _ x) = case f Snd x of
Proved p -> Proved $ WitAny Snd p
Disproved v -> Disproved $ \case WitAny Snd p -> v p
idecideAll f (STuple2 _ x) = case f Snd x of
Proved p -> Proved $ WitAll $ \case Snd -> p
Disproved v -> Disproved $ \a -> v $ runWitAll a Snd
igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case Snd -> p) <$> f Snd x