haskell 类型、新类型或仅包含大写字符的数据

Question

如果我想创建一个字符串但只包含一个大写字符。我知道 String 是一个 [Char]。我尝试过类似 type a = ['A'..'Z'] 但没有任何帮助？

Answer 1

你想要的是依赖类型，Haskell 没有。依赖类型是那些依赖值的类型，因此使用依赖类型，您可以在类型级别将长度为 5 的向量编码为

only5 :: Vector 5 a -> Vector 10 a
only5 vec = concatenate vec vec

同样，Haskell 没有依赖类型，但像 Agda、Coq 和 Idris 这样的语言确实支持它们。相反，您可以只使用“智能构造函数”

module MyModule
    ( Upper      -- export type only, not constructor
    , mkUpper    -- export the smart constructor
    ) where

import Data.Char (isUpper)

newtype Upper = Upper String deriving (Eq, Show, Read, Ord)

mkUpper :: String -> Maybe Upper
mkUpper s = if all isUpper s then Just (Upper s) else Nothing

此处构造函数 Upper 未导出，仅导出类型，然后该模块的用户必须使用安全拒绝非大写字符串的 mkUpper 函数。

<小时/>

为了澄清并展示依赖类型有多么出色，请考虑上面神秘的 concatenate 函数。如果我用依赖类型来定义它，它实际上看起来像

concatenate :: Vector n a -> Vector m a -> Vector (n + m) a
concatenate v1 v2 = undefined

等等，算术在类型签名中做什么？它实际上是对该类型所依赖的值执行类型系统级别的计算。这消除了 Haskell 中的许多潜在样板，并且在编译时保证了数组的长度不能为负。