predicate-typed-0.7.4.1: src/Predicate/Data/Either.hs
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
-- | promoted 'Either' functions
module Predicate.Data.Either (
-- ** boolean predicates
IsLeft
, IsRight
-- ** constructors
, MkLeft
, MkLeft'
, MkRight
, MkRight'
-- ** get rid of Either
, Left'
, Right'
, LeftDef
, LeftFail
, RightDef
, RightFail
, EitherBool
, PartitionEithers
-- ** miscellaneous
, type (|||)
, type (+++)
, EitherX
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import Data.Either (isLeft, isRight, partitionEithers)
-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> :set -XTypeOperators
-- >>> :set -XOverloadedStrings
-- >>> import qualified Data.Text as T
-- >>> import Predicate.Prelude
-- >>> import qualified Data.Semigroup as SG
-- | extracts the left value from an 'Either'
--
-- >>> pz @(Left' >> Succ) (Left 20)
-- Val 21
--
-- >>> pz @(Left' >> Succ) (Right 'a')
-- Fail "Left' found Right"
--
data Left' deriving Show
instance Show a => P Left' (Either a x) where
type PP Left' (Either a x) = a
eval _ opts lr =
let msg0 = "Left'"
in pure $ case lr of
Right _ -> mkNode opts (Fail (msg0 <> " found Right")) "" []
Left a -> mkNode opts (Val a) (msg0 <> " " <> showL opts a) []
-- | extracts the right value from an 'Either'
--
-- >>> pz @(Right' >> Succ) (Right 20)
-- Val 21
--
-- >>> pz @(Right' >> Succ) (Left 'a')
-- Fail "Right' found Left"
--
data Right' deriving Show
instance Show a => P Right' (Either x a) where
type PP Right' (Either x a) = a
eval _ opts lr =
let msg0 = "Right'"
in pure $ case lr of
Left _ -> mkNode opts (Fail (msg0 <> " found Left")) "" []
Right a -> mkNode opts (Val a) (msg0 <> " " <> showL opts a) []
-- | similar 'Control.Arrow.|||'
--
-- >>> pz @(Pred ||| Id) (Left 13)
-- Val 12
--
-- >>> pz @(ShowP Id ||| Id) (Right "hello")
-- Val "hello"
--
-- >>> pl @('True ||| 'False) (Left "someval")
-- True ((|||) Left True | "someval")
-- Val True
--
-- >>> pl @('True ||| 'False) (Right "someval")
-- False ((|||) Right False | "someval")
-- Val False
--
-- >>> pl @(ShowP Succ ||| ShowP Id) (Left 123)
-- Present "124" ((|||) Left "124" | 123)
-- Val "124"
--
-- >>> pl @(ShowP Succ ||| ShowP Id) (Right True)
-- Present "True" ((|||) Right "True" | True)
-- Val "True"
--
-- >>> pl @(Not Id ||| Id) (Right True)
-- Present True ((|||) Right True | True)
-- Val True
--
-- >>> pl @(Not Id ||| Id) (Left True)
-- False ((|||) Left False | True)
-- Val False
--
data p ||| q deriving Show
infixr 2 |||
instance ( Show (PP p a)
, P p a
, P q b
, PP p a ~ PP q b
, Show a
, Show b
) => P (p ||| q) (Either a b) where
type PP (p ||| q) (Either a b) = PP p a
eval _ opts lr = do
let msg0 = "(|||)"
case lr of
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR NoInline opts msg0 pp [] of
Left e -> e
Right a1 -> let msg1 = msg0 ++ " Left"
in mkNodeCopy opts pp (show3 opts msg1 a1 a) [hh pp]
Right a -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR NoInline opts msg0 qq [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Right"
in mkNodeCopy opts qq (show3 opts msg1 a1 a) [hh qq]
-- | similar to 'isLeft'
--
-- >>> pz @IsLeft (Right 123)
-- Val False
--
-- >>> pz @IsLeft (Left 'a')
-- Val True
--
data IsLeft deriving Show
instance x ~ Either a b
=> P IsLeft x where
type PP IsLeft x = Bool
eval _ opts x = pure $ mkNodeB opts (isLeft x) "IsLeft" []
-- | similar to 'isRight'
--
-- >>> pz @IsRight (Right 123)
-- Val True
--
-- >>> pz @IsRight (Left "aa")
-- Val False
--
data IsRight deriving Show
instance x ~ Either a b
=> P IsRight x where
type PP IsRight x = Bool
eval _ opts x = pure $ mkNodeB opts (isRight x) "IsRight" []
-- | similar 'Control.Arrow.+++'
--
-- >>> pz @(Pred +++ Id) (Left 13)
-- Val (Left 12)
--
-- >>> pz @(ShowP Id +++ Reverse) (Right "hello")
-- Val (Right "olleh")
--
-- >>> pl @(HeadDef 'False Id +++ Id) (Right @[Bool] 1) -- need @[Bool] to match with 'False
-- Present Right 1 ((+++) Right 1 | 1)
-- Val (Right 1)
--
-- >>> pl @(HeadDef 'False Id +++ Id) (Left [True,False]) -- need @[Bool] to match with 'False!
-- Present Left True ((+++) Left True | [True,False])
-- Val (Left True)
--
-- >>> pl @(Not Id +++ Id) (Right True)
-- Present Right True ((+++) Right True | True)
-- Val (Right True)
--
-- >>> pl @(Not Id +++ Id) (Right 12)
-- Present Right 12 ((+++) Right 12 | 12)
-- Val (Right 12)
--
-- >>> pl @(HeadDef () Id +++ Id) (Right @[()] 1) -- breaks otherwise: Id says () -> () so has to be a list of [()]
-- Present Right 1 ((+++) Right 1 | 1)
-- Val (Right 1)
--
-- >>> pl @(HeadDef () Id +++ Id) (Right @[()] 1) -- this breaks! as Left doesnt have a type
-- Present Right 1 ((+++) Right 1 | 1)
-- Val (Right 1)
--
-- >>> pl @(Not Id +++ Id) (Right @Bool 12)
-- Present Right 12 ((+++) Right 12 | 12)
-- Val (Right 12)
--
data p +++ q deriving Show
infixr 2 +++
instance ( Show (PP p a)
, Show (PP q b)
, P p a
, P q b
, Show a
, Show b
) => P (p +++ q) (Either a b) where
type PP (p +++ q) (Either a b) = Either (PP p a) (PP q b)
eval _ opts lr = do
let msg0 = "(+++)"
case lr of
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR NoInline opts msg0 pp [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Left"
in mkNode opts (Val (Left a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh pp]
Right a -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR NoInline opts msg0 qq [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Right"
in mkNode opts (Val (Right a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh qq]
-- | similar to 'partitionEithers'
--
-- >>> pz @PartitionEithers [Left 'a',Right 2,Left 'c',Right 4,Right 99]
-- Val ("ac",[2,4,99])
--
-- >>> pz @PartitionEithers [Right 2,Right 4,Right 99]
-- Val ([],[2,4,99])
--
-- >>> pz @PartitionEithers [Left 'a',Left 'c']
-- Val ("ac",[])
--
-- >>> pz @PartitionEithers ([] :: [Either () Int])
-- Val ([],[])
--
-- >>> pl @PartitionEithers [Left 4, Right 'x', Right 'y',Left 99]
-- Present ([4,99],"xy") (PartitionEithers ([4,99],"xy") | [Left 4,Right 'x',Right 'y',Left 99])
-- Val ([4,99],"xy")
--
-- >>> pl @PartitionEithers [Left 'x', Right 1,Left 'a', Left 'b',Left 'z', Right 10]
-- Present ("xabz",[1,10]) (PartitionEithers ("xabz",[1,10]) | [Left 'x',Right 1,Left 'a',Left 'b',Left 'z',Right 10])
-- Val ("xabz",[1,10])
--
data PartitionEithers deriving Show
instance ( Show a
, Show b
) => P PartitionEithers [Either a b] where
type PP PartitionEithers [Either a b] = ([a], [b])
eval _ opts as =
let msg0 = "PartitionEithers"
b = partitionEithers as
in pure $ mkNode opts (Val b) (show3 opts msg0 b as) []
-- | Convenient method to convert a @p@ or @q@ to a 'Either' based on a predicate @b@
-- if @b@ then Right @p@ else Left @q@
--
-- >>> pz @(EitherBool (Fst > 4) L21 L22) (24,(-1,999))
-- Val (Right 999)
--
-- >>> pz @(EitherBool (Fst > 4) L21 L22) (1,(-1,999))
-- Val (Left (-1))
--
-- >>> pl @(EitherBool (Fst > 10) L21 L22) (7,('x',99))
-- Present Left 'x' (EitherBool(False) Left 'x')
-- Val (Left 'x')
--
-- >>> pl @(EitherBool (Fst > 10) L21 L22) (11,('x',99))
-- Present Right 99 (EitherBool(True) Right 99)
-- Val (Right 99)
--
-- >>> pl @(EitherBool (Gt 10) "found left" 99) 12
-- Present Right 99 (EitherBool(True) Right 99)
-- Val (Right 99)
--
-- >>> pl @(EitherBool (Gt 10) "found left" 99) 7
-- Present Left "found left" (EitherBool(False) Left "found left")
-- Val (Left "found left")
--
data EitherBool b p q deriving Show
instance ( Show (PP p a)
, P p a
, Show (PP q a)
, P q a
, P b a
, PP b a ~ Bool
) => P (EitherBool b p q) a where
type PP (EitherBool b p q) a = Either (PP p a) (PP q a)
eval _ opts z = do
let msg0 = "EitherBool"
bb <- evalBool (Proxy @b) opts z
case getValueLR NoInline opts (msg0 <> " b failed") bb [] of
Left e -> pure e
Right False -> do
pp <- eval (Proxy @p) opts z
pure $ case getValueLR NoInline opts (msg0 <> " p failed") pp [hh bb] of
Left e -> e
Right p -> mkNode opts (Val (Left p)) (msg0 <> "(False) Left " <> showL opts p) [hh bb, hh pp]
Right True -> do
qq <- eval (Proxy @q) opts z
pure $ case getValueLR NoInline opts (msg0 <> " q failed") qq [hh bb] of
Left e -> e
Right q -> mkNode opts (Val (Right q)) (msg0 <> "(True) Right " <> showL opts q) [hh bb, hh qq]
-- | similar to 'Control.Arrow.|||' but additionally gives @p@ and @q@ the original input
--
-- >>> pz @(EitherX (ShowP (L11 + Snd)) (ShowP Id) Snd) (9,Left 123)
-- Val "132"
--
-- >>> pz @(EitherX (ShowP (L11 + Snd)) (ShowP Id) Snd) (9,Right 'x')
-- Val "((9,Right 'x'),'x')"
--
-- >>> pz @(EitherX (ShowP Id) (ShowP (Second Succ)) Snd) (9,Right 'x')
-- Val "((9,Right 'x'),'y')"
--
data EitherX p q r deriving Show
instance ( P r x
, P p (x,a)
, P q (x,b)
, PP r x ~ Either a b
, PP p (x,a) ~ c
, PP q (x,b) ~ c
) => P (EitherX p q r) x where
type PP (EitherX p q r) x = EitherXT (PP r x) x p
eval _ opts x = do
let msg0 = "EitherX"
rr <- eval (Proxy @r) opts x
case getValueLR NoInline opts msg0 rr [] of
Left e -> pure e
Right (Left a) -> do
let msg1 = msg0 <> "(Left)"
pp <- eval (Proxy @p) opts (x,a)
pure $ case getValueLR NoInline opts msg1 pp [hh rr] of
Left e -> e
Right _ -> mkNodeCopy opts pp msg1 [hh rr, hh pp]
Right (Right b) -> do
let msg1 = msg0 <> "(Right)"
qq <- eval (Proxy @q) opts (x,b)
pure $ case getValueLR NoInline opts msg1 qq [hh rr] of
Left e -> e
Right _ -> mkNodeCopy opts qq msg1 [hh rr, hh qq]
type family EitherXT lr x p where
EitherXT (Either a _b) x p = PP p (x,a)
EitherXT o _ _ = GL.TypeError (
'GL.Text "EitherXT: expected 'Either a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
-- | 'Data.Either.Left' constructor
data MkLeft' t p deriving Show
instance ( Show (PP p x)
, P p x
) => P (MkLeft' t p) x where
type PP (MkLeft' t p) x = Either (PP p x) (PP t x)
eval _ opts x = do
let msg0 = "MkLeft"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR NoInline opts msg0 pp [] of
Left e -> e
Right p ->
let d = Left p
in mkNode opts (Val d) (msg0 <> " Left " <> showL opts p) [hh pp]
-- | 'Data.Either.Left' constructor
--
-- >>> pz @(MkLeft _ Id) 44
-- Val (Left 44)
--
data MkLeft (t :: Type) p deriving Show
type MkLeftT (t :: Type) p = MkLeft' (Hole t) p
instance P (MkLeftT t p) x => P (MkLeft t p) x where
type PP (MkLeft t p) x = PP (MkLeftT t p) x
eval _ = eval (Proxy @(MkLeftT t p))
-- | 'Data.Either.Right' constructor
data MkRight' t p deriving Show
instance ( Show (PP p x)
, P p x
) => P (MkRight' t p) x where
type PP (MkRight' t p) x = Either (PP t x) (PP p x)
eval _ opts x = do
let msg0 = "MkRight"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR NoInline opts msg0 pp [] of
Left e -> e
Right p ->
let d = Right p
in mkNode opts (Val d) (msg0 <> " Right " <> showL opts p) [hh pp]
-- | 'Data.Either.Right' constructor
--
-- >>> pz @(MkRight _ Id) 44
-- Val (Right 44)
--
data MkRight (t :: Type) p deriving Show
type MkRightT (t :: Type) p = MkRight' (Hole t) p
instance P (MkRightT t p) x => P (MkRight t p) x where
type PP (MkRight t p) x = PP (MkRightT t p) x
eval _ = eval (Proxy @(MkRightT t p))
-- | extract the Left value from an 'Either' otherwise use the default value: similar to 'Data.Either.fromLeft'
--
-- if there is no Left value then @p@ is passed the Right value and the whole context
--
-- >>> pz @(LeftDef (1 % 4) Id) (Left 20.4)
-- Val (102 % 5)
--
-- >>> pz @(LeftDef (1 % 4) Id) (Right "aa")
-- Val (1 % 4)
--
-- >>> pz @(LeftDef (PrintT "found right=%s fst=%d" '(Fst,L21)) Snd) (123,Right "xy")
-- Val "found right=xy fst=123"
--
-- >>> pz @(LeftDef (MEmptyT _) Id) (Right 222)
-- Val ()
--
-- >>> pz @(LeftDef (MEmptyT (SG.Sum _)) Id) (Right 222)
-- Val (Sum {getSum = 0})
--
data LeftDef p q deriving Show
instance ( PP q x ~ Either a b
, PP p (b,x) ~ a
, P q x
, P p (b,x)
) => P (LeftDef p q) x where
type PP (LeftDef p q) x = LeftT (PP q x)
eval _ opts x = do
let msg0 = "LeftDef"
qq <- eval (Proxy @q) opts x
case getValueLR NoInline opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Left a -> pure $ mkNode opts (Val a) (msg0 <> " Left") [hh qq]
Right b -> do
pp <- eval (Proxy @p) opts (b,x)
pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (Val p) (msg0 <> " Right") [hh qq, hh pp]
-- | extract the Right value from an 'Either': similar to 'Data.Either.fromRight'
--
-- if there is no Right value then @p@ is passed the Left value and the whole context
--
-- >>> pz @(RightDef (1 % 4) Id) (Right 20.4)
-- Val (102 % 5)
--
-- >>> pz @(RightDef (1 % 4) Id) (Left "aa")
-- Val (1 % 4)
--
-- >>> pz @(RightDef (PrintT "found left=%s fst=%d" '(Fst,L21)) Snd) (123,Left "xy")
-- Val "found left=xy fst=123"
--
-- >>> pz @(RightDef (MEmptyT _) Id) (Left 222)
-- Val ()
--
-- >>> pz @(RightDef (MEmptyT (SG.Sum _)) Id) (Left 222)
-- Val (Sum {getSum = 0})
--
data RightDef p q deriving Show
instance ( PP q x ~ Either a b
, PP p (a,x) ~ b
, P q x
, P p (a,x)
) => P (RightDef p q) x where
type PP (RightDef p q) x = RightT (PP q x)
eval _ opts x = do
let msg0 = "RightDef"
qq <- eval (Proxy @q) opts x
case getValueLR NoInline opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Right b -> pure $ mkNode opts (Val b) (msg0 <> " Right") [hh qq]
Left a -> do
pp <- eval (Proxy @p) opts (a,x)
pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (Val p) (msg0 <> " Left") [hh qq, hh pp]
-- | extract the Left value from an 'Either' otherwise fail with a message
--
-- if there is no Left value then @p@ is passed the Right value and the whole context
--
-- >>> pz @(LeftFail "oops" Id) (Left 20.4)
-- Val 20.4
--
-- >>> pz @(LeftFail "oops" Id) (Right "aa")
-- Fail "oops"
--
-- >>> pz @(LeftFail (PrintT "found right=%s fst=%d" '(Fst,L21)) Snd) (123,Right "xy")
-- Fail "found right=xy fst=123"
--
-- >>> pz @(LeftFail (MEmptyT _) Id) (Right 222)
-- Fail ""
--
-- >>> pl @(LeftFail (PrintF "someval=%d" L21) Snd) (13::Int,Right @(SG.Sum Int) "abc")
-- Error someval=13 (LeftFail Right)
-- Fail "someval=13"
--
-- >>> pl @(LeftFail (PrintF "someval=%s" Fst) Id) (Right @(SG.Sum Int) "abc")
-- Error someval=abc (LeftFail Right)
-- Fail "someval=abc"
--
-- >>> pl @(LeftFail (PrintF "found rhs=%d" Fst) Id) (Right @String @Int 10)
-- Error found rhs=10 (LeftFail Right)
-- Fail "found rhs=10"
--
-- >>> pl @(LeftFail (PrintF "found rhs=%d" (Snd >> L22)) L21) ('x',(Right 10,23))
-- Error found rhs=23 (LeftFail Right)
-- Fail "found rhs=23"
--
-- >>> pl @(LeftFail (PrintF "found rhs=%d" (L2 L22)) L21) ('x',(Left "abc",23))
-- Present "abc" (Left)
-- Val "abc"
--
data LeftFail p q deriving Show
instance ( PP p (b,x) ~ String
, PP q x ~ Either a b
, P p (b,x)
, P q x
)
=> P (LeftFail p q) x where
type PP (LeftFail p q) x = LeftT (PP q x)
eval _ opts x = do
let msg0 = "LeftFail"
qq <- eval (Proxy @q) opts x
case getValueLR NoInline opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Left a -> pure $ mkNode opts (Val a) "Left" [hh qq]
Right b -> do
pp <- eval (Proxy @p) opts (b,x)
pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (Fail p) (msg0 <> " Right") [hh qq, hh pp]
-- | extract the Right value from an 'Either' otherwise fail with a message
--
-- if there is no Right value then @p@ is passed the Left value and the whole context
--
-- >>> pz @(RightFail "oops" Id) (Right 20.4)
-- Val 20.4
--
-- >>> pz @(RightFail "oops" Id) (Left "aa")
-- Fail "oops"
--
-- >>> pz @(RightFail (PrintT "found left=%s fst=%d" '(Fst,L21)) Snd) (123,Left "xy")
-- Fail "found left=xy fst=123"
--
-- >>> pz @(RightFail (MEmptyT _) Id) (Left 222)
-- Fail ""
--
data RightFail p q deriving Show
instance ( PP p (a,x) ~ String
, PP q x ~ Either a b
, P p (a,x)
, P q x
)
=> P (RightFail p q) x where
type PP (RightFail p q) x = RightT (PP q x)
eval _ opts x = do
let msg0 = "RightFail"
qq <- eval (Proxy @q) opts x
case getValueLR NoInline opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Right b -> pure $ mkNode opts (Val b) "Right" [hh qq]
Left a -> do
pp <- eval (Proxy @p) opts (a,x)
pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (Fail p) (msg0 <> " Left") [hh qq, hh pp]