用于表示具有 0 到 5 个值的列表的类型

Question

我有一个练习，我必须定义一个类型来表示具有 0 到 5 个值的列表。首先，我认为我可以像这样递归地解决这个问题：

data List a = Nil | Content a (List a)

但我认为这不是正确的方法。能不能给我点思路。

Answer 1

嗯，递归解决方案在 Haskell 中当然是正常的，实际上 nice 的东西，但是限制元素的数量有点棘手。因此，对于问题的简单解决方案，首先考虑 bradm 给出的愚蠢但有效的解决方案。

使用递归解决方案，诀窍是在递归中传递一个“计数器”变量，然后在达到允许的最大值时禁用更多元素。这可以通过 GADT 很好地完成：

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeInType, StandaloneDeriving #-}

import Data.Kind
import GHC.TypeLits

infixr 5 :#
data ListMax :: Nat -> Type -> Type where
  Nil :: ListMax n a
  (:#) :: a -> ListMax n a -> ListMax (n+1) a

deriving instance (Show a) => Show (ListMax n a)

然后

*Main> 0:#1:#2:#Nil :: ListMax 5 Int
0 :# (1 :# (2 :# Nil))

*Main> 0:#1:#2:#3:#4:#5:#6:#Nil :: ListMax 5 Int

<interactive>:13:16: error:
    • Couldn't match type ‘1’ with ‘0’
      Expected type: ListMax 0 Int
        Actual type: ListMax (0 + 1) Int
    • In the second argument of ‘(:#)’, namely ‘5 :# 6 :# Nil’
      In the second argument of ‘(:#)’, namely ‘4 :# 5 :# 6 :# Nil’
      In the second argument of ‘(:#)’, namely ‘3 :# 4 :# 5 :# 6 :# Nil’

Answer 2

我不会为你回答你的练习——对于练习，最好自己找出答案——但这里有一个提示可以引导你找到答案：你可以将一个包含 0 到 2 个元素的列表定义为

data List a = None | One a | Two a a

现在，想想如何将其扩展到五个元素。

Answer 3

为了完整起见，让我添加一个“丑陋”的替代方法，但它相当基本。

回想一下，Maybe a 是一种类型，其值的形式为 Nothing 或 Just x，对于某些 x :: a。

因此，通过重新解释上面的值，我们可以将Maybe a 视为“受限列表类型”，其中列表可以有零个或一个元素。

现在，(a, Maybe a) 只是添加了一个元素，因此它是一种“列表类型”，其中列表可以包含一个 ((x1, Nothing)) 或两个 ((x1, Just x2)) 元素。

因此，Maybe (a, Maybe a) 是一种“列表类型”，其中列表可以包含零个 (Nothing)、一个 (Just (x1, Nothing)) 或两个 ((Just (x1, Just x2)) 元素。

您现在应该能够理解如何进行了。让我再次强调一下，这不是一个方便使用的解决方案，但它是（IMO）一个很好的练习来理解它。

---

使用 Haskell 的一些高级特性，我们可以使用类型族来概括上述内容：

type family List (n :: Nat) (a :: Type) :: Type where
    List 0 a = ()
    List n a = Maybe (a, List (n-1) a)