{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Predicate.Quantification (
Any, WitAny(..), None
, decideAny, idecideAny, decideNone, idecideNone
, entailAny, ientailAny, entailAnyF, ientailAnyF
, All, WitAll(..)
, decideAll, idecideAll
, entailAll, ientailAll, entailAllF, ientailAllF
, decideEntailAll, idecideEntailAll
) where
import Data.Kind
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Predicate
import Data.Type.Universe
idecideNone
:: forall f k (p :: k ~> Type) (as :: f k). Universe f
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> (Sing as -> Decision (None f p @@ as))
idecideNone f xs = decideNot @(Any f p) $ idecideAny f xs
decideNone
:: forall f k (p :: k ~> Type). Universe f
=> Decide p
-> Decide (None f p)
decideNone f = idecideNone (const f)
ientailAny
:: forall f p q as. (Universe f, SingI as)
=> (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)
-> Any f p @@ as
-> Any f q @@ as
ientailAny f (WitAny i x) = WitAny i (f i (index i sing) x)
entailAny
:: forall f p q. Universe f
=> (p --> q)
-> (Any f p --> Any f q)
entailAny = tmap @(Any f)
ientailAll
:: forall f p q as. (Universe f, SingI as)
=> (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)
-> All f p @@ as
-> All f q @@ as
ientailAll f a = WitAll $ \i -> f i (index i sing) (runWitAll a i)
entailAll
:: forall f p q. Universe f
=> (p --> q)
-> (All f p --> All f q)
entailAll = tmap @(All f)
ientailAnyF
:: forall f p q as h. Functor h
=> (forall a. Elem f as a -> p @@ a -> h (q @@ a))
-> Any f p @@ as
-> h (Any f q @@ as)
ientailAnyF f = \case WitAny i x -> WitAny i <$> f i x
entailAnyF
:: forall f p q h. (Universe f, Functor h)
=> (p --># q) h
-> (Any f p --># Any f q) h
entailAnyF f x a = withSingI x $
ientailAnyF @f @p @q (\i -> f (index i x)) a
ientailAllF
:: forall f p q as h. (Universe f, Applicative h, SingI as)
=> (forall a. Elem f as a -> p @@ a -> h (q @@ a))
-> All f p @@ as
-> h (All f q @@ as)
ientailAllF f a = igenAllA (\i _ -> f i (runWitAll a i)) sing
entailAllF
:: forall f p q h. (Universe f, Applicative h)
=> (p --># q) h
-> (All f p --># All f q) h
entailAllF f x a = withSingI x $
ientailAllF @f @p @q (\i -> f (index i x)) a
idecideEntailAll
:: forall f p q as. (Universe f, SingI as)
=> (forall a. Elem f as a -> p @@ a -> Decision (q @@ a))
-> All f p @@ as
-> Decision (All f q @@ as)
idecideEntailAll f a = idecideAll (\i _ -> f i (runWitAll a i)) sing
decideEntailAll
:: forall f p q. Universe f
=> p -?> q
-> All f p -?> All f q
decideEntailAll = dmap @(All f)