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

Defunctionalization is a general way to work around the lack of first-class functions (in fact, it was originally discovered as a compilation technique to get rid of those), encoding them as symbols that get interpreted by a single first-order Apply function.

For example, your Foo a b is a symbol that encodes the function \n -> a n b.

---

Another way of obtaining an equivalent symbol is to follow the intuition that (\n -> a n b) = flip a b.

Note that type constructors like Vec are not themselves symbols that can be passed to Apply, but must be wrapped in "symbol constructors": TyCon2 Vec is the symbol for \n -> \b -> Vec n b.

singletons has a symbol for flip, FlipSym0 (symbols can stand for higher-order functions by taking other symbols as arguments).

Foo a b = Apply (Apply FlipSym0 (TyCon2 a)) b

Note that partial applications reduce to other symbols:

        = Apply (FlipSym1 (TyCon2 a)) b
        = FlipSym2 (TyCon2 a) b

---

The TyFun type is a way to give types to defunctionalized symbols. The main benefit I see is type inference; without it, type families might get stuck in confusing ways.

See also this blogpost by Richard Eisenberg on defunctionalization for Haskell types: https://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/

Answer 2

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.