Let’s say I have the following type: import Test.QuickCheck import GHC.TypeLits import Data.Kind data Vect :: Nat -> Type -> Type where VNil :: Vect 0 a VCons :: a -> Vect n a -> Vect (n + 1) a I want to be able to write some QuickChecks about my values, so I want to write an Arbitrary instance. sizedVect :: Int -> Gen a -> Gen (Vect n a) sizedVect 0 _ = pure VNil sizedVect n g = VCons <$> g <*> sizedVect (n - 1) g instance Arbitrary (Vect n a) where arbitrary :: Gen (Vect n a) arbi...| Haskell Community
To explain these concepts in more detail, you want a Sigma type (n :: Nat, Vect (n :: Nat) a) But we don’t have those in Haskell. Instead you can have a second class existential type by writing it as a GADT: data SomeVect a where SomeVect :: (n :: Nat) -> Vect (n :: Nat) a -> SomeNat a -- ^ This is not yet valid Haskell! But we don’t have dependent types either! Instead there is a singleton type SNat :: Nat -> Type that does a similar job. It’s called a “singleton” because there is ...| Haskell Community