haskell - 我怎样才能 ‘convince’ 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

例如，很容易定义一个只在非空列表上操作的“安全头”函数:

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

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

eLast :: NEList a -> a
eLast (Cons a Nil) = a
eLast (Cons _ b@(Cons _ _)) = 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) = eLast b

我完全知道为什么会这样。我想知道的是，我可以避免写 b@(Cons _ _)吗？每次？有没有其他方法可以限制类型，以便 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留给读者作为练习。