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

Question

根据"Haskell的好消息",Bool的类型声明是

data Bool = True | False

并且Int的类型声明可以被认为是类似的

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

对于一些抽象代数应用程序,我想创建一个具有有限多个指定值的类似类型,例如,值可以是$ 0 $和$ n $之间的整数,对于某些$ n $.尽管声称Int的定义,以下不起作用:

data F3 = 0 | 1 | 2

错误"类型中的非法文字".如何创建一个这些是唯一居民的类型？类似于:

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虽然.