When to use existential type vs. dependent pair in Haskell?

Question

When would one want to use a specialized existential type vs. a dependent pair (also called a dependent sum or sigma type)?

Here is an example.

The following is a length-indexed list and dependently-typed replicate function. See this other question for how to implement replicateVect. The following is using the singletons library:

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

replicateVect :: forall n a. SNat n -> a -> Vect a n

There are (at least) two possible ways to create a replicate function that takes a normal Natural, instead of a singleton SNat.

One way is to create a specialized existential type for Vect. I call this SomeVect, following the conventions of singletons:

data SomeVect :: Type -> Type where
  SomeVect :: forall a n. Vect a n -> SomeVect a

replicateExistentialVect :: forall a. Natural -> a -> SomeVect a
replicateExistentialVect nat a =
  case toSing nat of
    SomeSing sNat -> SomeVect $ replicateVect sNat a

Another way is to use a dependent pair. This uses the Sigma type from singletons:

replicateSigmaVect :: forall n a. Natural -> a -> Sigma Nat (TyCon (Vect a))
replicateSigmaVect nat a =
  case toSing nat of
    SomeSing sNat -> sNat :&: replicateVect sNat a

These functions looks very similar. Using replicateExistentialVect and replicteSigmaVect is also very similar:

testReplicateExistentialVect :: IO ()
testReplicateExistentialVect =
  case replicateExistentialVect 3 "hello" of
    SomeVect vect -> print vect

testReplicateSigmaVect :: IO ()
testReplicateSigmaVect =
  case replicateSigmaVect 3 "hello" of
    _ :&: vect -> print vect

The full code can be found here.

---

This brings me to my questions.

1. When should I use a specialized existential type (like SomeVect) vs. a dependent pair (like Sigma)?
2. Are there any functions that can only be written with one or the other?
3. Are there any functions that are significantly easier to write with one or the other?

Answer 1

1. When should I use a specialized existential type (like SomeVect) vs. a dependent pair (like Sigma)?

This question is somewhat tricky to answer, because:

1. Sigma is itself a form of specialized existential type.
2. There are infinitely many ways to create specialized existential types—SomeVect and Sigma are just two examples of the phenomenon.

Nevertheless, it does feel as if Sigma is subtly different from other ways of encoding existential types in GHC. Let's try and identify what exactly makes it different.

First, let's write out the definition of Sigma, in its full glory:

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

And for comparison, I'll also define a "typical" existential type:

    data Ex :: (s -> Type) -> Type where
      MkEx :: forall s (t :: s -> Type) (x :: s).
              t x -> Ex t

Let's go over the differences between the two:

1. Sigma s t has two type arguments, whereas Ex t only has one. This isn't a terribly significant difference, and in fact, you could write Sigma using only one argument:

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

   Or Ex using two arguments:

   data Ex (s :: Type) :: (s -> Type) -> Type where
     MkEx :: forall s (t :: s -> Type) (x :: s).
             t x -> Ex s t
   

   The only reason why I opted to use two arguments in Sigma is to more closely match the presentation of dependent pairs in other languages, such as in Idris's DPair. It also perhaps makes the analogy between Sigma s t and ∃ (x ∈ s). t(x) clearer.

2. Much more importantly, the kind of Sigma's last argument, s ~> Type, is different from the kind of Ex's argument, s -> Type. In particular, the difference is between the (~>) and (->) kinds. The latter, (->) is the familiar function arrow, whereas the former, (~>), is the kind of defunctionalization symbols in singletons.

   What are defunctionalization symbols, and why do they need their own kind? They're explained in section 4.3 of the paper Promoting Functions to Type Families in Haskell, but I'll try to give a condensed version here. Essentially, we want to be able to write type families like:

   type family Positive (n :: Nat) :: Type where
     Positive Z     = Void
     Positive (S _) = ()
   

   And be able to use the type Sigma Nat Positive. But this won't work, since you can't partially apply a type family like Positive. Luckily, the defunctionalization trick lets us work around this issue. Using the following definitions:

   data TyFun :: Type -> Type -> Type
   
   type a ~> b = TyFun a b -> Type
   infixr 0 ~>
   
   type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
   

   We can define a defunctionalization symbol for Positive that lets us partially apply it:

   data PositiveSym0 :: Nat ~> Type
   type instance Apply PositiveSym0 n = Positive n
   

   Now, in the type Sigma Nat PositiveSym0, the second field is of type Apply PositiveSym0 x, or just Positive x. Thus, (~>) is in some sense more general than (->), since it lets us use more types than (->) would.

   (If it helps, one can think of (~>) as the kind of unmatchable functions, as described in Section 4.2.4 of Richard Eisenberg's thesis, whereas (->) is the kind of matchable functions.)

3. While the MkEx constructor only has one field, the (:&:) constructor has an additional field (of type Sing x). There are two reasons for this. One is that storing this extra field is, by definition, part of what makes Sigma a dependent pair, and this allows us to retrieve it by way of the projSigma1 function. Another reason is that if you took out the Sing x field:

   data Sigma (s :: Type) :: (s ~> Type) -> Type where
     (:&:) :: forall s (t :: s ~> Type) (x :: s).
              Apply t x -> Sigma s t
   

   Then this definition would require AllowAmbiguousTypes, as the x type variable is ambiguous. This might be burdensome, so having an explicit Sing x field avoids this.

---

Now that I've finished my long-winded explanation, let me try to actually answer your questions:

1. When should I use a specialized existential type (like SomeVect) vs. a dependent pair (like Sigma)?

I think this is ultimately a matter of personal taste. Sigma is nice because it's pretty darn general, but you may find that defining a specialized existential type makes your code easier to understand. (But also see the caveats below.)

2. Are there any functions that can only be written with one or the other?

I suppose my earlier Sigma Nat PositiveSym0 example would count as something you couldn't do with Ex, since it requires exploiting the (~>) kind. On the other hand, you could just as well define:

data SomePositiveNat :: Type where
  SPN :: Sing (n :: Nat) -> Positive n -> SomePositiveNat

So you'd don't technically need (~>) to do this.

Additionally, I don't know of a way to write a projSigma1 equivalent for Ex, since it doesn't store enough information in order to be able to write this.

On the other hand, Sigma s t requires that there be a Sing instance for the kind s, so if there isn't one, Sigma is probably not going to work.

3. Are there any functions that are significantly easier to write with one or the other?

You'll have an easier time using Sigma when you have a pressing need to use something with a (~>) kind, since that is where it shines. If your type can get away with just a (->) kind, it might be more convenient to use a "typical" existential type like Ex, because otherwise you have to introduce noise in the form of TyCon to lift something of kind s -> Type to s ~> Type.

Also, you might find Sigma easier to work with if being able to retrieve the field of type Sing x conveniently is important.