使用提升的数据构造函数作为幻像参数

Question

在 Maguire 的《Thinking with Types》中，第 14 页。29，有一个示例，说明如何使用提升的数据构造函数作为幻像参数。这是我根据书中示例编写的一个模块。

{-# LANGUAGE DataKinds #-}
module Main where

import           Data.Maybe
import           Data.Proxy

-- | The only purpose of this constructor is to give us access to its
--   promoted data constructors.
data UserType = DummyUser | Admin

-- | Give some users an administration token.
data User = User
  { userAdminToken :: Maybe (Proxy 'Admin),
    name           :: String
  }

doSensitiveThings :: Proxy 'Admin -> IO ()
doSensitiveThings _ = putStrLn "you did something sensitive"

trustedUser :: User
trustedUser = User (Just (Proxy :: Proxy Admin)) "Trust me"

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 "you did something sensitive"

trustedUser :: User Admin
trustedUser = User "Trust me"

untrustedUser :: User ()
untrustedUser = User "Don't trust me"

main = do
    doSensitiveThings trustedUser
    -- doSensitiveThings untrustedUser -- won't compile

Answer 1

好吧，现在已经没有“a User”这样的东西了。AUser Admin和 aUser ()现在具有不同的类型，因此您不能将它们视为与列表元素相同：

users :: [User] -- ill-kinded!
users = [User "untrusted" :: User (), User "trusted" :: User Admin] -- ill-typed!

您也不能再根据用户是否是管理员进行分支（请记住 Haskell是类型擦除的！）：

displayActions :: User a -> [String]
displayActions (User name) =
    ["Delete My Account (" ++ name ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])
isAdmin :: User a -> Bool -- this function can take either User Admin or User ()...
isAdmin = ??? -- ...but how's it supposed to branch on that?

所以也许可以尝试

data SomeUser = SomeAdmin (User Admin) | SomeNormalUser (User ())

但现在我们基本上在第一个示例中做同样的事情（其中User Admin成为令牌类型而不是Proxy Admin），只是它更糟。只是有很多代码噪音。

name :: SomeUser -> String -- having to write your own accessor functions over pattern matching/record fields; ew
name (SomeAdmin (User x)) = x
name (SomeNormalUser (User x)) = x -- ugly pattern matching and same code twice; ew
isAdmin :: SomeUser -> Bool
isAdmin (SomeAdmin _) = True
isAdmin _ = False

displayActions :: SomeUser -> [String] -- having both SomeUser and User instead of just one type and having to know which one to use in any given situation; ew
displayActions u =
    ["Delete My Account (" ++ name u ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])

我确实发现原版有问题，我相信这就是让你感到困惑的地方。原始代码中“唯一”“好东西”是令牌类型的存在。使用Proxy类型参数来构造令牌类型而不是执行

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 ["Delete Someone Else's Account"] else [])