时间戳

首页 > 解决方案 > 如何处理非穷举模式匹配？

haskell - 如何处理非穷举模式匹配？

问题描述

我给我的函数一个列表作为参数，但我知道它可以是空列表或包含一个元素的列表。

当我进行模式匹配时，我会收到有关非详尽模式的警告。我可以忽略它并且代码可以工作，但是有哪些惯用的方法呢？

标签： haskell

解决方案

有几种技术。（下面是一些未经测试的代码。）

限制域

代替

useList :: [a] -> T

我们可以为非空列表使用类型：

useList :: NonEmptyList a -> T

威廉的回答已经解释了这一点。

削弱共域

我们可以改为使用

useList :: [a] -> Maybe T
useList (x:xs) = Just (...) -- as before
useList []     = Nothing

并使模式匹配详尽无遗。然而，这对于必须处理案件的呼叫者来说不太方便Nothing，我们可能知道这永远不会发生。

部分但记录在案的功能

我们可以改为error：

useList :: [a] -> T
useList (x:xs) = (...) -- as before
useList []     = error "useList: empty list"

这也使得模式匹配是详尽的。它以产生我们可以自定义的运行时错误消息为代价来抑制警告。

在某些情况下，没有更实用的替代方案。例如，假设我们正在使用一种算法来解决一项复杂的任务，并且所述算法保持（或至少应该保持）一个不变量，其中列表始终为非空。然后，而不是

useList :: [a] -> Int
useList (x:xs) = (...)
useList []     = -1          -- it never happens, so we can return anything

最好使用

useList :: [a] -> Int
useList (x:xs) = (...)
useList []     = "useList: internal error -- non null list invariant broken!"

后者使得尽早检测错误成为可能。

GADTs 证明

有时我们可以使用 GADT 传递信息，这有助于使模式匹配变得详尽。例如，可以使用标记列表的类型，其中标记表示空虚

data Tag = Empty | NonEmpty

data List (t :: Tag) a where
   Nil  :: List 'Empty a
   Cons :: a -> List t a -> List 'NonEmpty a

然后，

useList :: List 'NonEmpty a -> T
useList (Cons x xs) = ...

是详尽无遗的，即使我们从未处理过Nil此案。

GHC 还允许单独通过“非空证明”：

data IsNonEmpty (t :: Tag) where
   IsNE :: IsNonEmpty 'NonEmpty

useList :: IsNonEmpty t -> List t a -> T
useList IsNE (Cons x xs) = ...

也被认为是详尽无遗的。

推荐阅读