GADTs的功能

Question

这是

的后续问题

数据类型 Question 使用 Message（问题的文本）和将用户输入映射到结果的函数 (String -> a) 对 question/answer 进行建模问题：

data Question where
  Simple :: (Typeable a, Show a) => Message -> (String -> a) -> Question

此 CLI 程序应首先获取 Question 的名称，使用 getQuestion 函数查找实例，然后运行 Question 并打印出结果。

{-# LANGUAGE GADTs #-}

import Data.Typeable

type Message = String

data Question where
  Simple :: (Typeable a, Show a) => Message -> (String -> a) -> Question
  -- more constructors

yourName :: Question
yourName = Simple "Your name?" id

yourWeight :: Question
yourWeight = Simple "What is your weight?" (read :: String -> Int)

getQuestion :: String -> Question
getQuestion "name" =  yourName
getQuestion "weight" =  yourWeight    

runQuestion :: (Typeable a, Show a) => Question -> IO a
runQuestion (Simple message parser) = do
  putStrLn message
  ans <- getLine
  return $ parser ans

main = getLine >>= (runQuestion . getQuestion) >>= print

此处的类型检查失败：runQuestion :: (Typeable a, Show a) => Question -> IO a 和 No instance for (Typeable a0) arising from a use of ‘runQuestion’。

如果我删除 class 约束 (runQuestion :: Question -> IO a)，那么我会得到 No instance for (Show a0) arising from a use of ‘print.

Answer 1

这种类型

Question -> IO a

表示"a function that accepts a Question and returns an IO a for whatever a the caller wants"。这显然是错误的；有些问题有 Int 答案，有些问题有 String 答案，但没有问题的答案可以按需为 Int、String 或我们可能想要的任何其他答案.

如果您只需要答案能够自我展示，只需 return 显示的答案作为 IO String。

type Message = String

data Question = Simple Message (String -> String)
  -- more constructors

yourName :: Question
yourName = Simple "Your name?" show

yourWeight :: Question
yourWeight = Simple "What is your weight?" (show . (read :: String -> Int))

getQuestion :: String -> Question
getQuestion "name" =  yourName
getQuestion "weight" =  yourWeight

runQuestion :: Question -> IO String
runQuestion (Simple message parser) = do
  putStrLn message
  ans <- getLine
  return $ parser ans

main = getLine >>= (runQuestion . getQuestion) >>= putStrLn

否则你可以将存在性移动到答案中，你需要将其封装在一个新的 GADT 中：

type Message = String

data Question where
  Simple :: Message -> (String -> Answer) → Question
  -- more constructors

data Answer where
  Easy ::  (Typeable a, Show a) => a -> Answer

instance Show Answer where
  show (Easy a) = show a

yourName :: Question
yourName = Simple "Your name?" Easy

yourWeight :: Question
yourWeight = Simple "What is your weight?" (Easy . (read :: String -> Int))

getQuestion :: String -> Question
getQuestion "name" =  yourName
getQuestion "weight" =  yourWeight

runQuestion :: Question -> IO Answer
runQuestion (Simple message parser) = do
  putStrLn message
  ans <- getLine
  return $ parser ans

main = getLine >>= (runQuestion . getQuestion) >>= print

但恕我直言，这是矫枉过正。

Answer 2

您报告的错误不是唯一的错误。

让我们戴上特殊的眼镜，可以看到通常被 "type inference" 隐藏的东西。

首先是数据构造函数：

Simple :: forall a. (Typeable a, Show a) =>
          Message -> (String -> a) -> Question

实际上，Question 类型的值看起来像

Simple {a}{typeableDict4a}{showDict4a} message parser

我在大括号中写下了看不见的东西。构造函数打包了一个类型和两个类型类字典，它们为 Typeable 和 Show.

的成员提供了实现

现在让我们进入主程序。我重命名了类型变量以说明问题。

runQuestion :: forall b. (Typeable b, Show b) => Question -> IO b

要返回的类型由 runQuestion 的调用者选择，与类型 Question 的参数中包含的任何类型分开。现在让我们填写程序本身不可见的组件。

runQuestion {b}{typeableDict4b}{showDict4b}
  (Simple {a}{typeableDict4a}{showDict4a} message parser) = do
                        -- so parser :: String -> a
      putStrLn message  -- ok, as message :: String
      ans <- getLine    -- ensures ans :: String
  return $ parser ans   -- has type IO a, not IO b

parser 计算 a 类型的值打包在 Question 中，它与直接传递给 [=21] 的类型 b 完全不同=].该程序不进行类型检查，因为两种类型之间存在冲突，程序的调用者可以将其设置为不同的类型。

同时，让我们看看print

print :: forall c. Show c => c -> IO ()

写的时候

main = getLine >>= (runQuestion . getQuestion) >>= print

你得到

main = getLine >>=
  (runQuestion {b}{typeableDict4b}{showDict4b} . getQuestion) >>=
  print {b}{showDict4b}

并且由于runQuestion {b}的return类型是IO b，所以print的c类型必须与runQuestion 的 b 类型，但除此之外，还有 nothing 可以确定 b 是哪种类型，或者为什么它是一个实例Typeable 或 Show。使用类型注释，需要 Typeable 首先出现（在 runQuestion 调用中）；没有，在 print 中需要 Show 会引起投诉。

真正的问题是，不知何故，您似乎希望 runQuestion 以隐藏在问题中的任何类型提供一个东西，就好像您可以以某种方式编写一个（依赖类型的）程序，如

typeFrom :: Question -> *
typeFrom (Simple {a}{typeableDict4a}{showDict4a} message parser) = a

runQuestion :: (q :: Question) -> IO (typeFrom q)

这是一件非常明智的事情，但它不是 Haskell：无法命名 "the type packed up inside that argument"。涉及该类型的所有内容都必须存在于案例分析或公开它的模式匹配的范围内。您试图在该范围之外执行 print 是不允许的。

GADTs的功能

Functions of GADTs

haskell

gadt