How to create Arbitrary instance for dependent types?

Learn
7

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 one value of type SNat n for each literal type n :: Natural. Using SNat we can write the desired Sigma type equivalent as

data SomeVect a where
    SomeVect :: SNat (n :: Nat) -> Vect (n :: Nat) a -> SomeNat a
    -- ^ This is now valid Haskell

For convenience there is a class KnownNat (n :: Nat) where natSing :: SNat n. This makes the above type equivalent to

data SomeVect a where
    SomeVect :: KnownNat (n :: Nat) => Vect (n :: Nat) a -> SomeNat a

In order to reify a value level Nat (or Integer) to a type level Nat we need to use reifyNat. That is we pass in an i :: Integer (actually I should have put a guard that it is non-negative) and we “get out” a type level n :: Nat.

I’ve never used Agda, but I guess in Agda SNat vanishes and reifyNat is roughly just function application.

5 Likes