如何在Haskell中强制执行数据的运行时条件？

Question

我想定义一个函数f [Int] -> Int,f如果列表的长度是一个完美的正方形,则该函数等于列表中元素的总和,否则是未定义的.在Haskell中这样做的惯用方法是什么？

在命令式语言中,我会添加一行来assert sqrt(len(xs)) is integer为未定义的案例生成异常.在像Haskell这样的强类型函数语言中,您希望在类型系统中构建未定义的条件,但是由于没有"长度完美平方列表"类型,因此无法在此处完成.

我宁愿让程序在未定义的情况下暂停,而不是让函数返回Nothing.

Answer 1

如果你想要正式使用它,那么使用智能构造函数可能是个好机会.

module PSqList
    ( PSqList   -- constructor *not* exported
    , fromList
    )
where

newtype PSqList a = PSqList [a]
    deriving (Functor, Foldable)

fromList :: [a] -> Maybe (PSqList a)
fromList xs
    | isPerfectSquare (length xs) = Just (PSqList xs)
    | otherwise = Nothing

然后,当您使用该PSqList模块时,您可能只构造一个PSqList具有完美方形长度的s.

使用整个模块这样的事情感觉有点奇怪; 也许你想要一个更通用的不变跟踪系统.这是一个依赖类型语言的领域,比如Agda一般,但在Haskell中有一个可爱的中点,显示在功能珍珠Ghosts of Departed Proofs中.

Answer 2

我宁愿让程序在未定义的情况下暂停,而不是让函数返回Nothing.

做到这一点的标准和惯用方法肯定是返回a Maybe Int,而不是做你喜欢做的事情.

如果你问的是如何从纯代码中引发错误,你可以这样做

f ... = error "oops it wasn't a perfect square"

另一种可能性是您的输入[Int]不是正确的类型.也许你想要的是一个保证是两个长度的力量的列表.在这种情况下,您可以创建一个智能构造函数(一个函数,它是生成一个PowerOfTwoList a,并进行验证的唯一方法).你也可以使用某种长度索引向量,其中类型级自然是2的幂(即列表的长度在类型中表示,并且通过构造也是正确的)