Skip to content

Commit

Permalink
instance for Maybe
Browse files Browse the repository at this point in the history
  • Loading branch information
@mstksg
mstksg committed Aug 4, 2019
1 parent 5f29247 commit ec88852
Show file tree
Hide file tree
Showing 3 changed files with 154 additions and 51 deletions.
1 change: 1 addition & 0 deletions package.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ dependencies:
- base >= 4.11 && < 5
- singletons >= 2.5
- vinyl
- microlens

library:
source-dirs: src
55 changes: 34 additions & 21 deletions src/Data/Type/Universe/Internal.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,7 @@
module Data.Type.Universe.Internal (
-- * Universe
Elem, In, Prod, HasProd(..), Universe(..)
-- , mapProd
, imapProd
, mapProd, imapProd, indexProd
-- , foldMapProd, ifoldMapProd
-- , splitSing
-- -- ** Instances
Expand Down Expand Up @@ -71,6 +70,8 @@ import Data.Type.Predicate.Logic
import Data.Typeable (Typeable)
import Data.Vinyl (Rec(..))
import GHC.Generics (Generic, (:*:)(..))
import Lens.Micro
import Lens.Micro.Extras
import Prelude hiding (any, all)
import qualified Data.Singletons.Prelude.List.NonEmpty as NE

Expand Down Expand Up @@ -124,18 +125,15 @@ class HasProd (f :: Type -> Type) where
singProd :: Sing as -> Prod f Sing as
prodSing :: Prod f Sing as -> Sing as

itraverseProd
:: Applicative m
=> (forall a. Elem f as a -> g a -> m (h a))
-> Prod f g as
-> m (Prod f h as)
withIndices
:: Prod f g as
-> Prod f (Elem f as :*: g) as

traverseProd
:: Applicative m
=> (forall a. g a -> m (h a))
-> Prod f g as
-> m (Prod f h as)
traverseProd f = itraverseProd (const f)

zipWithProd
:: (forall a. g a -> h a -> j a)
Expand All @@ -144,10 +142,20 @@ class HasProd (f :: Type -> Type) where
-> Prod f j as
zipWithProd f xs ys = imapProd (\i x -> f x (indexProd i ys)) xs

indexProd
ixProd
:: Elem f as a
-> Lens' (Prod f g as) (g a)

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
-> g a
-> All f p @@ as


-- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the
Expand Down Expand Up @@ -216,16 +224,6 @@ class HasProd f => 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

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))

Expand All @@ -241,12 +239,20 @@ type None f p = (Not (Any f p) :: Predicate (f k))
-- @a@ in @as@ does not satisfy predicate @p@.
type NotAll f p = (Not (All f p) :: Predicate (f k))

mapProd
:: HasProd f
=> (forall a. g a -> h a)
-> Prod f g as
-> Prod f h as
mapProd f = runIdentity . traverseProd (Identity . f)


imapProd
:: HasProd f
=> (forall a. Elem f as a -> g a -> h a)
-> Prod f g as
-> Prod f h as
imapProd f = runIdentity . itraverseProd (\i -> Identity . f i)
imapProd f = mapProd (\(i :*: x) -> f i x) . withIndices

-- | Extract the item from the container witnessed by the 'Elem'
index
Expand All @@ -256,6 +262,13 @@ index
-> Sing a
index i = indexProd i . singProd

indexProd
:: HasProd f
=> Elem f as a
-> Prod f g as
-> g a
indexProd i = view (ixProd i)

-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
-- a collection @as@ that is true if and only if /any/ item in @as@
-- satisfies the original predicate.
Expand Down
149 changes: 119 additions & 30 deletions src/Data/Type/Universe/Prod.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ module Data.Type.Universe.Prod (

-- * Universe
Elem, In, Prod, HasProd(..)
, mapProd, imapProd, foldMapProd, ifoldMapProd
, mapProd, imapProd, foldMapProd, ifoldMapProd, itraverseProd
-- ** Instances
, Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)
, CompElem(..), SumElem(..)
Expand Down Expand Up @@ -75,15 +75,16 @@ import Data.Type.Universe.Internal
import Data.Typeable (Typeable)
import Data.Vinyl (Rec(..))
import GHC.Generics (Generic, (:*:)(..))
import Lens.Micro (Lens')
import Prelude hiding (any, all)
import qualified Data.Singletons.Prelude.List.NonEmpty as NE

mapProd
:: HasProd f
=> (forall a. g a -> h a)
itraverseProd
:: (HasProd f, Applicative m)
=> (forall a. Elem f as a -> g a -> m (h a))
-> Prod f g as
-> Prod f h as
mapProd f = runIdentity . traverseProd (Identity . f)
-> m (Prod f h as)
itraverseProd f = traverseProd (\(i :*: x) -> f i x) . withIndices

ifoldMapProd
:: (HasProd f, Monoid m)
Expand Down Expand Up @@ -204,10 +205,6 @@ instance HasProd [] where
RNil -> SNil
x :& xs -> x `SCons` prodSing xs

itraverseProd f = \case
RNil -> pure RNil
x :& xs -> (:&) <$> f IZ x <*> itraverseProd (f . IS) xs

traverseProd
:: forall g h m as. Applicative m
=> (forall a. g a -> m (h a))
Expand Down Expand Up @@ -235,7 +232,83 @@ instance HasProd [] where
x :& xs -> \case
y :& ys -> f x y :& go xs ys

withIndices = \case
RNil -> RNil
x :& xs -> (IZ :*: x) :& mapProd (\(i :*: y) -> IS i :*: y) (withIndices xs)

ixProd
:: forall g as a. ()
=> Elem [] as a
-> Lens' (Prod [] g as) (g a)
ixProd i0 (f :: g a -> h (g a)) = go i0
where
go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)
go = \case
IZ -> \case
x :& xs -> (:& xs) <$> f x
IS i -> \case
x :& xs -> (x :&) <$> go i xs

allProd
:: forall p g. ()
=> (forall a. Sing a -> p @@ a -> g a)
-> All [] p --> TyPred (Prod [] g)
allProd f = go
where
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 [] 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



-- | Test if two indices point to the same item in a list.
--
Expand Down Expand Up @@ -310,36 +383,52 @@ type instance Prod Maybe = PMaybe
--type IsNothing = (Null Maybe :: Predicate (Maybe k))

instance HasProd 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

singProd = \case
SNothing -> PNothing
SJust x -> PJust x
prodSing = \case
PNothing -> SNothing
PJust x -> SJust x

itraverseProd f = \case
withIndices = \case
PNothing -> PNothing
PJust x -> PJust (IJust :*: x)

traverseProd f = \case
PNothing -> pure PNothing
PJust x -> PJust <$> f IJust x
PJust x -> PJust <$> f x

-- zipWithProd f = \case
-- PNothing -> \case
-- PNothing -> \case
zipWithProd f = \case
PNothing -> \case
PNothing -> PNothing
PJust x -> \case
PJust y -> PJust (f x y)

ixProd = \case
IJust -> \f -> \case
PJust x -> PJust <$> f x

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 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


-- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
-- is 'Right'.
Expand Down Expand Up @@ -466,8 +555,8 @@ instance SDecide (NEIndex as a) where
type instance Elem NonEmpty = NEIndex

instance HasProd NonEmpty where
instance Universe NonEmpty where

instance Universe NonEmpty where
-- idecideAny
-- :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
-- => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
Expand Down

0 comments on commit ec88852

Please sign in to comment.