How can I correctly create an Arbitrary instance for my Tableaux constructors?

Hello! I’m trying to develop an analyrtic tableaux prover with Haskell and I want to test it with PBT using quickcheck.

I never used quickcheck and I have this data constructors:

data InputMetadata = InputMetadata
    { metadataLine :: Int
    , metadataColumn :: Int
    }
    deriving (Show)

data Operator
    = Not Char
    | And Char
    | Or Char
    | Implies Char
    | Equiv Char
    | Prove Char
    deriving (Show)

data Sign = T | F deriving (Show, Enum)

data TableauxInput
    = TableauxAtom InputMetadata Text
    | TableauxSign InputMetadata Sign
    | TableauxOperator InputMetadata Operator
    | TableauxWff InputMetadata [TableauxInput]
    deriving (Show)

and this is my test file for now:

module Language.Tableaux.ParserSpec where

import Data.Text (singleton)

import Test.Hspec
import Test.Hspec.Parsec
import Test.Hspec.QuickCheck
import Test.QuickCheck
import Test.QuickCheck.Unicode

import Text.Parsec (parse)

import Language.Tableaux.Parser

instance Arbitrary Sign where
    arbitrary = chooseEnum (T, F)

instance Arbitrary Operator where
    arbitrary = intToOp <$> choose (1, 6)

instance Arbitrary TableauxInput where
    arbitrary = intToTableaux <$> choose (1, 4)

main :: Spec
main = undefined

intToOp 1 = Not <$> elements "¬~!"
intToOp 2 = And <$> elements "∧&·"
intToOp 3 = Or <$> elements "∨+∥"
intToOp 4 = Implies <$> elements "⇒→⊃"
intToOp 5 = Equiv <$> elements "⇔≡↔"
intToOp 6 = Prove <$> elements "⊢"

intToTableaux 1 = TableauxAtom <$> inputMetadata <*> letter
intToTableaux 2 = TableauxSign <$> inputMetadata <*> arbitrary
intToTableaux 3 = TableauxOperator <$> inputMetadata <*> arbitrary
intToTableaux 4 = TableauxWff <$> inputMetadata <*> arbitrary

letter = frequency [(26, choose ('a', 'z'))]
inputMetadata = InputMetadata <$> arbitrary <*> arbitrary

however Iḿ having these errors:

/ParserSpec.hs:19:15: error:
    • Couldn't match type ‘Gen Operator’ with ‘Operator’
      Expected type: Gen Operator
        Actual type: Gen (Gen Operator)
    • In the expression: intToOp <$> choose (1, 6)
      In an equation for ‘arbitrary’:
          arbitrary = intToOp <$> choose (1, 6)
      In the instance declaration for ‘Arbitrary Operator’
   |
19 |   arbitrary = intToOp <$> choose (1, 6)
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^

/ParserSpec.hs:22:15: error:
    • Couldn't match type ‘Gen TableauxInput’ with ‘TableauxInput’
      Expected type: Gen TableauxInput
        Actual type: Gen (Gen TableauxInput)
    • In the expression: intToTableaux <$> choose (1, 4)
      In an equation for ‘arbitrary’:
          arbitrary = intToTableaux <$> choose (1, 4)
      In the instance declaration for ‘Arbitrary TableauxInput’
   |
22 |   arbitrary = intToTableaux <$> choose (1, 4)
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Protip: Add type signatures to your top level definitions. It helps in knowing what shape the functions have when trying to figure out what’s going on; AND when asking for help, the reader can more easily figure out what’s going on :+1:


Most of the time when you get a:

Expected type: m a
  Actual type: m (m a)

You’ve fmap-ed (or <$>-ed) where you should have >>=-ed. Here it would type check if written as e.g. choose (1, 6) >>= intToOp


In this case, however, I’d suggest to not make Int -> a functions, but just use oneof and combine it with the possible Gens. For example:

instance Arbitrary Operator where
  arbitrary = oneof
    [ Not <$> elements "¬~!"
    , And <$> elements "∧&·"
    , Or <$> elements "∨+∥"
    , Implies <$> elements "⇒→⊃"
    , Equiv <$> elements "⇔≡↔"
    , pure $ Prove '⊢'
    ]

Also, frequency only does something if the applied list has more than one element. As letter is defined right now, it’s equivalent to choose ('a', 'z'). (Which is what you want, I think)

4 Likes

Thank so much! Yeah, all your comments makes total sense haha

I will take this for my next tries