How to create Arbitrary instance for dependent types?

Learn
#1

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)
  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:

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)

#2

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:

#3

How about

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

arbitrary :: Arbitrary a => Gen (SomeVect a)
1 Like
#5

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

{-# 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
4 Likes
#6

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.

#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
How to create quickcheck tests for dependently typed matrix addition without specifying each dimension statically?
#8

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?

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:

• 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?

#9

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

#10

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

1 Like
#11

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

#12

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

#13

I spent some time reading the blog posts about Singeltons

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:

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

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.

#14

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

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

#15

What type constructor should I plugin for the variable proxy?

#16

Easiest to use Data.Proxy.Proxy

#17

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]

#18

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

#19

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.

#20

ignore my gibberish attempt

#21

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.