在 Maguire 的 Thinking with Types 中，第 29 頁有一個如何使用推廣的資料建構式作為幻象引數的例子。下面是我根據書中的例子撰寫的一個模塊。
{-# LANGUAGE DataKinds #-}
module Main where
import Data.Maybe
import Data.Proxy
--|這個建構式的唯一目的是讓我們訪問它的。
--促進了資料建構式的發展。
data UserType = DummyUser | Admin
-- |給一些用戶一個管理令牌。
data User = User
{ userAdminToken :: Maybe （Proxy 'Admin）。
名稱 :: String, name :: Admin.
}
doSensitiveThings :: Proxy 'Admin -> IO ( )
doSensitiveThings _ = putStrLn "你做了一些敏感的事情"。
trustedUser :: 用戶 用戶trustedUser = User (Just Proxy :: Proxy Admin) "相信我"
main = do
doSensitiveThings (fromJust . userAdminToken $ trustedUser)
我理解這使得沒有管理令牌就無法呼叫doSensitiveThings。但我覺得我錯過了一些重要的東西。
上面的代碼比下面的代碼好在哪里？
module Main where?
import Data.Maybe
data Admin = Admin
data User a = User String
doSensitiveThings :: User Admin -> IO ( )
doSensitiveThings _ = putStrLn "你做了一些敏感的事情"。
trustedUser :: User Admin Admin
trustedUser = User "信任我"
untrustedUser :: User ()
untrustedUser = User "不要相信我"。
main =do
做敏感的事情 信任的用戶
-- doSensitiveThings untrustedUser--不會編譯。
uj5u.com熱心網友回復：
使用原始代碼，你可以寫：
trustedUser = User (Just Proxy) "trusted"/span>
untrustedUser = User Nothing "untrusted"twoUsers :: [User] --或Map Username User或其他。
twoUsers = [trustedUser, untrustedUser]。
你不能用第二個代碼段做一個類似的twoUsers串列，因為你的信任和不信任的用戶有不同的型別。
uj5u.com熱心網友回復：
好吧，現在沒有所謂的 "一個用戶"。一個User Admin和一個User()現在有不同的型別，所以你不能像對待一個串列中的元素一樣對待它們：
users :: [User] -- ill-kinded!
users = [User "untrusted"/span> :: User (), User " trusted" :: User Admin] 。--型別不對！
你也不能再根據一個用戶是否是管理員來進行分支（記住，Haskell 是型別錯誤的！）：
displayActions :: User a -> [String]
displayActions（User name）=
["洗掉我的帳戶（" name "）"] (if isAdmin u then ["洗掉別人的賬戶"] else [])
isAdmin :: User a -> Bool --此函式可以接受User Admin或User ()...
isAdmin = ?? -- ......但它應該如何在此基礎上分支？
所以也許可以試試
data SomeUser = SomeAdmin (User Admin) | SomeNormalUser (User ())
但是現在我們基本上在做你第一個例子中的同樣的事情（其中User Admin成為標記型別，而不是Proxy Admin），只是情況更糟。這里有很多代碼噪音。
name :: SomeUser -> String --不得不在模式匹配/記錄欄位上撰寫自己的訪問函式; ew
name (SomeAdmin (User x) = x
name (SomeNormalUser (User x)) = x --丑陋的模式匹配和相同的代碼兩次; ew
isAdmin :: SomeUser -> Bool[/span
isAdmin (SomeAdmin _) = True
isAdmin _ = False
displayActions :: SomeUser -> [String] --同時擁有SomeUser和User，而不是只有一種型別，并且必須知道在任何特定情況下使用哪一種；ew
displayActions u =
["洗掉我的帳戶（"/span> name u "）"] (if isAdmin u then ["洗掉別人的帳戶"] else [] )
我確實看到原來的內容有問題，我相信這就是讓你困惑的地方。原始代碼中 "唯一 "的 "好東西 "是令牌型別的存在。使用帶有型別引數的Proxy來構造token型別，而不是做
data AdminToken = AdminToken
這（IMO）是毫無意義的，也是令人困惑的（無論是對于理解該技術，還是在結果代碼中）。型別引數與這個想法的好壞無關，保留型別引數而不保留令牌，你將一無所獲。我認為以下內容是對原版的實際改進，同時保留了它的好主意。
data User = { userAdminToken : : Maybe AdminToken; userName :: String }
isAdmin :: User -> Bool
isAdmin = isJust . userAdminToken
displayActions :: User -> [String]
displayActions u
["Delete My Account (" userName u ")"] (if isAdmin u then ["洗掉別人的帳戶"] else [] )
轉載請註明出處，本文鏈接：https://www.uj5u.com/gongcheng/329822.html
標籤：
下一篇：werkzeug.routing.BuildError。無法為端點'post'建立網址。你是否忘記了指定值['post_id']？