重複の可能性:
制限付きの型を作成する方法
Haskellで、文字列であるが10文字以下の「名前」などのタイプを作成することは可能ですか?
そうでない場合、長い名前で Person を作成することを禁止するにはどうすればよいですか ( 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
そのため、以前に名前を 10 文字に制限する必要のないコードを使用していた場合、nameFromString型String -> 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
問題は、をに変換する方法が必要なことStringです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:[]
そして、ここで Text.PrettyPrint を ghci にインポートしていますが、なぜパーサーではないのでしょうか?
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 に答える