This file shows how similar existential types are vs. sigma types (dependent pairs).

existential-vs-sigma.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

module VectStuff20 where

import Data.Constraint (Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import GHC.Natural (Natural)
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.Decide
       ((:~:)(Refl), Decision(Disproved, Proved), Refuted, (%~))
import Data.Singletons.Sigma (Sigma((:&:)))
import Data.Singletons.TypeLits (KnownNat, Nat, Sing(SNat))
import Unsafe.Coerce (unsafeCoerce)

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

deriving instance Show a => Show (Vect a n)

plusMinus1Law :: forall (n :: Nat) m. n :~: ((n - m) + m)
plusMinus1Law = unsafeCoerce Refl

data Magic = Magic Natural

natToSing :: forall (n :: Nat). Natural -> Sing n
natToSing = unsafeCoerce Magic

gtZeroMinusNat :: Sing n -> Refuted (n :~: 0) -> Sing (n - 1)
gtZeroMinusNat sNat _ = natToSing (fromSing sNat - 1)

replicateVect :: forall n a. Sing n -> a -> Vect a n
replicateVect sNatN a =
  case sNatN %~ (sing @_ @0) of
    Proved Refl -> VNil
    Disproved f ->
      case plusMinus1Law @n @1 of
        Refl ->
          case gtZeroMinusNat sNatN f of
            snatNMinus1 -> VCons a $ replicateVect snatNMinus1 a

testReplicateVect :: Vect String 3
testReplicateVect = replicateVect (sing @_ @3) "hello"

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

deriving instance Show a => Show (SomeVect a)

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

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

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

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

existentialToSigma :: forall a. SomeVect a -> Sigma Nat (TyCon (Vect a))
existentialToSigma (SomeVect (vect :: Vect a n)) = sing :&: vect

sigmaToExistential :: Sigma Nat (TyCon (Vect a)) -> SomeVect a
sigmaToExistential (SNat :&: vect) = SomeVect vect

-- | Generalized existential type.
data Ex :: (k -> Type) -> Type where
  Ex :: a i -> Ex a

replicateGenExistentialVect :: forall n a. Natural -> a -> Ex (Vect a)
replicateGenExistentialVect nat a =
  case toSing nat of
    SomeSing sNat -> Ex $ replicateVect sNat a

testReplicateGenExistentialVect :: IO ()
testReplicateGenExistentialVect =
  case replicateGenExistentialVect 3 "hello" of
    Ex vect -> print vect

This can be loaded into ghci with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package singletons --package constraints