Haskell类型的特定数据构造函数

Question

假设我有以下Haskell代码:

data Option
    = Help
    | Opt1 Int Double String
    -- more options would be here in a real case

handleOption :: Option -> IO ()
handleOption option = case option of
    Help -> handleHelp
    Opt1 n f s -> handleOpt1 n f s

handleHelp :: IO ()
handleHelp = print "help"

handleOpt1 :: Int -> Double -> String -> IO ()
handleOpt1 n f s = print (n, f, s)

在上面的代码中,在我可以将数据整齐地捆绑在一起的意义上提前解构对象似乎是浪费.现在我必须单独传递Opt1的每个部分,或者创建一个单独的数据类型来拖运它们.是否有可能在整个传递Opt1到handleOpt1同时不允许一般的Option情况下被传递的,比如做handleOpt1 Help一个编译错误？

示例伪代码如下:

---

data Option
    = Help
    | Opt1 Int Double String

handleOption :: Option -> IO ()
handleOption option = case option of
    Help -> handleHelp
    opt1 @ Opt1{} -> handleOpt1 opt1

handleHelp :: IO ()
handleHelp = print "help"

handleOpt1 :: Option:Opt1 -> IO ()
handleOpt1 (Opt1 n f s) = print (n, f, s)

Answer 1

您可以使用GADT.

{-# LANGUAGE GADTs #-}

data Option a where
    Help :: Option ()
    Opt1 :: Int -> Double -> String -> Option (Int, Double, String)

handleOption :: Option a -> IO ()
handleOption option = case option of
    Help          -> handleHelp
    opt1 @ Opt1{} -> handleOpt1 opt1

handleHelp :: IO ()
handleHelp = print "help"

handleOpt1 :: Option (Int, Double, String) -> IO ()
handleOpt1 (Opt1 n f s) = print (n, f, s)

使用GADT,您可以向编译器提供更多类型信息.对handleOpt1,因为它只接受Option (Int, Double, String),编译器知道Option ()(即Help)将永远不会被传入.

也就是说,使用GADT会使其他一些事情变得更难.例如,自动导出(例如deriving (Eq, Show))通常不适用于它们.您应该仔细考虑在您的情况下使用它们的利弊.