问题描述
代数数据类型可以轻松地从集合中选择一项：只需使用适当的和类型即可。
我很好奇如何实现从一组中严格选择 n 项或更少的选项。我可以看到如何使用 Data.Set 实现这一点，但我想知道是否有更健壮的模式或代数结构。
假设一个汉堡可以有 Pickle 中的三种配料 |洋葱 |生菜 | Tomato 等。想要在 UI 中显示所有选项是合理的，所以如果我们使用 Data.Set，我马上注意到 Data.Set.all 丢失了，所以没有简单的方法打印所有可能的值被选中。但是 Data.Set.powerSet 可用，所以我想也许我应该让用户选择基数
使用幂集的元素来表示从基集中进行的选择似乎是个好主意。不过，它看起来不像我能想到的任何 UI。幂集函子是一个 monad，但我不确定这是否相关（请参阅此处关于幂集作为函子的讨论 Sets,Functors and Eq confusion）。
也许以前解决过类似问题的人会对如何最好地完成这项工作提出建议。如果有意义的话，我真的在寻找有关“n 选择 k”类型的概念的见解。
解决方法
这是一个答案。
以下是其余代码所需的一些扩展和导入。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeNats
import Data.Proxy
import Data.Set (Set)
import qualified Data.Set as Set
您可能知道，将单个项目表示为 ADT 的好处：
data Topping = Pickle | Onion | Lettuce | Tomato deriving (Show,Eq,Ord,Enum,Bounded)
是类型的定义使得除了 Topping 的一个选择之外无法表示任何其他内容，前提是我们忽略具有 undefined 值的可能性。使用 Topping 类型，以这种万无一失的方式表示“最多一个 Maybe 选择”同样容易：
type UpToOneTopping = Maybe Topping
我们还可以使用列表表示零个或多个（包括可能的无限个）浇头，可能有重复：
type ManyToppings = [Topping]
然而，很难以同样的方式表示一组没有重复的浇头。我们可以使用 Set Topping 类型，但我们不再依赖类型系统来使具有重复项的集合无法表示。相反，我们依赖于 Set 包中 containers 类型的实现及其提供的受限接口，以保证该集合不包含任何重复项。如果我们深入研究 Set 实现的内容，我们可能会发现内部表示可以允许具有重复的集合，并且我们依赖于 Set 作者编写的代码的正确性以确保不会发生这种情况。
相比之下，上面的 Topping 类型提供了比这更强的保证，使得除了单一类型之外的任何东西都无法通过构造来表示。 （好吧，我想您可以说我们依赖于编译器的正确性，但通常认为这种保证比依赖于 Set 实现的正确性的保证“更强”。）
与 Set 类型类似，可以使用 UpToThree Topping 类型来表示一组零到三个不同的浇头，但保证将由实现和它认可的接口，而不是数据表示本身。也就是说，我们可以这样写：
newtype UpToThree a = UpToThree (Set a)
upToThree :: (Ord a) => [a] -> UpToThree a
upToThree xs | length xs' > 3 = error "no more than three allowed"
| otherwise = UpToThree xs'
where xs' = Set.fromList xs
如果我们只通过这个UpToThree“智能构造函数”创建upToThree值（或者通过程序员纪律或者使用Haskell的包系统来限制导出给数据类型用户的接口），那么我们可以保证任何 UpToThree 值将代表不超过三个不同的 a 值。
在实际的 Haskell 代码中，这可能是最合理的方法。一个限制是它需要为每个最多 k 的数字使用单独的新类型。我们可以使数字成为数据类型中的一个字段：
data UpToK a = UpToK Int (Set a)
upToK :: (Ord a) => Int -> [a] -> UpToK a
upToK k xs | length xs' > k = error "too many"
| otherwise = UpToK k xs'
where xs' = Set.fromList xs
但是这个 UpToK 类型没有它最初出现的时候那么有用。问题在于智能构造函数确保特定的 UpToK 表示多个 a 类型的不同值，该值不超过值中编码的整数字段 k 给出的计数，因此它确保了值中两个字段之间的一致性，但类型系统不会强制执行任何关于 k 的事情，所以如果我们有一个使用原始 UpToThree 需要不超过三个浇头的函数:
data Burger = Burger
placeOnBurger :: UpToThree Topping -> Burger
placeOnBurger u = undefined
我们可以通过使用 UpToThree 的类型签名确保我们收到的浇头不超过三个，前提是 UpToThree 类型的实现是合理的，但是如果我们尝试编写一个 {{1}版本，我们最终不得不检查字段以确保满足我们的先决条件：
UpToK这意味着我们可以直接检查 placeOnBurger' :: UpToK Topping -> Burger
placeOnBurger' (UpToK k _) | k > 3 = error "no one can fit so many toppings!"
placeOnBurger' u = undefined
的长度而根本不需要 Set 类型：
UpToK幸运的是，有一种方法可以使用 placeOnBurger'' :: Set Topping -> Burger
placeOnBurger'' s | length s > 3 = error "too many toppings for a burger"
placeOnBurger'' s = undefined
扩展名，通过非负数索引类型集合。通过其他一些扩展，我们可以这样写：
DataKinds此 newtype UpTo (k :: Nat) a = UpTo (Set a)
upTo :: forall k a. (KnownNat k,Ord a) => [a] -> UpTo k a
upTo xs | length xs' > fromIntegral (natVal (Proxy @k)) = error "too many"
| otherwise = UpTo xs'
where xs' = Set.fromList xs
类型比 UpTo 有用得多。它仍然依赖于受保护的 UpToK 智能构造函数来确保仅生成有效的 upTo 值，但上限现在是类型的一部分，因此我们可以这样写：
UpTo而且我们有一个强大的类型系统保证，这个版本的 placeOnBurger''' :: UpTo 3 Topping -> Burger
placeOnBurger''' s = undefined
只会被一个 placeOnBurger''' 值调用，这意味着一个（较弱的）智能构造函数保证传递的浇头数量将不超过三个。
如果您希望对类型中的最高限制进行更强有力的编码保证，以便由类型系统本身强制执行，就像 UpTo 3 Topping 强制执行零或一最高规则一样，那么这是可能的，但是它很快就会变得笨拙。
一种方法是将 GADT 与由 Maybe Topping 扩展自动提升到类型级别的 Peano natural 结合使用：
DataKinds拥有一个类型级别的函数来将普通类型级别的自然转换为这些 Peano 类型级别的自然也很有帮助：
data Peano = Z | S Peano
然后我们可以轻松地创建一个 GADT，表示一个“不超过 type family P n where
P 0 = Z
P n = S (P (n-1))
”元素的列表：
n需要一点研究才能理解为什么这种表示有效，但是当我们尝试创建类型级别限制为 3、5 和 2 的 3 元素列表时，请观察 GHCi 中会发生什么：
-- a list of no more than `n` elements of type `a`
data LimitedList (n :: Peano) a where
Empty :: LimitedList n a
Cons :: a -> LimitedList n a -> LimitedList (S n) a
infixr 5 `Cons`
deriving instance (Show a) => Show (LimitedList n a)
这个 GADT 的缺点是它允许重复并且不提供唯一的表示，所以如果我们有多个泡菜和洋葱的表示作为不超过 3 的浇头列表：
λ> 1 `Cons` 2 `Cons` 3 `Cons` Empty :: LimitedList (P 3) Int
...works...
λ> 1 `Cons` 2 `Cons` 3 `Cons` Empty :: LimitedList (P 5) Int
...works...
λ> 1 `Cons` 2 `Cons` 3 `Cons` Empty :: LimitedList (P 2) Int
...generates a type error...
但希望它们被统一对待（比较相等，当我们对它们运行 top1 = Pickle `Cons` Onion `Cons` Empty :: LimitedList (P 3) Topping
top2 = Onion `Cons` Pickle `Cons` Empty :: LimitedList (P 3) Topping
top3 = Onion `Cons` Pickle `Cons` Onion `Cons` Empty :: LimitedList (P 3) Topping
时以相同的顺序生成相同的浇头列表，等等），我们最终不得不写更多提供这些（弱）保证的代码。
要回答问题的另一部分，可以编写一个函数来为任何可枚举类型生成特定大小的所有有效 toList，尽管输出将包括这些重复项和替代表示。编写这样的函数需要对 Peano 自然数使用所谓的“单例”表示：
LimitedList这里相当奇怪的 data SPeano n where
SZ :: SPeano Z
SS :: SPeano n -> SPeano (S n)
allLimitedLists :: (Enum a,Bounded a) => SPeano n -> [LimitedList n a]
allLimitedLists SZ = [Empty]
allLimitedLists (SS n) = [x `Cons` xs | x <- [minBound..maxBound],xs <- rest]
++ map levelUp rest
where rest = allLimitedLists n
levelUp :: LimitedList n a -> LimitedList (S n) a
levelUp Empty = Empty
levelUp (x `Cons` xs) = x `Cons` levelUp xs
all3Toppings :: [LimitedList (P 3) Topping]
all3Toppings = allLimitedLists (SS (SS (SS SZ)))
main = print all3Toppings
函数是一个昂贵的恒等函数，至少在术语级别。 （在类型级别，这不是身份，这是重点。）无论如何，这是选择 levelUp 表示的不幸产物。具有讽刺意味的是，它可以安全地替换为 LimitedList。至少，我认为可以。无论如何，它似乎有效。
在我给出最后一种方法之前，这里是到目前为止的所有代码，以防您想使用它：
levelUp = unsafeCoerce最后，可以在类型级别强制实施唯一的、无重复的表示，但它增加了另一层复杂性并使类型变得更加困难使用。这是通过对类型中的最小元素进行编码并使用约束来仅允许附加较小元素来实现的一种方法。我已经使用 {-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeNats
import Data.Proxy
import Data.Set (Set)
import qualified Data.Set as Set
data Topping = Pickle | Onion | Lettuce | Tomato deriving (Show,Bounded)
type UpToOneTopping = Maybe Topping
type ManyToppings = [Topping]
newtype UpToThree a = UpToThree (Set a)
upToThree :: (Ord a) => [a] -> UpToThree a
upToThree xs | length xs' > 3 = error "no more than three allowed"
| otherwise = UpToThree xs'
where xs' = Set.fromList xs
data UpToK a = UpToK Int (Set a)
upToK :: (Ord a) => Int -> [a] -> UpToK a
upToK k xs | length xs' > k = error "too many"
| otherwise = UpToK k xs'
where xs' = Set.fromList xs
data Burger = Burger
placeOnBurger :: UpToThree Topping -> Burger
placeOnBurger u = undefined
placeOnBurger' :: UpToK Topping -> Burger
placeOnBurger' (UpToK k _) | k > 3 = error "no one can fit so many toppings!"
placeOnBurger' u = undefined
placeOnBurger'' :: Set Topping -> Burger
placeOnBurger'' s | length s > 3 = error "too many toppings for a burger"
placeOnBurger'' s = undefined
newtype UpTo (k :: Nat) a = UpTo (Set a)
upTo :: forall k a. (KnownNat k,Ord a) => [a] -> UpTo k a
upTo xs | length xs' > fromIntegral (natVal (Proxy @k)) = error "too many"
| otherwise = UpTo xs'
where xs' = Set.fromList xs
placeOnBurger''' :: UpTo 3 Topping -> Burger
placeOnBurger''' s = undefined
data Peano = Z | S Peano
type family P n where
P 0 = Z
P n = S (P (n-1))
-- a list of no more than `n` elements of type `a`
data LimitedList (n :: Peano) a where
Empty :: LimitedList n a
Cons :: a -> LimitedList n a -> LimitedList (S n) a
infixr 5 `Cons`
deriving instance (Show a) => Show (LimitedList n a)
top1 = Pickle `Cons` Onion `Cons` Empty :: LimitedList (P 3) Topping
top2 = Onion `Cons` Pickle `Cons` Empty :: LimitedList (P 3) Topping
top3 = Onion `Cons` Pickle `Cons` Onion `Cons` Empty :: LimitedList (P 3) Topping
data SPeano n where
SZ :: SPeano Z
SS :: SPeano n -> SPeano (S n)
allLimitedLists :: (Enum a,xs <- rest]
++ map levelUp rest
where rest = allLimitedLists n
levelUp :: LimitedList n a -> LimitedList (S n) a
levelUp Empty = Empty
levelUp (x `Cons` xs) = x `Cons` levelUp xs
all3Toppings :: [LimitedList (P 3) Topping]
all3Toppings = allLimitedLists (SS (SS (SS SZ)))
main = print all3Toppings
包来处理一些样板文件，因此我们需要相当多的扩展和一些导入：
singletons我们的 Peano naturals 和 {-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH
类型都需要单例，如下所示。
Topping这里，我们使用 $(singletons [d|
data Peano = Z | S Peano
data Topping = Pickle | Onion | Lettuce | Tomato deriving (Show,Bounded)
|])
来定义类型函数 promote 和 P。这些可以使用类型系列定义，但推广普通的 Haskell 函数会提供更好的语法。
Before我们的有限集合将由以下 GADT 表示，它表示 $(promote [d|
p 0 = Z
p n = S (p (n-1))
before _ Nothing = True
before x (Just y) = x < y
|])
类型元素的（严格）升序列表，其头部（最小）元素是 a，并且包含不超过h 元素。我们在这里使用 n 类型函数来允许将 Before 值添加到列表中，前提是它严格小于列表的头元素。
x在代码中使用此 data MinLimitedSet (n :: Peano) (h :: Maybe a) where
Empty' :: MinLimitedSet n Nothing
Cons' :: (Before x min ~ True) => Sing x -> MinLimitedSet n min -> MinLimitedSet (S n) (Just x)
infixr 5 `Cons'`
类型需要在类型签名中指定列表的最小元素。这不是很方便，所以我们提供了一个存在类型 MinLimitedSet，它表示一个 LimitedSet 具有未指定的最小元素：
MinLimitedSet有了这些 GADT，我们可以定义一个示例值：
data LimitedSet (n :: Peano) a where
LimitedSet :: MinLimitedSet n (h :: Maybe a) -> LimitedSet n a
请注意，此定义仅因为 top1' :: LimitedSet (P 3) Topping
top1' = LimitedSet $ sing @Pickle `Cons'` sing @Onion `Cons'` Empty'
和 Pickle 严格按升序排列（根据 Onion 的 Ord 实例）并且不超过三个要素相结合。如果您尝试创建一个包含过多浇头的列表，或者一个包含重复项或严格按升序排列的列表，您将收到编译时类型错误。要在程序中使用此类列表，您通常需要将它们转换为普通的术语级列表，这就是 Topping 函数所做的。
toList完整代码：
toList :: forall n a. (SingKind a) => LimitedSet n a -> [Demote a]
toList (LimitedSet asc) = go asc
where go :: forall n lst. MinLimitedSet n lst -> [Demote a]
go (Empty') = []
go (x `Cons'` xs) = fromSing x : go xs
main = print $ toList top1'