{-|
Description : A 2-tuple with identically parameterized elements
Copyright   : (c) Galois, Inc 2017-2019

This module defines a 2-tuple where both elements are parameterized over the
same existentially quantified parameter.

-}
{-# 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

-- | Like a 2-tuple, but with an existentially quantified parameter that both of
-- the elements share.
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 a tp
xa b tp
xb == :: Pair a b -> Pair a b -> Bool
== Pair a tp
ya b tp
yb =
    case a tp -> a tp -> Maybe (tp :~: tp)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality a tp
xa a tp
ya of
      Just tp :~: tp
Refl -> b tp -> b tp -> Bool
forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
eqF b tp
xb b tp
b tp
yb
      Maybe (tp :~: tp)
Nothing -> Bool
False

instance FunctorF (Pair a) where
  fmapF :: (forall (x :: k). f x -> g x) -> Pair a f -> Pair a g
fmapF forall (x :: k). f x -> g x
f (Pair a tp
x f tp
y) = a tp -> g tp -> Pair a g
forall k (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair a tp
x (f tp -> g tp
forall (x :: k). f x -> g x
f f tp
y)

instance FoldableF (Pair a) where
  foldMapF :: (forall (s :: k). e s -> m) -> Pair a e -> m
foldMapF forall (s :: k). e s -> m
f (Pair a tp
_ e tp
y) = e tp -> m
forall (s :: k). e s -> m
f e tp
y
  foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Pair a e -> b
foldrF forall (s :: k). e s -> b -> b
f b
z (Pair a tp
_ e tp
y) = e tp -> b -> b
forall (s :: k). e s -> b -> b
f e tp
y b
z

-- | Extract the first element of a pair.
fstPair :: Pair a b -> Some a
fstPair :: Pair a b -> Some a
fstPair (Pair a tp
x b tp
_) = a tp -> Some a
forall k (f :: k -> *) (x :: k). f x -> Some f
Some a tp
x

-- | Extract the second element of a pair.
sndPair :: Pair a b -> Some b
sndPair :: Pair a b -> Some b
sndPair (Pair a tp
_ b tp
y) = b tp -> Some b
forall k (f :: k -> *) (x :: k). f x -> Some f
Some b tp
y

-- | Project out of Pair.
viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c
viewPair :: (forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
viewPair forall (tp :: k). a tp -> b tp -> c
f (Pair a tp
x b tp
y) = a tp -> b tp -> c
forall (tp :: k). a tp -> b tp -> c
f a tp
x b tp
y