haskell – QuickCheck测试依赖类型

我正在编写依赖类型的Vector和Matrix数据类型.

data Vector n e where
  EmptyVector :: Vector Zero e
  (:>)        :: e -> Vector n e -> Vector (Succ n) e

deriving instance Eq e => Eq (Vector n e)

infixr :>

data Matrix r c e where
  EmptyMatrix :: Matrix Zero c e
  (:/)        :: Vector c e -> Matrix r c e -> Matrix (Succ r) c e

deriving instance Eq e => Eq (Matrix r c e)

infixr :/

它们取决于自然数,也取决于类型.

data Natural where
    Zero :: Natural
    Succ :: Natural -> Natural

我编写了一个函数来计算矩阵中的列数.

columns :: Matrix r c e -> Int
columns m = Fold.foldr (\_ n -> 1 + n) 0 $getRow 0 m

getRow :: Int -> Matrix r c e -> Vector c e
getRow 0 (v :/ _)    = v
getRow i (_ :/ m)    = getRow (i - 1) m
getRow _ EmptyMatrix = error "Cannot getRow from EmptyMatrix."

我现在想使用QuickCheck测试列函数.

为此,我必须将Matrix和Vector声明为QuickCheck提供的Arbitrary类型类的实例.

但是,我不知道如何做到这一点.

>我的数据是否依赖于类型的事实会影响我如何编写这些实例？
>如何生成任意长度的矩阵,确保它们与定义匹配(例如(Succ(Succ r))将有两行)？

解决方法

您可以编写在编译时已知的特定长度的实例：

instance Arbitrary (Vector Zero e) where
    arbitrary = return EmptyVector

instance (Arbitrary e,Arbitrary (Vector n e))
    => Arbitrary (Vector (Succ n) e) where
    arbitrary = do
      e <- arbitrary
      es <- arbitrary
      return (e :> es)

除非你想写,否则上述实例本身并不是很有用
您想要尝试的每个长度的一个表达式(或获取模板 – haskell
生成那些表达式).获取Int以确定类型n的一种方法
应该是隐藏存在主义的n：

data BoxM e where
    BoxM :: Arbitrary (Vector c e) => Matrix r c e -> BoxM e

data Box e where Box :: Arbitrary (Vector c e) => Vector c e -> Box e

addRow :: Gen e -> BoxM e -> Gen (BoxM e)
addRow mkE (BoxM es) = do
    e <- mkE
    return $BoxM (e :/ es)

firstRow :: Arbitrary a => [a] -> BoxM a
firstRow es = case foldr (\e (Box es) -> Box (e :> es)) (Box EmptyVector) es of
    Box v -> BoxM (v :/ EmptyMatrix)

使用addRow和firstRow,编写一个非常简单
mkBoxM :: Int – > Int – > Gen(BoxM Int),然后使用它：

forAll (choose (0,3)) $\n -> forAll (choose (0,3)) $\m -> do
      BoxM matrix <- mkBoxM n m
      return $columns matrix == m -- or whatever actually makes sense

haskell – QuickCheck测试依赖类型

解决方法

猜你在找的设计模式相关文章