# How to create Arbitrary instance for dependent types?

**URL:** <https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990>\
**Category:** Learn\
**Created:** [July 13, 2023, 9:19am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990 "2023-07-13T09:19:42Z")\
**Posts on this page:** 1\
**Showing post:** 7

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [July 13, 2023, 10:52am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/7 "2023-07-13T10:52:11Z")

</div>

To explain these concepts in more detail, you want a Sigma type

```haskell
(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:

```haskell
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

```haskell
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

```haskell
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.

---

_[View the full topic](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990)._