Adding curry/uncurry, leftAdjunct/rightAdjunct

[Icelandjack]

For Data.Singleton.Sigma, these functions witness an isomorphism from Sigma being left adjoint

curry
  :: (Sigma k f -> b)
  -> (forall (a::k). Sing a -> f@@a -> b)
curry kont sing fa = kont (sing :&: fa)

uncurry
  :: (forall (a::k). Sing a -> f@@a -> b)
  -> (Sigma k f -> b)
uncurry kont ((fst :: Sing fst) :&: f_fst) = kont @fst fst f_st

Any interest in adding these with better names? There is also

unit :: Sing a -> f@@a -> Sigma k f
unit = curry id

counit :: Sigma k (ConstSym1 b) -> b
counit = projSigma2 id

[RyanGlScott]

I have no objection to a PR which adds curry or uncurry (although they should probably be named currySigma and uncurrySigma to match the existing naming conventions). There are already a number of existing utility functions in Data.Singleton.Sigma which generalize functions which work over non-dependent pairs, and these functions fit in quite nicely within that space.

I don't see much utility in having unit or counit. unit is just another way to write (:&:), and counit is just a less general version of projSigma2.

[RyanGlScott]

On second thought, I wonder if we should actually wait until (if?) #366 is implemented before going through with this. The reason is that we could actually make the types of currySigma and uncurrySigma more general:

type family Sing :: k -> Type

newtype WrappedSing (a :: k) = WrapSing (Sing a)
newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
  SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
               Sing a -> SWrappedSing ws
type instance Sing = SWrappedSing

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t
data SSigma :: forall s (t :: s ~> Type). Sigma s t -> Type where
  (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst).
            Sing (WrapSing sfst) -> Sing snd -> SSigma (sfst :&: snd :: Sigma s t)
type instance Sing = SSigma

currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
              (forall (p :: Sigma a b). Sing p -> c @@ p)
           -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
                 Sing (WrapSing sx) -> Sing y -> c @@ (sx :&: y))
currySigma f x y = f (x :%&: y)

uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
                (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
                   Sing (WrapSing sx) -> Sing y -> c @@ (sx :&: y))
             -> (forall (p :: Sigma a b). Sing p -> c @@ p)
uncurrySigma f (x :%&: y) = f x y

These more closely resemble how these functions are defined in Agda:

curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
        ((p : Σ A B) → C p) →
        ((x : A) → (y : B x) → C (x , y))
curry f x y = f (x , y)

uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
          ((x : A) → (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f (x , y) = f x y