summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorjle <>2019-08-13 06:36:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-08-13 06:36:00 (GMT)
commit764fd14ea5e117a512c025e166f79449e736b392 (patch)
tree743780c0b3e1881cf18262f708c873f3880fe32a
parent44b0a1c892b3a3e13104a1226c3fd0d4ab378609 (diff)
version 0.2.0.00.2.0.0
-rw-r--r--CHANGELOG.md10
-rw-r--r--decidable.cabal13
-rw-r--r--src/Data/Type/Predicate.hs97
-rw-r--r--src/Data/Type/Predicate/Auto.hs48
-rw-r--r--src/Data/Type/Predicate/Logic.hs2
-rw-r--r--src/Data/Type/Predicate/Param.hs1
-rw-r--r--src/Data/Type/Predicate/Quantification.hs21
-rw-r--r--src/Data/Type/Universe.hs844
-rw-r--r--src/Data/Type/Universe/Subset.hs9
9 files changed, 291 insertions, 754 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d3e2b1..2c9bc55 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,16 @@
Changelog
=========
+Version 0.2.0.0
+---------------
+
+*August 12, 2019*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.2.0.0>
+
+* Full restructuring of the Universe system, pulling it all out into a new
+ package, *functor-products*.
+
Version 0.1.5.0
---------------
diff --git a/decidable.cabal b/decidable.cabal
index 004f002..da3345c 100644
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -1,13 +1,13 @@
cabal-version: 1.12
--- This file has been generated from package.yaml by hpack version 0.31.0.
+-- This file has been generated from package.yaml by hpack version 0.31.2.
--
-- see: https://github.com/sol/hpack
--
--- hash: 39c525768bc5e732a9d0d8a6b1931c269a0e4339a68d83434f6b3a4cf3f80c9f
+-- hash: 91c5808428e945b6349291657cb7510e476dba940bd88509714b4178da856af3
name: decidable
-version: 0.1.5.0
+version: 0.2.0.0
synopsis: Combinators for manipulating dependently-typed predicates.
description: This library provides combinators and typeclasses for working and manipulating
type-level predicates in Haskell, which are represented as matchable type-level
@@ -22,7 +22,7 @@ maintainer: justin@jle.im
copyright: (c) Justin Le 2018
license: BSD3
license-file: LICENSE
-tested-with: GHC >= 8.4 && < 8.8
+tested-with: GHC >= 8.6
build-type: Simple
extra-source-files:
README.md
@@ -48,5 +48,8 @@ library
ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns
build-depends:
base >=4.11 && <5
- , singletons >=2.4
+ , functor-products
+ , microlens
+ , singletons >=2.5
+ , vinyl
default-language: Haskell2010
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
index 32ce940..f8d7d40 100644
--- a/src/Data/Type/Predicate.hs
+++ b/src/Data/Type/Predicate.hs
@@ -1,8 +1,10 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
@@ -27,7 +29,7 @@ module Data.Type.Predicate (
-- * Predicates
Predicate, Wit(..)
-- ** Construct Predicates
- , TyPred, Evident, EqualTo, BoolPred, Impossible
+ , TyPred, Evident, EqualTo, BoolPred, Impossible, In
-- ** Manipulate predicates
, PMap, type Not, decideNot
-- * Provable Predicates
@@ -50,12 +52,17 @@ module Data.Type.Predicate (
, mapRefuted
) where
+import Data.Functor.Identity
import Data.Kind
+import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe
import Data.Singletons
import Data.Singletons.Decide
-import Data.Singletons.Prelude hiding (Not)
+import Data.Singletons.Prelude hiding (Not, ElemSym1)
+import Data.Singletons.Prelude.Identity
+import Data.Type.Functor.Product
import Data.Void
+import qualified Data.Singletons.Prelude.List.NonEmpty as NE
-- | A type-level predicate in Haskell. We say that the predicate @P ::
-- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists
@@ -354,6 +361,37 @@ instance Decidable Evident
instance Provable Evident where
prove = id
+-- | @since 2.0.0
+instance Provable (TyPred (Rec Sing)) where
+ prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (Rec Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PMaybe Sing)) where
+ prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PMaybe Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (NERec Sing)) where
+ prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (NERec Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PIdentity Sing)) where
+ prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PIdentity Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PEither Sing)) where
+ prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PEither Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PTup Sing)) where
+ prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PTup Sing))
+
instance (Decidable p, SingI f) => Decidable (PMap f p) where
decide = decide @p . applySing (sing :: Sing f)
@@ -463,3 +501,58 @@ mapRefuted
-> Refuted b
-> Refuted a
mapRefuted = flip (.)
+
+-- | @'In' f as@ is a predicate that a given input @a@ is a member of
+-- collection @as@.
+type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
+
+instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where
+ decide :: forall a. Sing a -> Decision (Index as a)
+ decide x = go (sing @as)
+ where
+ go :: Sing bs -> Decision (Index bs a)
+ go = \case
+ SNil -> Disproved $ \case {}
+ y `SCons` ys -> case x %~ y of
+ Proved Refl -> Proved IZ
+ Disproved v -> case go ys of
+ Proved i -> Proved (IS i)
+ Disproved u -> Disproved $ \case
+ IZ -> v Refl
+ IS i -> u i
+
+instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where
+ decide x = case sing @as of
+ SNothing -> Disproved $ \case {}
+ SJust y -> case x %~ y of
+ Proved Refl -> Proved IJust
+ Disproved v -> Disproved $ \case IJust -> v Refl
+
+instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where
+ decide x = case sing @as of
+ SLeft _ -> Disproved $ \case {}
+ SRight y -> case x %~ y of
+ Proved Refl -> Proved IRight
+ Disproved v -> Disproved $ \case IRight -> v Refl
+
+instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where
+ decide x = case sing @as of
+ y NE.:%| (Sing :: Sing bs) -> case x %~ y of
+ Proved Refl -> Proved NEHead
+ Disproved v -> case decide @(In [] bs) x of
+ Proved i -> Proved $ NETail i
+ Disproved u -> Disproved $ \case
+ NEHead -> v Refl
+ NETail i -> u i
+
+instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where
+ decide x = case sing @as of
+ STuple2 _ y -> case x %~ y of
+ Proved Refl -> Proved ISnd
+ Disproved v -> Disproved $ \case ISnd -> v Refl
+
+instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where
+ decide x = case sing @as of
+ SIdentity y -> case x %~ y of
+ Proved Refl -> Proved IId
+ Disproved v -> Disproved $ \case IId -> v Refl
diff --git a/src/Data/Type/Predicate/Auto.hs b/src/Data/Type/Predicate/Auto.hs
index de41c60..4fc069d 100644
--- a/src/Data/Type/Predicate/Auto.hs
+++ b/src/Data/Type/Predicate/Auto.hs
@@ -43,6 +43,7 @@ import Data.List.NonEmpty (NonEmpty(..))
import Data.Singletons
import Data.Singletons.Sigma
import Data.Type.Equality
+import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Predicate.Param
@@ -167,18 +168,9 @@ instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where
instance AutoElem ((,) j) '(w, a) a where
autoElem = ISnd
--- TODO: ???
--- instance AutoElem (f :.: g) p ('Comp ass) where
-
instance AutoElem Identity ('Identity a) a where
autoElem = IId
-instance AutoElem f as a => AutoElem (f :+: g) ('InL as) a where
- autoElem = IInL autoElem
-
-instance AutoElem g bs b => AutoElem (f :+: g) ('InR bs) b where
- autoElem = IInR autoElem
-
instance AutoElem f as a => Auto (In f as) a where
auto = autoElem @f @as @a
@@ -219,25 +211,12 @@ instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
NEHead -> auto @_ @p @a
NETail i -> runWitAll (autoAll @[] @p @as) i
-instance AutoAll f (All g p) ass => AutoAll (f :.: g) p ('Comp ass) where
- autoAll = WitAll $ \(i :? j) ->
- runWitAll (runWitAll (autoAll @f @(All g p) @ass) i) j
-
instance Auto p a => AutoAll ((,) j) p '(w, a) where
autoAll = WitAll $ \case ISnd -> auto @_ @p @a
-instance AutoAll Proxy p 'Proxy where
- autoAll = WitAll $ \case {}
-
instance Auto p a => AutoAll Identity p ('Identity a) where
autoAll = WitAll $ \case IId -> auto @_ @p @a
-instance AutoAll f p as => AutoAll (f :+: g) p ('InL as) where
- autoAll = allSumL $ autoAll @f @p @as
-
-instance AutoAll g p bs => AutoAll (f :+: g) p ('InR bs) where
- autoAll = allSumR $ autoAll @g @p @bs
-
-- | @since 0.1.2.0
instance AutoAll f p as => Auto (All f p) as where
auto = autoAll @f @p @as
@@ -265,12 +244,6 @@ instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
instance SingI a => Auto (NotNull Identity) ('Identity a) where
auto = WitAny IId sing
-instance Auto (NotNull f) as => Auto (NotNull (f :+: g)) ('InL as) where
- auto = anySumL $ auto @_ @(NotNull f) @as
-
-instance Auto (NotNull g) bs => Auto (NotNull (f :+: g)) ('InR bs) where
- auto = anySumR $ auto @_ @(NotNull g) @bs
-
-- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to
-- not be true at compiletime.
--
@@ -339,3 +312,22 @@ autoNotAll = anyNotNotAll sing . autoAny
instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p))) as where
auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))
$ auto @_ @(Not (Any f (Found p))) @as
+
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (Rec Sing)) as where
+ auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PMaybe Sing)) as where
+ auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (NERec Sing)) as where
+ auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PEither Sing)) as where
+ auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PTup Sing)) as where
+ auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PIdentity Sing)) as where
+ auto = singProd sing
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
index c997f24..a8a0621 100644
--- a/src/Data/Type/Predicate/Logic.hs
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -208,7 +208,7 @@ atom = const
-- | We cannot have both @p@ and @'Not' p@.
--
--- (Renamed in v0.1.4.0; used to be 'excludedMiddle')
+-- (Renamed in v0.1.4.0; used to be @excludedMiddle@)
--
-- @since 0.1.4.0
complementation :: forall p. (p &&& Not p) --> Impossible
diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs
index c976c68..23196a6 100644
--- a/src/Data/Type/Predicate/Param.hs
+++ b/src/Data/Type/Predicate/Param.hs
@@ -44,6 +44,7 @@ import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude.Tuple
import Data.Singletons.Sigma
+import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Universe
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
index b41950b..80fec02 100644
--- a/src/Data/Type/Predicate/Quantification.hs
+++ b/src/Data/Type/Predicate/Quantification.hs
@@ -25,8 +25,6 @@ module Data.Type.Predicate.Quantification (
, decideAny, idecideAny, decideNone, idecideNone
-- ** Entailment
, entailAny, ientailAny, entailAnyF, ientailAnyF
- -- ** Composition
- , allComp, compAll
-- * All
, All, WitAll(..), NotAll
-- ** Decision
@@ -34,8 +32,6 @@ module Data.Type.Predicate.Quantification (
-- ** Entailment
, entailAll, ientailAll, entailAllF, ientailAllF
, decideEntailAll, idecideEntailAll
- -- ** Composition
- , anyComp, compAny
-- * Logical interplay
, allToAny
, allNotNone, noneAllNot
@@ -45,6 +41,7 @@ module Data.Type.Predicate.Quantification (
import Data.Kind
import Data.Singletons
import Data.Singletons.Decide
+import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Universe
@@ -74,7 +71,7 @@ ientailAny
=> (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) -- ^ implication
-> Any f p @@ as
-> Any f q @@ as
-ientailAny f (WitAny i x) = WitAny i (f i (index i sing) x)
+ientailAny f (WitAny i x) = WitAny i (f i (indexSing i sing) x)
-- | If there exists an @a@ s.t. @p a@, and if @p@ implies @q@, then there
-- must exist an @a@ s.t. @q a@.
@@ -90,7 +87,7 @@ ientailAll
=> (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) -- ^ implication
-> All f p @@ as
-> All f q @@ as
-ientailAll f a = WitAll $ \i -> f i (index i sing) (runWitAll a i)
+ientailAll f a = WitAll $ \i -> f i (indexSing i sing) (runWitAll a i)
-- | If for all @a@ we have @p a@, and if @p@ implies @q@, then for all @a@
-- we must also have @p a@.
@@ -124,7 +121,7 @@ entailAnyF
=> (p --># q) h -- ^ implication in context
-> (Any f p --># Any f q) h
entailAnyF f x a = withSingI x $
- ientailAnyF @f @p @q (\i -> f (index i x)) a
+ ientailAnyF @f @p @q (\i -> f (indexSing i x)) a
-- | 'entailAllF', but providing an 'Elem'.
ientailAllF
@@ -132,7 +129,9 @@ ientailAllF
=> (forall a. Elem f as a -> p @@ a -> h (q @@ a)) -- ^ implication in context
-> All f p @@ as
-> h (All f q @@ as)
-ientailAllF f a = igenAllA (\i _ -> f i (runWitAll a i)) sing
+ientailAllF f a = fmap (prodAll getWit)
+ . itraverseProd (\i _ -> Wit @q <$> f i (runWitAll a i))
+ $ singProd (sing @as)
-- | If @p@ implies @q@ under some context @h@, and if we have @p a@ for
-- all @a@, then we must have @q a@ for all @a@ under context @h@.
@@ -141,7 +140,7 @@ entailAllF
=> (p --># q) h -- ^ implication in context
-> (All f p --># All f q) h
entailAllF f x a = withSingI x $
- ientailAllF @f @p @q (\i -> f (index i x)) a
+ ientailAllF @f @p @q (\i -> f (indexSing i x)) a
-- | 'entailAllF', but providing an 'Elem'.
idecideEntailAll
@@ -163,7 +162,7 @@ decideEntailAll = dmap @(All f)
--
-- @since 0.1.2.0
anyImpossible :: Universe f => Any f Impossible --> Impossible
-anyImpossible _ (WitAny i p) = p . index i
+anyImpossible _ (WitAny i p) = p . indexSing i
-- | If any @a@ in @as@ does not satisfy @p@, then not all @a@ in @as@
-- satisfy @p@.
@@ -182,7 +181,7 @@ notAllAnyNot
=> NotAll f p --> Any f (Not p)
notAllAnyNot xs vAll = elimDisproof (decide @(Any f (Not p)) xs) $ \vAny ->
vAll $ WitAll $ \i ->
- elimDisproof (decide @p (index i xs)) $ \vP ->
+ elimDisproof (decide @p (indexSing i xs)) $ \vP ->
vAny $ WitAny i vP
-- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies
diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs
index add5756..ed1bdf7 100644
--- a/src/Data/Type/Universe.hs
+++ b/src/Data/Type/Universe.hs
@@ -1,21 +1,21 @@
-{-# 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 #-}
+{-# 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 TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
-- |
-- Module : Data.Type.Universe
@@ -32,9 +32,9 @@
module Data.Type.Universe (
-- * Universe
Elem, In, Universe(..)
+ , singAll
-- ** Instances
- , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)
- , CompElem(..), SumElem(..)
+ , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..)
-- ** Predicates
, All, WitAll(..), NotAll
, Any, WitAny(..), None
@@ -42,59 +42,26 @@ module Data.Type.Universe (
-- *** Specialized
, IsJust, IsNothing, IsRight, IsLeft
-- * Decisions and manipulations
- , decideAny, decideAll, genAllA, genAll, igenAll
- , foldMapUni, ifoldMapUni, index, pickElem
- -- * Universe Combination
- -- ** Universe Composition
- , (:.:)(..), sGetComp, GetComp
- , allComp, compAll, anyComp, compAny
- -- ** Universe Disjunction
- , (:+:)(..)
- , anySumL, anySumR, sumLAny, sumRAny
- , allSumL, allSumR, sumLAll, sumRAll
- -- * Defunctionalization symbols
- , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1
- -- * Singletons
- , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIProxy, SIIdentity(..)
- , Sing (SComp, SInL, SIndex', SIJust', SIRight', SNEIndex', SISnd', SIProxy', SIIdentity')
+ , decideAny, decideAll
+ , genAll, igenAll
+ , splitSing
+ , pickElem
) 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.Singletons.Prelude.Identity
+import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
-import Data.Typeable (Typeable)
-import GHC.Generics (Generic)
+import GHC.Generics ((:*:)(..))
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
-
--- | A witness for membership of a given item in a type-level collection
-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
-
--- | @'In' f as@ is a predicate that a given input @a@ is a member of
--- collection @as@.
-type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
-
-- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the
-- type-level collection @as@, the predicate @p a@ is true.
data WitAny f :: (k ~> Type) -> f k -> Type where
@@ -135,20 +102,21 @@ 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)
+ prove xs = WitAll $ \i -> prove @p (indexSing i xs)
instance Universe f => TFunctor (Any f) where
- tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)
+ tmap f xs (WitAny i x) = WitAny i (f (indexSing i xs) x)
instance Universe f => TFunctor (All f) where
- tmap f xs a = WitAll $ \i -> f (index i xs) (runWitAll a i)
+ tmap f xs a = WitAll $ \i -> f (indexSing 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
-- | Typeclass for a type-level container that you can quantify or lift
-- type-level predicates over.
-class Universe (f :: Type -> Type) where
+class FProd f => Universe (f :: Type -> Type) where
+
-- | 'decideAny', but providing an 'Elem'.
idecideAny
:: forall k (p :: k ~> Type) (as :: f k). ()
@@ -161,11 +129,16 @@ class Universe (f :: Type -> Type) where
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -- ^ predicate on value
-> (Sing as -> Decision (All f p @@ as)) -- ^ predicate on collection
- -- | 'genAllA', but providing an 'Elem'.
- igenAllA
- :: forall k (p :: k ~> Type) (as :: f k) h. Applicative h
- => (forall a. Elem f as a -> Sing a -> h (p @@ a)) -- ^ predicate on value in context
- -> (Sing as -> h (All f p @@ as)) -- ^ predicate on collection in context
+ allProd
+ :: forall p g. ()
+ => (forall a. Sing a -> p @@ a -> g a)
+ -> All f p --> TyPred (Prod f g)
+
+ prodAll
+ :: forall p g as. ()
+ => (forall a. g a -> p @@ a)
+ -> Prod f g as
+ -> All f p @@ as
-- | Predicate that a given @as :: f k@ is empty and has no items in it.
type Null f = (None f Evident :: Predicate (f k))
@@ -210,28 +183,28 @@ decideAll
-> Decide (All f p) -- ^ predicate on collection
decideAll f = idecideAll (const f)
--- | If @p a@ is true for all values @a@ in @as@ under some
--- (Applicative) context @h@, then you can create an @'All' p as@ under
--- that Applicative context @h@.
---
--- Can be useful with 'Identity' (which is basically unwrapping and
--- wrapping 'All'), or with 'Maybe' (which can express predicates that
--- are either provably true or not provably false).
---
--- In practice, this can be used to iterate and traverse and sequence
--- actions over all "items" in @as@.
-genAllA
- :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
- => (forall a. Sing a -> h (p @@ a)) -- ^ predicate on value in context
- -> (Sing as -> h (All f p @@ as)) -- ^ predicate on collection in context
-genAllA f = igenAllA (const f)
+-- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
+splitSing
+ :: forall f k (as :: f k). Universe f
+ => Sing as
+ -> All f (TyPred Sing) @@ as
+splitSing = prodAll id . singProd
+
+-- | Automatically generate a witness for a member, if possible
+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
-- | 'genAll', but providing an 'Elem'.
igenAll
:: forall f k (p :: k ~> Type) (as :: f k). Universe f
=> (forall a. Elem f as a -> Sing a -> p @@ a) -- ^ always-true predicate on value
-> (Sing as -> All f p @@ as) -- ^ always-true predicate on collection
-igenAll f = runIdentity . igenAllA (\i -> Identity . f i)
+igenAll f = prodAll (\(i :*: x) -> f i x) . imapProd (:*:) . singProd
-- | If @p a@ is true for all values @a@ in @as@, then we have @'All'
-- p as@. Basically witnesses the definition of 'All'.
@@ -239,109 +212,35 @@ genAll
:: forall f k (p :: k ~> Type). Universe f
=> Prove p -- ^ always-true predicate on value
-> Prove (All f p) -- ^ always-true predicate on collection
-genAll f = igenAll (const f)
-
--- | Extract the item from the container witnessed by the 'Elem'
-index
- :: forall f as a. Universe f
- => Elem f as a -- ^ Witness
- -> Sing as -- ^ Collection
- -> Sing a
-index i = (`runWitAll` i) . splitSing
+genAll f = prodAll f . singProd
-- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
-splitSing
+singAll
:: forall f k (as :: f k). Universe f
=> Sing as
- -> All f (TyPred Sing) @@ as
-splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)
+ -> All f Evident @@ as
+singAll = prodAll id . singProd
--- | Automatically generate a witness for a member, if possible
-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
-
--- | 'foldMapUni' but with access to the index.
-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)
-
--- | A 'foldMap' over all items in a collection.
-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)
-
--- | Witness an item in a type-level list by providing its index.
-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
-
--- | Kind-indexed singleton for 'Index'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper 'SIndex'',
--- which has an actual proper 'Sing' instance.
+-- | Test that a 'Maybe' is 'Just'.
--
--- @since 0.1.5.0
-data SIndex as a :: Index as a -> Type where
- SIZ :: SIndex (a ': as) a 'IZ
- SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)
-
-deriving instance Show (SIndex as a i)
-
-newtype instance Sing (i :: Index as a) where
- SIndex' :: SIndex as a i -> Sing i
+-- @since 0.1.2.0
+type IsJust = (NotNull Maybe :: Predicate (Maybe k))
-instance SingI 'IZ where
- sing = SIndex' SIZ
+-- | Test that a 'Maybe' is 'Nothing'.
+--
+-- @since 0.1.2.0
+type IsNothing = (Null Maybe :: Predicate (Maybe k))
-instance SingI i => SingI ('IS i) where
- sing = case sing of
- SIndex' i -> SIndex' (SIS i)
+-- | Test that an 'Either' is 'Right'
+--
+-- @since 0.1.2.0
+type IsRight = (NotNull (Either j) :: Predicate (Either j k))
-instance SingKind (Index as a) where
- type Demote (Index as a) = Index as a
- fromSing (SIndex' i) = go i
- where
- go :: SIndex bs b i -> Index bs b
- go = \case
- SIZ -> IZ
- SIS j -> IS (go j)
- toSing i = go i (SomeSing . SIndex')
- where
- go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
- go = \case
- IZ -> ($ SIZ)
- IS j -> \f -> go j (f . SIS)
+-- | Test that an 'Either' is 'Left'
+--
+-- @since 0.1.2.0
+type IsLeft = (Null (Either j) :: Predicate (Either j k))
-instance SDecide (Index as a) where
- SIndex' i %~ SIndex' j = go i j
- where
- go :: SIndex bs b i -> SIndex bs b j -> Decision (i :~: j)
- go = \case
- SIZ -> \case
- SIZ -> Proved Refl
- SIS _ -> Disproved $ \case {}
- SIS i' -> \case
- SIZ -> Disproved $ \case {}
- SIS j' -> case go i' j' of
- Proved Refl -> Proved Refl
- Disproved v -> Disproved $ \case Refl -> v Refl
instance Universe [] where
idecideAny
@@ -375,65 +274,31 @@ instance Universe [] where
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
+ allProd
+ :: forall p g. ()
+ => (forall a. Sing a -> p @@ a -> g a)
+ -> All [] p --> TyPred (Prod [] g)
+ allProd f = go
where
- go :: p @@ b -> All [] p @@ bs -> All [] p @@ (b ': bs)
- go p a = WitAll $ \case
- IZ -> p
- IS i -> runWitAll a i
-
--- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
--- 'Just'.
-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
-
--- | Kind-indexed singleton for 'IJust'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper 'SIJust'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIJust as a :: IJust as a -> Type where
- SIJust :: SIJust ('Just a) a 'IJust
-
-deriving instance Show (SIJust as a i)
-
-newtype instance Sing (i :: IJust as a) where
- SIJust' :: SIJust as a i -> Sing i
-
-instance SingI 'IJust where
- sing = SIJust' SIJust
-
-instance SingKind (IJust as a) where
- type Demote (IJust as a) = IJust as a
- fromSing (SIJust' SIJust) = IJust
- toSing IJust = SomeSing (SIJust' SIJust)
-
-instance SDecide (IJust as a) where
- SIJust' SIJust %~ SIJust' SIJust = Proved Refl
-
-type instance Elem Maybe = IJust
-
--- | Test that a 'Maybe' is 'Just'.
---
--- @since 0.1.2.0
-type IsJust = (NotNull Maybe :: Predicate (Maybe k))
-
--- | Test that a 'Maybe' is 'Nothing'.
---
--- @since 0.1.2.0
-type IsNothing = (Null Maybe :: Predicate (Maybe k))
+ go :: Sing as -> WitAll [] p as -> Prod [] g as
+ go = \case
+ SNil -> \_ -> RNil
+ x `SCons` xs -> \a -> f x (runWitAll a IZ)
+ :& go xs (WitAll (runWitAll a . IS))
+
+ prodAll
+ :: forall p g as. ()
+ => (forall a. g a -> p @@ a)
+ -> Prod [] g as
+ -> All [] p @@ as
+ prodAll f = go
+ where
+ go :: Prod [] g bs -> All [] p @@ bs
+ go = \case
+ RNil -> WitAll $ \case {}
+ x :& xs -> WitAll $ \case
+ IZ -> f x
+ IS i -> runWitAll (go xs) i
instance Universe Maybe where
idecideAny f = \case
@@ -442,62 +307,17 @@ instance Universe Maybe where
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
-
--- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
--- is 'Right'.
-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
-
--- | Kind-indexed singleton for 'IRight'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper 'SIRight'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIRight as a :: IRight as a -> Type where
- SIRight :: SIRight ('Right a) a 'IRight
-
-deriving instance Show (SIRight as a i)
-
-newtype instance Sing (i :: IRight as a) where
- SIRight' :: SIRight as a i -> Sing i
-
-instance SingI 'IRight where
- sing = SIRight' SIRight
-
-instance SingKind (IRight as a) where
- type Demote (IRight as a) = IRight as a
- fromSing (SIRight' SIRight) = IRight
- toSing IRight = SomeSing (SIRight' SIRight)
-
-instance SDecide (IRight as a) where
- SIRight' SIRight %~ SIRight' SIRight = Proved Refl
-
-type instance Elem (Either j) = IRight
-
--- | Test that an 'Either' is 'Right'
---
--- @since 0.1.2.0
-type IsRight = (NotNull (Either j) :: Predicate (Either j k))
-
--- | Test that an 'Either' is 'Left'
---
--- @since 0.1.2.0
-type IsLeft = (Null (Either j) :: Predicate (Either j k))
+ allProd f = \case
+ SNothing -> \_ -> PNothing
+ SJust x -> \a -> PJust (f x (runWitAll a IJust))
+ prodAll f = \case
+ PNothing -> WitAll $ \case {}
+ PJust x -> WitAll $ \case IJust -> f x
instance Universe (Either j) where
idecideAny f = \case
@@ -506,71 +326,17 @@ instance Universe (Either j) where
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
-
--- | Witness an item in a type-level 'NonEmpty' by either indicating that
--- it is the "head", or by providing an index in the "tail".
-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
-
--- | Kind-indexed singleton for 'NEIndex'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper
--- 'SNEIndex'', which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SNEIndex as a :: NEIndex as a -> Type where
- SNEHead :: SNEIndex (a ':| as) a 'NEHead
- SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
-
-deriving instance Show (SNEIndex as a i)
-
-newtype instance Sing (i :: NEIndex as a) where
- SNEIndex' :: SNEIndex as a i -> Sing i
-
-instance SingI 'NEHead where
- sing = SNEIndex' SNEHead
-
-instance SingI i => SingI ('NETail i) where
- sing = case sing of
- SIndex' i -> SNEIndex' (SNETail i)
-
-instance SingKind (NEIndex as a) where
- type Demote (NEIndex as a) = NEIndex as a
- fromSing = \case
- SNEIndex' SNEHead -> NEHead
- SNEIndex' (SNETail i) -> NETail $ fromSing (SIndex' i)
- toSing = \case
- NEHead -> SomeSing (SNEIndex' SNEHead)
- NETail i -> withSomeSing i $ \case
- SIndex' j -> SomeSing (SNEIndex' (SNETail j))
-
-instance SDecide (NEIndex as a) where
- (%~) = \case
- SNEIndex' SNEHead -> \case
- SNEIndex' SNEHead -> Proved Refl
- SNEIndex' (SNETail _) -> Disproved $ \case {}
- SNEIndex' (SNETail i) -> \case
- SNEIndex' SNEHead -> Disproved $ \case {}
- SNEIndex' (SNETail j) -> case SIndex' i %~ SIndex' j of
- Proved Refl -> Proved Refl
- Disproved v -> Disproved $ \case Refl -> v Refl
-
-type instance Elem NonEmpty = NEIndex
+ allProd f = \case
+ SLeft w -> \_ -> PLeft w
+ SRight x -> \a -> PRight (f x (runWitAll a IRight))
+ prodAll f = \case
+ PLeft _ -> WitAll $ \case {}
+ PRight x -> WitAll $ \case IRight -> f x
instance Universe NonEmpty where
idecideAny
@@ -600,369 +366,41 @@ instance Universe NonEmpty where
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
-
--- | Trivially witness an item in the second field of a type-level tuple.
-data ISnd :: (j, k) -> k -> Type where
- ISnd :: ISnd '(a, b) b
-
-deriving instance Show (ISnd as a)
--- TODO: does this interfere with NonNull stuff?
-instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where
- decide x = withSingI x $ pickElem
-
--- | Kind-indexed singleton for 'ISnd'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper 'SISnd'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SISnd as a :: ISnd as a -> Type where
- SISnd :: SISnd '(a, b) b 'ISnd
-
-deriving instance Show (SISnd as a i)
-
-newtype instance Sing (i :: ISnd as a) where
- SISnd' :: SISnd as a i -> Sing i
-
-instance SingI 'ISnd where
- sing = SISnd' SISnd
-
-instance SingKind (ISnd as a) where
- type Demote (ISnd as a) = ISnd as a
- fromSing (SISnd' SISnd) = ISnd
- toSing ISnd = SomeSing (SISnd' SISnd)
-
-instance SDecide (ISnd as a) where
- SISnd' SISnd %~ SISnd' SISnd = Proved Refl
-
-type instance Elem ((,) j) = ISnd
+ allProd
+ :: forall p g. ()
+ => (forall a. Sing a -> p @@ a -> g a)
+ -> All NonEmpty p --> TyPred (Prod NonEmpty g)
+ allProd f (x NE.:%| xs) a =
+ f x (runWitAll a NEHead)
+ :&| allProd @[] @p f xs (WitAll (runWitAll a . NETail))
+ prodAll
+ :: forall p g as. ()
+ => (forall a. g a -> p @@ a)
+ -> Prod NonEmpty g as
+ -> All NonEmpty p @@ as
+ prodAll f (x :&| xs) = WitAll $ \case
+ NEHead -> f x
+ NETail i -> runWitAll (prodAll @[] @p f xs) i
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
+ allProd f (STuple2 w x) a = PTup w $ f x (runWitAll a ISnd)
+ prodAll f (PTup _ x) = WitAll $ \case ISnd -> f x
- igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x
-
--- | There are no items of type @a@ in a @'Proxy' a@.
---
--- @since 0.1.3.0
-data IProxy :: Proxy k -> k -> Type
-
-deriving instance Show (IProxy 'Proxy a)
-
-instance Provable (Not (TyPred (IProxy 'Proxy))) where
- prove _ = \case {}
-
--- | Kind-indexed singleton for 'IProxy'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper 'SIProxy'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIProxy as a :: IProxy as a -> Type
-
-deriving instance Show (SIProxy as a i)
-
-newtype instance Sing (i :: IProxy as a) where
- SIProxy' :: SIProxy as a i -> Sing i
-
-instance SingKind (IProxy as a) where
- type Demote (IProxy as a) = IProxy as a
- fromSing (SIProxy' i) = case i of {}
- toSing = \case {}
-
-instance SDecide (IProxy as a) where
- SIProxy' i %~ SIProxy' _ = Proved $ case i of {}
-
-type instance Elem Proxy = IProxy
-
--- | The null universe
-instance Universe Proxy where
- idecideAny _ _ = Disproved $ \case
- WitAny i _ -> case i of {}
- idecideAll _ _ = Proved $ WitAll $ \case {}
- igenAllA _ _ = pure $ WitAll $ \case {}
-
--- | Trivially witness the item held in an 'Identity'.
---
--- @since 0.1.3.0
-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
-
--- | Kind-indexed singleton for 'IIdentity'. Provided as a separate data
--- declaration to allow you to use these at the type level. However, the
--- main interface is still provided through the newtype wrapper 'SIIdentity'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIIdentity as a :: IIdentity as a -> Type where
- SIId :: SIIdentity ('Identity a) a 'IId
-
-deriving instance Show (SIIdentity as a i)
-
-newtype instance Sing (i :: IIdentity as a) where
- SIIdentity' :: SIIdentity as a i -> Sing i
-
-instance SingI 'IId where
- sing = SIIdentity' SIId
-
-instance SingKind (IIdentity as a) where
- type Demote (IIdentity as a) = IIdentity as a
- fromSing (SIIdentity' SIId) = IId
- toSing IId = SomeSing (SIIdentity' SIId)
-
-instance SDecide (IIdentity as a) where
- SIIdentity' SIId %~ SIIdentity' SIId = Proved Refl
-
-type instance Elem Identity = IIdentity
-
--- | The single-pointed universe. Note that this instance is really only
--- usable in /singletons-2.5/ and higher (so GHC 8.6).
+-- | The single-pointed universe.
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
-
--- | Compose two Functors. Is the same as 'Data.Functor.Compose.Compose'
--- and 'GHC.Generics.:.:', except with a singleton and meant to be used at
--- the type level. Will be redundant if either of the above gets brought
--- into the singletons library.
---
--- Note that because this is a higher-kinded data constructor, there is no
--- 'SingKind' instance; if you need 'fromSing' and 'toSing', try going
--- through 'Comp' and 'getComp' and 'SComp' and 'sGetComp'.
---
--- Note that 'Identity' acts as an identity.
---
--- @since 0.1.2.0
-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)
-
--- | 'getComp' lifted to the type level
---
--- @since 0.1.2.0
-type family GetComp c where
- GetComp ('Comp a) = a
-
--- | Singletonized witness for 'GetComp'
---
--- @since 0.1.2.0
-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
-
--- instance forall f g a f' g' a'. (SingKind (f (g a)), Demote (f (g a)) ~ f' (g' a')) => SingKind ((f :.: g) a) where
--- type Demote ((f :.: g) a) = (:.:) f' g' a'
-
--- | A pair of indices allows you to index into a nested structure.
---
--- @since 0.1.2.0
-data CompElem :: (f :.: g) k -> k -> Type where
- (:?) :: Elem f ass as
- -> Elem g as a
- -> CompElem ('Comp ass) a
-
--- deriving instance ((forall as. Show (Elem f ass as)), (forall as. Show (Elem g as a)))
--- => Show (CompElem ('Comp ass :: (f :.: g) k) 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)
-
--- | Turn a composition of 'Any' into an 'Any' of a composition.
---
--- @since 0.1.2.0
-anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
-anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p
-
--- | Turn an 'Any' of a composition into a composition of 'Any'.
---
--- @since 0.1.2.0
-compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
-compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)
-
--- | Turn a composition of 'All' into an 'All' of a composition.
---
--- @since 0.1.2.0
-allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
-allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j
-
--- | Turn an 'All' of a composition into a composition of 'All'.
---
--- @since 0.1.2.0
-compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
-compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)
-
--- | Disjoint union of two Functors. Is the same as 'Data.Functor.Sum.Sum'
--- and 'GHC.Generics.:+:', except with a singleton and meant to be used at
--- the type level. Will be redundant if either of the above gets brought
--- into the singletons library.
---
--- Note that because this is a higher-kinded data constructor, there is no
--- 'SingKind' instance; if you need 'fromSing' and 'toSing', consider
--- manually pattern matching.
---
--- Note that 'Proxy' acts as an identity.
---
--- @since 0.1.3.0
-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
-
--- | Index into a disjoint union by providing an index into one of the two
--- possible options.
---
--- @since 0.1.3.0
-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
-
--- | Turn an 'Any' of @f@ into an 'Any' of @f ':+:' g@.
-anySumL :: Any f p @@ as -> Any (f :+: g) p @@ 'InL as
-anySumL (WitAny i x) = WitAny (IInL i) x
-
--- | Turn an 'Any' of @g@ into an 'Any' of @f ':+:' g@.
-anySumR :: Any g p @@ bs -> Any (f :+: g) p @@ 'InR bs
-anySumR (WitAny j y) = WitAny (IInR j) y
-
--- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @f@.
-sumLAny :: Any (f :+: g) p @@ 'InL as -> Any f p @@ as
-sumLAny (WitAny (IInL i) x) = WitAny i x
-
--- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @g@.
-sumRAny :: Any (f :+: g) p @@ 'InR bs -> Any g p @@ bs
-sumRAny (WitAny (IInR j) y) = WitAny j y
-
--- | Turn an 'All' of @f@ into an 'All' of @f ':+:' g@.
-allSumL :: All f p @@ as -> All (f :+: g) p @@ 'InL as
-allSumL a = WitAll $ \case IInL i -> runWitAll a i
-
--- | Turn an 'All' of @g@ into an 'All' of @f ':+:' g@.
-allSumR :: All g p @@ bs -> All (f :+: g) p @@ 'InR bs
-allSumR a = WitAll $ \case IInR j -> runWitAll a j
-
--- | Turn an 'All' of @f ':+:' g@ into an 'All' of @f@.
-sumLAll :: All (f :+: g) p @@ 'InL as -> All f p @@ as
-sumLAll a = WitAll $ runWitAll a . IInL
-
--- | Turn an 'All' of @f ':+:' g@ into an 'All' of @g@.
-sumRAll :: All (f :+: g) p @@ 'InR bs -> All g p @@ bs
-sumRAll a = WitAll $ runWitAll a . IInR
+ 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
+ allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)
+ prodAll f (PIdentity x) = WitAll $ \case IId -> f x
diff --git a/src/Data/Type/Universe/Subset.hs b/src/Data/Type/Universe/Subset.hs
index e36e796..804e830 100644
--- a/src/Data/Type/Universe/Subset.hs
+++ b/src/Data/Type/Universe/Subset.hs
@@ -37,6 +37,7 @@ import Data.Kind
import Data.Monoid (Alt(..))
import Data.Singletons
import Data.Singletons.Decide
+import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Predicate.Quantification
@@ -63,7 +64,7 @@ makeSubset
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Subset f p @@ as
-makeSubset f xs = WitSubset $ \i -> f i (index i xs)
+makeSubset f xs = WitSubset $ \i -> f i (indexSing i xs)
-- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
-- predicates.
@@ -72,7 +73,7 @@ makeSubset f xs = WitSubset $ \i -> f i (index i xs)
subsetToList
:: forall f p t. (Universe f, Alternative t)
=> (Subset f p --># Any f p) t
-subsetToList xs s = getAlt $ (`ifoldMapUni` xs) $ \i _ -> Alt $ case runWitSubset s i of
+subsetToList xs s = getAlt $ (`ifoldMapSing` xs) $ \i _ -> Alt $ case runWitSubset s i of
Proved p -> pure $ WitAny i p
Disproved _ -> empty
@@ -158,5 +159,5 @@ mapSubset
-> (q --> p)
-> (Subset f p --> Subset f q)
mapSubset f g xs = withSingI xs $
- imapSubset (\i -> f (index i xs))
- (\i -> g (index i xs))
+ imapSubset (\i -> f (indexSing i xs))
+ (\i -> g (indexSing i xs))