可能重复：
如何制作有限制的类型
是否可以在 Haskell 中创建一个类型，例如“名称”，它是一个字符串但不包含超过 10 个字母？
如果不是，我怎么能禁止创建一个长名称的人（其中 Person 的定义是这样的：）data Person = Person Name。
也许它根本不重要，也许这种问题应该在 Haskell 中以不同的方式解决？
问问题
2689 次
3 回答
13
不要从定义类型的模块中导出构造函数，而是导出“智能构造函数”：
module Name (Name(), -- exports the type Name, but not the data constructor Name
nameFromString,
stringFromName)
where
data Name = Name String
-- this is the only way to create a Name
nameFromString :: String -> Maybe Name
nameFromString s | 10 < length s = Nothing
| otherwise = Just (Name s)
-- this is the only way to access the contents of a Name
stringFromName :: Name -> String
stringFromName (Name s) = s
因此，您担心，如果您以前的代码不需要名称限制为十个字符，那么您不能直接插入，nameFromString因为它有 typeString -> Maybe Name而不是String -> Name.
首先，如果你真的想抛出异常，你可以定义
import Data.Maybe (fromMaybe)
nameFromString' :: String -> Name
nameFromString' = fromMaybe (error "attempted to construct an invalid Name") . nameFromString
并改用它。
其次，抛出异常有时是错误的做法。考虑
askUserForName :: IO Name
askUserForName
= do putStr "What's your name? (10 chars max) "
s <- getLine
case nameFromString s of
Just n -> return n
Nothing -> askUserForName
重写它以使用异常会导致更复杂的代码。
于 2012-05-05T00:03:27.347 回答
9
dave4420 有你应该做什么的答案。也就是说，只导出智能构造函数。在依赖类型语言中，您可以将数据类型限制为某些形式。但是，Haskell 不是依赖类型的。
等等，不，那不是真的。Haskell 是“世界上最流行的依赖类型语言”。你只需要伪造依赖类型。停止。如果您是 1. 仍在学习基本的 Haskell 2. 并非完全疯狂，请不要再阅读。
可以在类型系统中对“不超过 10 个字符”的约束进行编码。像这样的类型
data Name where
Name :: LessThan10 len => DList Char len -> Name
但我正在超越自己
首先，你需要大量的扩展（我假设 GHC 7.4，早期版本仍然可以做到，但更痛苦）
{-# LANGUAGE TypeFamilies,
DataKinds,
GADTs,
FlexibleInstances,
FlexibleContexts,
ConstraintKinds-}
import Prelude hiding (succ)
现在我们为类型级别的自然构建一些机器......使用新的 DataKinds 扩展
data Nat = Z | S Nat
type N1 = S Z --makes writing numbers easier
type N2 = S N1
--etc
type N10 = S N9
现在我们需要数字的数据表示和生成它们的方法
data Natural n where
Zero :: Natural Z
Succ :: Natural a -> Natural (S a)
class Reify a where
reify :: a
instance Reify (Natural Z) where
reify = Zero
instance Reify (Natural n) => Reify (Natural (S n)) where
reify = Succ (reify)
好的，现在我们可以对数字小于 10 的想法进行编码，并编写一个帮助程序来测试它是否可以启动
type family LTE (a :: Nat) (b :: Nat) :: Bool
type instance LTE Z b = True
type instance LTE (S a) Z = False
type instance LTE (S a) (S b) = LTE a b
--YAY constraint kinds!
type LessThan10 a = True ~ (LTE a N10)
data HBool b where
HTrue :: HBool True
HFalse :: HBool False
isLTE :: Natural a -> Natural b -> HBool (LTE a b)
isLTE Zero _ = HTrue
isLTE (Succ _) Zero = HFalse
isLTE (Succ a) (Succ b) = isLTE a b
有了所有这些，我们可以定义长度编码的字符串
data DList a len where
Nil :: DList a Z
Cons :: a -> DList a len -> DList a (S len)
toList :: DList a len -> [a]
toList Nil = []
toList (Cons x xs) = x:toList xs
data Name where
Name :: LessThan10 len => DList Char len -> Name
甚至取回字符串，并Show为Name
nameToString :: Name -> String
nameToString (Name l) = toList l
instance Show Name where
show n = "Name: " ++ nameToString n
问题是我们需要一种将 aString变成 a 的方法Name。那更难。
首先，让我们弄清楚一个字符串有多长
data AnyNat where
AnyNat :: Natural n -> AnyNat
zero = AnyNat Zero
succ (AnyNat n) = AnyNat (Succ n)
lengthNat :: [a] -> AnyNat
lengthNat [] = zero
lengthNat (_:xs) = succ (lengthNat xs)
现在将列表转换为依赖列表是一件简单的事情
fromListLen :: Natural len -> [a] -> Maybe (DList a len)
fromListLen Zero [] = Just Nil
fromListLen Zero (x:xs) = Nothing
fromListLen (Succ a) [] = Nothing
fromListLen (Succ a) (x:xs) = do rs <- fromListLen a xs
return (Cons x rs)
仍然不是免费的，但我们正在到达那里
data MaybeName b where
JustName :: LessThan10 len => DList Char len -> MaybeName True
NothingName :: MaybeName False
maybeName :: MaybeName b -> Maybe Name
maybeName (JustName l) = Just $ Name l
maybeName (NothingName) = Nothing
stringToName' :: Natural len -> String -> MaybeName (LTE len N10)
stringToName' len str = let t = isLTE len (reify :: Natural N10)
in case t of
HFalse -> NothingName
HTrue -> case fromListLen len str of
Just x -> JustName x
--Nothing -> logic error
最后一点只是让 GHC 相信我们并没有试图让编译器绞尽脑汁unsafePerformIO $ produce evilLaugh
stringToNameLen :: Natural len -> String -> Maybe Name
stringToNameLen len str = maybeName $ stringToName' len str
stringToNameAny :: AnyNat -> String -> Maybe Name
stringToNameAny (AnyNat len) str = stringToNameLen len str
stringToName :: String -> Maybe Name
stringToName str = stringToNameAny (lengthNat str) str
哇，我写了长堆栈溢出帖子，但这很重要
我们测试它
*Main> stringToName "Bob"
Just Name: Bob
*Main> stringToName "0123456789"
Just Name: 0123456789
*Main> stringToName "01234567890"
Nothing
所以它起作用了，类型系统现在可以强制你的名字不超过 10 个字符的不变量。不过说真的，这很可能不值得你付出努力。
于 2012-05-05T06:19:55.130 回答
5
你很好地描述了这个类型。当然，你很快就会后悔...
data Name = N1 Char
| N2 Char Char
| N3 Char Char Char
| N4 Char Char Char Char
| N5 Char Char Char Char Char
| N6 Char Char Char Char Char Char
| N7 Char Char Char Char Char Char Char
| N8 Char Char Char Char Char Char Char Char
| N9 Char Char Char Char Char Char Char Char Char
| N10 Char Char Char Char Char Char Char Char Char Char
deriving (Show, Eq,Ord)
prettyName :: Name -> String
prettyName (N1 a) = a:[]
prettyName (N2 a b) = a:b:[]
prettyName (N3 a b c) = a:b:c:[]
prettyName (N4 a b c d) = a:b:c:d:[]
prettyName (N5 a b c d e) = a:b:c:d:e:[]
prettyName (N6 a b c d e f) = a:b:c:d:e:f:[]
prettyName (N7 a b c d e f g) = a:b:c:d:e:f:g:[]
prettyName (N8 a b c d e f g h) = a:b:c:d:e:f:g:h:[]
prettyName (N9 a b c d e f g h i) = a:b:c:d:e:f:g:h:i:[]
prettyName (N10 a b c d e f g h i j) = a:b:c:d:e:f:g:h:i:j:[]
当我们在 ghci 中导入 Text.PrettyPrint 时，为什么不用解析器呢？
import Text.ParserCombinators.Parsec
import Control.Applicative ((<*))
-- still lame
pN :: Parser Name
pN = do letters <- many1 alphaNum <* space
case letters of
a:[] -> return $ N1 a
a:b:[] -> return $ N2 a b
a:b:c:[] -> return $ N3 a b c
a:b:c:d:[] -> return $ N4 a b c d
a:b:c:d:e:[] -> return $ N5 a b c d e
a:b:c:d:e:f:[] -> return $ N6 a b c d e f
a:b:c:d:e:f:g:[] -> return $ N7 a b c d e f g
a:b:c:d:e:f:g:h:[] -> return $ N8 a b c d e f g h
a:b:c:d:e:f:g:h:i:[] -> return $ N9 a b c d e f g h i
a:b:c:d:e:f:g:h:i:j:[] -> return $ N10 a b c d e f g h i j
_ -> unexpected "excess of letters"
-- *Main> parseTest pN "Louise "
-- N6 'L' 'o' 'u' 'i' 's' 'e'
-- *Main> parseTest pN "Louisiana "
-- N9 'L' 'o' 'u' 'i' 's' 'i' 'a' 'n' 'a'
-- *Main> parseTest (fmap prettyName pN) "Louisiana "
-- "Louisiana"
-- *Main> parseTest pN "Mississippi "
-- parse error at (line 1, column 13):
-- unexpected excess of letters
...也许这不是一个好主意...
于 2012-05-05T02:36:23.903 回答