我怎样才能“说服”GHC 我已经排除了某个案例？

Question

我有以下非空列表 (NEList) 数据类型的玩具实现：

-- A type to describe whether or not a list is empty.
data Emptiness :: Type where
  Empty    :: Emptiness
  NotEmpty :: Emptiness

-- The list itself. Note the existential type in `Cons'.
data List :: Emptiness -> Type -> Type where
  Nil :: List 'Empty a
  Cons :: a -> List e a -> List 'NotEmpty a

type EList a = List 'Empty a
type NEList a = List 'NotEmpty a

例如，很容易定义一个只在非空列表上运行的 'safe head' 函数：

eHead :: NEList a -> a
eHead (Cons a _) = a

最后一个同样简单，但有点复杂：

eLast :: NEList a -> a
eLast (Cons a Nil) = a
eLast (Cons _ <b>b@(Cons _ _)</b>) = eLast b

模式需要这样的原因是为了让 GHC 相信 b 的类型确实是 List 'NotEmpty，而不是未知的存在类型。由于这个原因，以下代码失败：(Couldn't match type ‘e’ with ‘'NotEmpty’ ...)

eLast :: NEList a -> a
eLast (Cons a Nil) = a
eLast (Cons _ <b>b</b>) = eLast b

我很清楚为什么会发生这种情况。我想知道的是，我可以避免每次都写 b@(Cons _ _) 吗？是否有一些 other 方法可以限制类型，以便 GHC 知道 b 严格引用类型 List 'NotEmpty?

一个明显的方法是使用 unsafeCoerce 但这违背了练习的重点。

为了可重复性，这是我的序言：

{-# OPTIONS_GHC -Wall -Werror #-} -- To prevent missed cases. {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} import Data.Kind

Answer 1

您可以做的一件事是为空列表传递替代方案：

lastDef :: a -> List e a -> a
lastDef a Nil = a
lastDef _ (Cons a b) = lastDef a b

然后在顶层把它包起来。

last :: NEList a -> a
last (Cons a b) = lastDef a b

将此模式扩展到 foldr 和 foldr1 留作 reader 的练习。

Answer 2

你 "defined" NEList（我说的比较笼统）和 base 定义 NonEmpty 的方式一样：作为一个固定在头上的元素一个可能为空的列表。

data NonEmpty a = a :| [a]

NonEmpty 的另一个演示文稿将单个元素放在末尾。

data NonEmpty a = Single a | Multiple a (NonEmpty a)

毫不奇怪，此演示文稿使 eLast 变得简单：

eLast (Single x) = x
eLast (Multiple _ xs) = eLast xs

每当您需要同一类型的多组构造函数时，请查看模式同义词。除了基础 NonEmpty，我们还可以翻译成您的 List.

pattern Single :: forall e a. () => e ~ 'NotEmpty => a -> List e a
pattern Single x = Cons x Nil
pattern Multiple :: forall e a. () => e ~ 'NotEmpty => a -> List 'NotEmpty a -> List e a
pattern Multiple x xs <- Cons x xs@(Cons _ _)
  where Multiple x xs = Cons x xs
-- my dormant bidirectional pattern synonyms GHC proposal would allow just
-- pattern Multiple x (Cons y xs) = Cons x (Cons y xs)
-- but current pattern synonyms are a little stupid, so Multiple is ugly
{-# COMPLETE Nil, Single, Multiple :: List #-}
-- Single and Multiple are actually patterns on List e a, not List NotEmpty a
-- Therefore the COMPLETE must include Nil, or else we'd show that all
-- Lists are nonempty (\case { Single _ -> Refl; Multiple _ _ -> Refl })
-- They are, however, still complete on List NotEmpty a
-- GHC will "infer" this by "trying" the Nil constructor and deeming it impossible

给予

eLast :: NEList a -> a
eLast (Single x) = x
eLast (Multiple _ xs) = eLast xs

我怎样才能“说服”GHC 我已经排除了某个案例？

How can I ‘convince’ GHC that I've excluded a certain case?

haskell

type-inference

gadt

existential-type