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

Question

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

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

但我认为这不是正确的方法。你能不能给我一个想法。

Answer 1

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

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

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

Answer 2

嗯，递归解决方案在 Haskell 中当然是正常的，实际上是一件好事，但是限制元素数量有点棘手。因此，对于该问题的简单解决方案，首先考虑 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 3

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

回想一下，这Maybe a是一种其值的形式为Nothing或Just xfor some 的类型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)