{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Data.Parameterized.Pair
( Pair(..)
, fstPair
, sndPair
, viewPair
) where
import Data.Parameterized.Classes
import Data.Parameterized.Some
import Data.Parameterized.TraversableF
data Pair (a :: k -> *) (b :: k -> *) where
Pair :: !(a tp) -> !(b tp) -> Pair a b
instance (TestEquality a, EqF b) => Eq (Pair a b) where
Pair xa xb == Pair ya yb =
case testEquality xa ya of
Just Refl -> eqF xb yb
Nothing -> False
instance FunctorF (Pair a) where
fmapF f (Pair x y) = Pair x (f y)
instance FoldableF (Pair a) where
foldMapF f (Pair _ y) = f y
foldrF f z (Pair _ y) = f y z
fstPair :: Pair a b -> Some a
fstPair (Pair x _) = Some x
sndPair :: Pair a b -> Some b
sndPair (Pair _ y) = Some y
viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c
viewPair f (Pair x y) = f x y