# 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:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![Agnishom](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/agnishom/32/2108_2.png) [@Agnishom](https://discourse.haskell.org/u/Agnishom)\
**Post date:** [July 13, 2023, 9:19am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/1 "2023-07-13T09:19:43Z")

</div>

Let’s say I have the following type:

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

```haskell
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)
  arbitrary = sized sizedVect

```

But it doesn’t work because, e.g, `VNil` does not have the type `forall n . Vect n a`, but `Vect 0 a`.

Perhaps I should be able to write something like this:

```haskell
sizedVect :: (n :: Nat) -> Gen a -> Gen (Vect (n :: Nat) a)
arbitrary :: Gen (n :: Nat, Vect (n :: Nat) a)

```

This is like a Sigma type, but it is not clear to me how to write this type in Haskell syntax (and then how to write the QuickCheck tests)

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [July 13, 2023, 9:48am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/2 "2023-07-13T09:48:41Z")

</div>

I don’t think this helps with answering your question for Haskell, but my colleague wrote a paper about how to do it generically in Agda:

[![](https://img.youtube.com/vi/xOvBBQthm9s/maxresdefault.jpg "[ICFP'22] A Completely Unique Account of Enumeration") ](https://www.youtube.com/watch?v=xOvBBQthm9s)

> **[A completely unique account of enumeration | Proceedings of the ACM on...](https://dl.acm.org/doi/10.1145/3547636)**
>
> How can we enumerate the inhabitants of an algebraic datatype? This paper explores
> a datatype generic solution that works for all regular types and indexed families. The enumerators presented here are provably both complete and unique—they will ...

---

<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, 9:49am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/3 "2023-07-13T09:49:12Z")

</div>

How about

```haskell
data SomeVect a where
    SomeVect :: SNat n -> Vect n a -> SomeVect a

arbitrary :: Arbitrary a => Gen (SomeVect a)

```

---

<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:11am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/5 "2023-07-13T10:11:08Z")

</div>

Here’s a more complete solution. Does it do what you want?

```haskell
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}

import Test.QuickCheck
import Data.Reflection
import GHC.TypeLits
import Data.Kind
import Data.Proxy

data SomeVect a where
    SomeVect :: KnownNat n => Vect n a -> SomeVect a

example :: Arbitrary a => Gen (SomeVect a)
example = do
  i <- arbitrary
  reifyNat i $ \(_ :: Proxy n) -> do
    v <- replicateV @n arbitrary
    pure (SomeVect v)

----

data Vect (n :: Nat) (a :: Type) where

replicateV :: forall n m a. Monad m => m a -> m (Vect n a)
replicateV = undefined

```

---

<div class="post-metadata">

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

</div>

Interesting. This is probably harder than I thought.

What is `SNat n`? And also what is `KnownNat n`? What user tomjaguarpaw seems very much like Sigma types but with these additional constructs.

I am not really sure what the connection with the enumeration concept here is. I watched about 5 minutes of the video. Also, shouldn’t it be relatively easy to express Sigma types in Agda since it is a language with first class support for dependent types.

---

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

---

<div class="post-metadata">

**Author:** ![Agnishom](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/agnishom/32/2108_2.png) [@Agnishom](https://discourse.haskell.org/u/Agnishom)\
**Post date:** [July 14, 2023, 3:12am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/8 "2023-07-14T03:12:15Z")

</div>

Thanks for explaining.

I am still trying to wrap my head around the `KnownNat` constraint. What exactly is known about it?

Consider the following code. How do I make it typecheck?

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

data SomeVect a where
    SomeVect :: KnownNat n => Vect n a -> SomeVect a

someVectCons :: a -> SomeVect a -> SomeVect a
someVectCons x (SomeVect xs) = SomeVect $ VCons x xs

```

The compiler says:

```haskell
• Could not deduce (KnownNat (n + 1))
    arising from a use of ‘SomeVect’
  from the context: KnownNat n
    bound by a pattern with constructor:
               SomeVect :: forall (n :: Nat) a.
                           KnownNat n =>
                           Vect n a -> SomeVect a,
             in an equation for ‘someVectCons’
    at /Users/agnishom/code/stl-workspace/server/src/PatternMatching/MITL.hs:96:17-27
• In the first argument of ‘($)’, namely ‘SomeVect’
  In the expression: SomeVect $ VCons x xs
  In an equation for ‘someVectCons’:
      someVectCons x (SomeVect xs) = SomeVect $ VCons x xs

```

If n is Known, shouldn’t n + 1 be so as well?

---

<div class="post-metadata">

**Author:** ![Agnishom](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/agnishom/32/2108_2.png) [@Agnishom](https://discourse.haskell.org/u/Agnishom)\
**Post date:** [July 14, 2023, 3:33am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/9 "2023-07-14T03:33:43Z")

</div>

> [@tomjaguarpaw](#):
>
> ```haskell
> data Vect (n :: Nat) (a :: Type) where
> 
> replicateV :: forall n m a. Monad m => m a -> m (Vect n a)
> replicateV = undefined
> 
> ```

Also, how would you actually define replicateV? I would need to pattern match on `n`, but it isn’t actually available

---

<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 14, 2023, 7:07am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/10 "2023-07-14T07:07:44Z")

</div>

> [@Agnishom](#):
>
> I would need to pattern match on `n`, but it isn’t actually available

Ah, that probably needs a `KnownNat` constraint too. `KnownNat n =>` is exactly what allows you to pattern match on `n`.

---

<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 14, 2023, 7:08am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/11 "2023-07-14T07:08:19Z")

</div>

> [@Agnishom](#):
>
> I am still trying to wrap my head around the `KnownNat` constraint. What exactly is known about it?

What’s known about it is its runtime representation, so you can pattern match/branch on it.

---

<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 14, 2023, 7:10am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/12 "2023-07-14T07:10:14Z")

</div>

> [@Agnishom](#):
>
> If n is Known, shouldn’t n + 1 be so as well?

Yes, you may need a GHC plugin to solve these constraints. I can’t remember which one. Maybe this one:

> **[ghc-typelits-natnormalise](https://hackage.haskell.org/package/ghc-typelits-natnormalise)**
>
> GHC typechecker plugin for types of kind GHC.TypeLits.Nat

---

<div class="post-metadata">

**Author:** ![Agnishom](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/agnishom/32/2108_2.png) [@Agnishom](https://discourse.haskell.org/u/Agnishom)\
**Post date:** [July 14, 2023, 7:12am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/13 "2023-07-14T07:12:38Z")

</div>

I spent some time reading the blog posts about [Singeltons](https://blog.jle.im/entry/introduction-to-singletons-2.html)

It seems that `KnownNat n =>` and `SNat n -> ` should be the same thing. However, I am confused.

I cannot seem to access the SNat type:

```haskell
ghci> import GHC.TypeNats
ghci> :i Nat
type Nat :: *
type Nat = Natural
        -- Defined in ‘GHC.TypeNats’
ghci> :i SNat

```

I also cannot get the witness from the KnownNat

```haskell
ghci> :i KnownNat 
type KnownNat :: Nat -> Constraint
class KnownNat n where
  GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
  {-# MINIMAL natSing #-}
        -- Defined in ‘GHC.TypeNats’
ghci> :t natSing

<interactive>:1:1: error: Variable not in scope: natSing

```

I imagine that the correct way to write the `replicateV` function would be like `replicateV :: forall n m a. (Monad m, KnownNat n) => m a -> m (Vect n a)` and I probably need to able to pattern match on the SNat witness so that I know how many times to repeat.

---

<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 14, 2023, 7:16am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/14 "2023-07-14T07:16:12Z")

</div>

You probably don’t need the `SNat` itself. You should be able to access all its functionality through `KnownNat`. For example, to pattern match you use

```haskell
natVal :: forall n proxy. KnownNat n => proxy n -> Integer

```

[https://hackage.haskell.org/package/base-4.18.0.0/docs/GHC-TypeLits.html#v:natVal](https://hackage.haskell.org/package/base-4.18.0.0/docs/GHC-TypeLits.html#v:natVal)

---

<div class="post-metadata">

**Author:** ![Agnishom](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/agnishom/32/2108_2.png) [@Agnishom](https://discourse.haskell.org/u/Agnishom)\
**Post date:** [July 14, 2023, 7:19am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/15 "2023-07-14T07:19:40Z")

</div>

What type constructor should I plugin for the variable `proxy`?

---

<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 14, 2023, 7:20am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/16 "2023-07-14T07:20:02Z")

</div>

Easiest to use `Data.Proxy.Proxy`

---

<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 14, 2023, 7:20am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/17 "2023-07-14T07:20:52Z")

</div>

I guess you’ll need an operator that can do a type level `pred` on a `KnownNat` constraint, and I don’t see where that is, but there must be one somewhere …

[EDIT: `pred`, not `succ`]

---

<div class="post-metadata">

**Author:** ![Agnishom](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/agnishom/32/2108_2.png) [@Agnishom](https://discourse.haskell.org/u/Agnishom)\
**Post date:** [July 14, 2023, 7:22am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/18 "2023-07-14T07:22:40Z")

</div>

How would you get the **value** `n :: Int` from the value `Proxy :: Proxy n`?

---

<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 14, 2023, 7:23am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/19 "2023-07-14T07:23:50Z")

</div>

Bind it in the type signature `\(_ :: Proxy n) -> ...`

You’ll need `ScopedTypeVariables` enabled (and exact behaviour may depend on GHC version, I’m not entirely sure.)

EDIT: Oh, to get the `Int` out (or rather `Nat`), just apply `natVal`, quoted [above](http://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/14).

---

<div class="post-metadata">

**Author:** ![hellwolf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/hellwolf/32/3020_2.png) [@hellwolf](https://discourse.haskell.org/u/hellwolf)\
**Post date:** [July 14, 2023, 12:39pm UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/20 "2023-07-14T12:39:05Z")

</div>

~~ignore my gibberish attempt~~

---

<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 14, 2023, 12:43pm UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/21 "2023-07-14T12:43:00Z")

</div>

You probably need to enable a GHC plugin. I don’t know which one, but if you type “ghc plugins for type arithmetic” into your favourite search engine you will probably find some good candidates.

[Next page](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990.md?page=2)