How to use the dependent pair type Sigma from the singletons library?

Question

How can the dependent pair type Sigma from the singletons library be used?

Let's assume the following type-indexed list and replicate function exist:

data Vect :: Nat -> Type -> Type where
  VNil :: Vect 0 a
  VCons :: a -> Vect n a -> Vect (n + 1) a

replicateVec :: forall n a. Sing n -> a -> Vect n a

(You can find a couple different implementations of replicateVec in this question).

I'd like to create a function replicateVecSigma that returns a Vect in a dependent pair. Ideally it would be like the following:

replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)

How can Sigma be used to write this function? And how can the type of the function be written?

---

Actually, I am able to implement replicateVecSigma as follows but it doesn't seem very clean:

data Foo a b (m :: TyFun Nat Type)

type instance Apply (Foo a b) (n :: Nat) = a n b

replicateVecSigma :: Natural -> Sigma Nat (Foo Vect String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

It seems unfortunate that I have to declare this Foo type and Apply instance just to use Sigma. Does the singletons library provide any way to make working with Sigma easier?

You can find my full code here.

---

For completeness, here is the definition of Sigma:

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t

Here is ~>:

type a ~> b = TyFun a b -> *

data TyFun :: * -> * -> *

instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

type instance Demote (k1 ~> k2) = Demote k1 -> Demote k2

class SingKind k where
  type family Demote k :: * = r | r -> k
  fromSing :: forall (a :: k). Sing a -> Demote k
  toSing :: Demote k -> SomeSing k

Here is @@:

type a @@ b = Apply a b

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

singletons defines a bunch of instances for Apply.

How do TyFun and Apply work?

---

Here are the three questions from above:

1. How can I use Sigma to write a function like replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)?
2. I am able to write replicateVecSigma using the Foo type above, but it seems like too much extra work. Is there an easier way?
3. How do TyFun and Apply work?

Answer 1

In this specific case, we want to compute the type-level lambda

\n -> Vect n String

Unfortunately, we do not have lambdas at the type level. At most, we can define type families, as the OP did. However, we can rewrite the lambda in pointfree style:

\n -> flip Vect String n    -- pseudocode
flip Vect String

and we can turn this idea into an actual type, using the singletons type-level Flip type function. Here, we want to partially apply Flip with two arguments (it takes three, in a saturated call), so we use the "defunctionalized" FlipSym2 variant instead.

This compiles:

replicateVecSigma :: Natural -> Sigma Nat (FlipSym2 (TyCon Vect) String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

If we had the n argument in the last position from the beginning, we could have avoided the Flip.

data Vect2 :: Type -> Nat -> Type where
  VNil2 :: Vect2 a 0
  VCons2 :: a -> Vect2 a n -> Vect2 a (n + 1)

replicateVec2 :: forall n a. Sing n -> a -> Vect2 a n
replicateVec2 = undefined

replicateVecSigma2 :: Natural -> Sigma Nat (TyCon (Vect2 String))
replicateVecSigma2 i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec2 snat "hello"

( TyCon Vect2 @@ String also works here, using the explicit application @@ at the defunctionalized level, instead of the actuall type applciation.)

Very roughly put, you can think of the defunctionalized variants like FlipSym0, FlipSym1, FlipSym2 as basic tags (not functions!), with no intrinsic meaning, except for the fact that Apply lets you work with them pretending they were functions. In this way we can work with non-functions ("tags") as if they were functions. This is needed since, in Haskell, we do not have functions at the type level, so we have to work with these "pretend" versions.

The approach is general, but it does require more work from the programmer than one would like.

I am not aware of any Template Haskell utility that can automatically turn type-level lambdas into pointfree form, and then defunctionalize them. That would be quite useful.