GADT的功能 [英] Functions of GADTs

问题描述

这是多态数据类型的函数

数据类型 Question 使用 Message (问题的文本)和函数( String-> a )将用户的输入映射到问题的结果:

Data type Question models a question/answer with a Message (the text of the question) and a function (String -> a) that maps user's input to the result of the question:

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

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

This CLI program should first gets the name of the Question, find an instance using getQuestion function and then run the Question and print out the result.

{-# 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 ::(可键入a，显示a)=>问题->IO a ，其中没有使用"runQuestion" 引起的(可键入a0)实例.

Type checking fails at here: runQuestion :: (Typeable a, Show a) => Question -> IO a with No instance for (Typeable a0) arising from a use of ‘runQuestion’.

如果我删除了类约束( runQuestion ::问题-> IO a )，那么我会得到由于使用'print .

If I remove the class constraints (runQuestion :: Question -> IO a) then I get No instance for (Show a0) arising from a use of ‘print.

推荐答案

此类型

Question -> IO a

表示接受呼叫者想要的 a 的 Question 并返回 IO a 的函数.".这显然是错误的.有些问题的答案是 Int ，有些问题的答案是 String ，但是没有问题的答案可以是 Int ，字符串，或者我们可能想要的其他任何东西.

means "a function that accepts a Question and returns an IO a for whatever a the caller wants". This is obviously wrong; some questions have an Int answer and some have a String answer, but no question has an answer that can on demand be Int, String, or whatever else we may want.

如果您只需要显示答案就可以显示自己，只需将显示的答案作为 IO String 返回即可.

If all you need from the answer is the ability to show itself, just return a shown answer as an 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中:

Otherwise you can move existentiality to the answer, which you need to encapsulate in a new 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

但这是恕我直言的矫kill过正.

but this is IMHO overkill.

这篇关于GADT的功能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！