Quickchecking a property about length indexed lists

3
votes

I'm trying to use QuickCheck to test properties about length-indexed lists (a.k.a vectors) in Haskell. My trouble is that GHC is complaining about an ambiguous variable appearing on a Show constraint on main function.

I've defined vectors in a standard way

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
   Nil :: Vec 'Z a
   (:>) :: a -> Vec n a -> Vec ('S n) a

vlength :: Vec n a -> Int
vlength Nil = 0
vlength (_ :> xs) = 1 + vlength xs

and I have defined a function that converts it to a list

toList :: Vec n a -> [a]
toList Nil = []
toList (x :> xs) = x : (toList xs)

such conversion function should preserve length, that has an immediate encoding as a property:

toList_correct :: Show a => Vec n a -> Bool
toList_correct v = vlength v == length (toList v)

I've defined Arbitrary instances for Vec as:

instance (Show a, Arbitrary a) => Arbitrary (Vec 'Z a) where
   arbitrary = return Nil

instance (Show a, Arbitrary a, Arbitrary (Vec n a)) => Arbitrary (Vec ('S n) a) where
   arbitrary
      = (:>) <$> arbitrary <*> arbitrary

The trouble happens when I call the quickCheck function on main:

main :: IO ()
main = quickCheck toList_correct

and GHC gives me the following message:

 Ambiguous type variable ‘a0’ arising from a use of ‘quickCheck’
  prevents the constraint ‘(Show a0)’ from being solved.
  Probable fix: use a type annotation to specify what ‘a0’ should be.
  These potential instances exist:
    instance [safe] Show Args -- Defined in ‘Test.QuickCheck.Test’
    instance [safe] Show Result -- Defined in ‘Test.QuickCheck.Test’
    instance (Show a, Show b) => Show (Either a b)
      -- Defined in ‘Data.Either’
    ...plus 27 others
    ...plus 65 instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)
• In the expression: quickCheck toList_correct
  In an equation for ‘main’: main = quickCheck toList_correct

I have no idea on how could I fix this error. Any tip is highly welcome.

The complete code is available here.

1
haskelldependent-typequickcheck

1 Answers

4
votes

There are two instances of the same problems here. The first instance is the one causing the error message. The second instance shows up only after you solve the first problem, and will be much harder to solve.

The error message comes from a common problem when your types are too general. A simpler example of the same error is the function:

-- Ambiguous type variable ‘a0’ arising from a use of ‘read’
showRead :: String -> String
showRead = show . read

In a nutshell, GHC knows that there is an intermediate value of some type a you will create (with read :: Read a => String -> a) which you then immediately convert back to a String (with show :: Show a => a -> String). The problem is that to run this, GHC does need to know what is the type of the thing you are reading and showing - yet it has no way of figuring that out.

The type variable a is ambiguous

GHC is telling you it has no way of telling vectors of what type you want quickCheck to be testing against when it uses toList_correct. One fix is to add a type annotation (or use TypeApplications) and tell GHC what type of vector you want:

    quickCheck (toList_correct :: Vec n () -> Bool)

The type variable n is ambiguous

However, not only is a ambiguous, so is n! Because you are encoding into the type of the vector its length, you will only be able to quickcheck your property for vectors of a particular length. The easy fix is to settle on a particular length (or several lengths).

    quickCheck (toList_correct :: Vec Z () -> Bool)
    quickCheck (toList_correct :: Vec (S Z) () -> Bool)
    quickCheck (toList_correct :: Vec (S (S Z)) () -> Bool)

That said, this feels (and so it should) a bit pointless - you want to test vectors of any length. The solution to this is to make an existential type BoxVector around your vector:

    data BoxVector a where
      box :: Vec n a -> BoxVector a

    deriving instance Show a => Show (BoxVector a)

Now that we have this existential type, we can make an Arbitrary instance of it which is arbitrary even over the length of the vector:

    instance (Show a, Arbitrary a) => Arbitrary (BoxVector a) where
      arbitrary = fromList <$> arbitrary
        where
          fromList :: [a] -> BoxVector a
          fromList = foldr (\e (Box es) -> Box (e :> es)) (Box Nil)

We can compare this arbitrary instance with your previous one (which we won't be needing) at GHCi:

    ghci> sample (arbitrary :: Gen (Vec (S (S Z)) Int)) -- must specify length
    (:>) 0 ((:>) 0 Nil)
    (:>) 1 ((:>) 1 Nil)
    (:>) 0 ((:>) (-2) Nil)
    (:>) (-4) ((:>) (-6) Nil)
    (:>) (-1) ((:>) 2 Nil)
    (:>) (-8) ((:>) (-5) Nil)
    (:>) (-11) ((:>) 4 Nil)
    (:>) (-8) ((:>) 2 Nil)
    (:>) (-8) ((:>) (-16) Nil)
    (:>) (-16) ((:>) (-11) Nil)
    (:>) 19 ((:>) (-6) Nil)

    ghci> sample (arbitrary :: Gen (BoxVector Int)) -- all lengths generated
    Box Nil
    Box ((:>) (-2) ((:>) 0 Nil))
    Box ((:>) (-4) Nil)
    Box ((:>) 0 ((:>) (-2) ((:>) (-6) ((:>) (-3) ((:>) (-6) Nil)))))
    Box ((:>) 8 Nil)
    Box ((:>) 6 ((:>) (-6) ((:>) 9 Nil)))
    Box ((:>) 5 ((:>) 4 ((:>) 4 ((:>) (-6) ((:>) (-6) ((:>) (-4) Nil))))))
    Box ((:>) (-4) ((:>) 10 ((:>) (-10) ((:>) 2 ((:>) 6 ((:>) 3 ((:>) 4 ((:>) 1 ((:>) 3 Nil)))))))))
    Box ((:>) 10 ((:>) (-16) ((:>) (-14) ((:>) 15 ((:>) 4 ((:>) (-7) ((:>) (-5) ((:>) 5 ((:>) 6 ((:>) (-1) ((:>) 1 ((:>) (-14) ((:>) (-4) ((:>) 15 Nil))))))))))))))
    Box ((:>) (-2) ((:>) 9 ((:>) 0 ((:>) 7 ((:>) 5 ((:>) 17 Nil))))))
    Box ((:>) (-19) ((:>) (-7) ((:>) (-17) ((:>) (-8) ((:>) (-16) ((:>) 16 ((:>) (-4) ((:>) 16 ((:>) 13 ((:>) (-7) ((:>) (-3) ((:>) 4 ((:>) (-6) ((:>) (-8) ((:>) (-14) Nil)))))))))))))))

Now, we are finally ready to make your test run. Since we want the test to run for all possible lengths, we need to change it to take a BoxVector instead of Vec.

    toList_correct :: Show a => BoxVector a -> Bool
    toList_correct (Box v) = vlength v == length (toList v)

Finally, we will still need to specify what our vectors will contain for the test. For this test, since we don't care about distinguishing elements of the vector from each other, might as well make them vectors of ().

    main :: IO ()
    main = quickCheck (toList_correct :: BoxVector () -> Bool)