创建具有有限多个居民的 Haskell 类型

Question

根据“Haskell for a great good”，Bool 的类型声明是

data Bool = True | False

并且 Int 的类型声明可能被视为类似

data Int = -2147483648 | -2147483647 | ... | -1 | 0 | 1 | 2 | ... | 2147483647

对于一些抽象代数应用程序，我想创建一个具有有限多个指定值的类似类型，例如对于某些 $n$，这些值可能是 $0$ 和 $n$ 之间的整数。尽管声明了 Int 的定义，但以下内容不起作用：

data F3 = 0 | 1 | 2

出现错误“Illegal literal in type”。如何创建一个只有这些居民的类型？类似：

data F a = (Int a) => [0..a]

会非常棒。

另外，我可以创建一个函数来枚举一个类型的所有有效值，或者返回一个值列表吗？

Answer 1

您可以使用空构造函数（如True、False、Nothing、() 等）

data F3 = Zero | One | Two
    deriving (Bounded, Enum, Show)

要枚举所有有效值，我们只需派生 Enum 和 Bounded 并让 GHC 为我们完成所有工作。

enum :: (Bounded a, Enum a) => [a]
enum = [minBound .. maxBound]

λ. enum :: [F3]
[Zero,One,Two]

如果你想像实际的Int 一样使用这些，你可以使用fromEnum :: Enum a => a -> Int，它相当于

fromEnum Zero = 0
fromEnum One  = 1
fromEnum Two  = 2

Answer 2

你不能在这样的新类型中使用整数字面量。它们已经被占用，所以它不是有效的语法。

cdk 的回答给出了一个更实际的场景，但我想我会举一个例子来说明如何在 Haskell 中实现你的上一个例子。

如果我们打开一些更有趣的扩展，我们可以说服 GHC 制作一个具有给定有限数量值的类型。但是，我可能不建议在实际代码中实际这样做，因为 GHC 目前对这种依赖类型的编程没有最好的支持。此外，不幸的是，这些值没有好听的名字。据我所知，没有办法给它们起像1, 2, 3... 这样的好名字（编辑：实际上，我们可以对此稍作改进，参见第二个代码块）。

可能是这样的：

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators #-}

module Fin (Fin (..))
  where

import GHC.TypeLits -- We get Nat from here as well as the type-level `<=` and `+`.

-- This is a type parameterized by another type. The type that parameterizes (`Nat`)
-- behaves like natural numbers at a type level. The `Nat -> *` is the "kind" of the type
-- `Fin`. A kind is like a type for types. To put it another way, a kind is to a type what
-- a type is to a value. In this case, the type `Nat` has kind `Nat`.
data Fin :: Nat -> * where
  FZero :: Fin upperBound
  FSucc :: (1 <= upperBound) => Fin upperBound -> Fin (upperBound + 1)

-- This is ok, because we are using the "fourth" value in a type with five values.
fifthValue :: Fin 5
fifthValue = FSucc (FSucc (FSucc FZero))

-- This doesn't compile, because it tries to make something of type
-- `Fin 2` using a "3rd value".
--    thirdValue :: Fin 2
--    thirdValue = FSucc (FSucc FZero)
--
-- The only inhabitants of `FiniteList 2` are `FZero` and `FSucc FZero`

请注意，要实际获取 Eq 和 Ord 之类的实例，您可能需要做更多棘手的事情（我什至不完全确定它是否可能。它可能需要新的类型级自然数定理证明他们正在使用 GHC 7.10）。

我可能应该指出的另一件事是Nat 中的类型被命名为1, 2, ...。这没关系，因为没有其他任何东西在类型级别（仅在值级别）使用这些名称。

编辑：

如果我们打开更多的扩展，我们可以获得一个版本，您可以（几乎）直接指定值的名称：

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, PolyKinds, TypeFamilies, UndecidableInstances #-}
import Data.Type.Equality
import GHC.TypeLits

type family (||) (a :: Bool) (b :: Bool) :: Bool where
  True  || x  = True
  False || x  = x

type family Elem (a :: k) (xs :: [k]) :: Bool where
  Elem x (y ': ys) = (x == y) || Elem x ys
  Elem x '[]       = False


data NamedFin :: [k] -> * where
  Val :: ((a `Elem` as) ~ True) => Proxy a -> NamedFin as

-- Countdown n makes a type level list of Nats.
-- So, for example, Countdown 3 is a shorthand for '[3, 2, 1]
type family Countdown (a :: Nat) :: [Nat] where
  Countdown 0 = '[]
  Countdown n = (n - 1) ': Countdown (n - 1)

data Proxy a = Proxy deriving Show

type Example = NamedFin (Countdown 5) -- This is the same as NamedFin '[5, 4, 3, 2, 1]

-- This compiles...
example :: Example
example = Val (Proxy :: Proxy 4)

-- ...but this doesn't
--     example2 :: Example
--     example2 = Val (Proxy :: Proxy 10)

虽然为 Eq 和 Ord 创建实例仍然存在问题。