1
{-# LANGUAGE TupleSections, GeneralizedNewtypeDeriving, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
2
3
module Agda.Utils.Tuple where
5
import Control.Applicative
8
import Data.Traversable
5
11
infix 3 /\ -- backslashes at EOL interacts badly with CPP...
13
-- | Bifunctoriality for pairs.
7
14
(-*-) :: (a -> c) -> (b -> d) -> (a,b) -> (c,d)
8
(f -*- g) (x,y) = (f x, g y)
15
(f -*- g) ~(x,y) = (f x, g y)
17
-- | @mapFst f = f -*- id@
18
mapFst :: (a -> c) -> (a,b) -> (c,b)
19
mapFst f ~(x,y) = (f x, y)
21
-- | @mapSnd g = id -*- g@
22
mapSnd :: (b -> d) -> (a,b) -> (a,d)
23
mapSnd g ~(x,y) = (x, g y)
10
26
(/\) :: (a -> b) -> (a -> c) -> a -> (b,c)
11
27
(f /\ g) x = (f x, g x)
29
-- * Triple (stolen from Data.Tuple.HT)
43
{-# INLINE uncurry3 #-}
13
44
uncurry3 :: (a -> b -> c -> d) -> (a,b,c) -> d
14
uncurry3 f (x,y,z) = f x y z
45
uncurry3 f ~(x,y,z) = f x y z
47
uncurry4 :: (a -> b -> c -> d -> e) -> (a,b,c,d) -> e
48
uncurry4 f ~(w,x,y,z) = f w x y z
50
-- | Monadic version of '-*-'.
51
mapPairM :: (Applicative m) => (a -> m c) -> (b -> m d) -> (a,b) -> m (c,d)
52
mapPairM f g ~(a,b) = (,) <$> f a <*> g b
54
-- | Monadic 'mapFst'.
55
mapFstM :: (Applicative m) => (a -> m c) -> (a,b) -> m (c,b)
56
mapFstM f ~(a,b) = (,b) <$> f a
58
-- | Monadic 'mapSnd'.
59
mapSndM :: (Applicative m) => (b -> m d) -> (a,b) -> m (a,d)
60
mapSndM f ~(a,b) = (a,) <$> f b
62
newtype List2 a = List2 { list2 :: (a,a) }
63
deriving (Eq, Functor, Foldable, Traversable)