GHC编译器不抱怨错误的代码路径

Question

我正在接近Haskell,将运行时错误转换为编译时错误.我希望编译器能够确定以下代码中的所有代码路径都没有错误.如果authorizeUser返回UnauthorizedCommand则调用(command $ authorizeUser cmd userId)将在运行时失败.

data Command = UnauthorizedCommand | Command {command :: String, userId :: String}

authorizedUsers = ["1", "2", "3"]

authorizeUser :: String -> String -> Command
authorizeUser cmd userId = if (userId `elem` authorizedUsers) then Command {command=cmd, userId=userId} else UnauthorizedCommand

main :: IO ()
main = do
  cmd <- getLine
  userId <- getLine
  case (command $ authorizeUser cmd userId) of
    "ls" -> putStrLn "works"
    _ -> putStrLn "not authorized"

是否有编译器开关来启用此类检查？

Answer 1

此示例中的主要问题是在具有多个构造函数的数据类型中使用记录语法最终会得到部分记录选择器函数.因此,除非所有构造函数具有相同的记录字段,否则不建议混合记录和多个构造函数.

最简单的解决方案是不在此处使用记录语法并定义您自己的command访问器,使得Maybe返回类型使错误案例显式:

data Command = UnauthorizedCommand | Command String String

command :: Command -> Maybe String
command UnauthorizedCommand = Nothing
command (Command cmd _)     = Just cmd

在编译期间检查此更复杂的方法是使用GADT对类型中的权限级别进行编码.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

data Permission
  = Authorized | Unauthorized

data Command p where
  UnauthorizedCommand :: Command Unauthorized
  Command :: {command :: String, userId :: String} -> Command Authorized

现在,command选择器的类型是Command Authorized -> String如此,如果您尝试使用未经授权的命令,则会出现编译时错误.