Haskell：类型签名完全是什么意思？

Question

我有以下代码，概述了布尔和算术表达式的语言：

data Exp a where
 Plus :: Exp Int -> Exp Int -> Exp Int
 Const :: (Show a) => a -> Exp a 
 Not :: Exp Bool -> Exp Bool
 And :: Exp Bool -> Exp Bool -> Exp Bool
 Greater :: Exp Int -> Exp Int -> Exp Bool

以下是仅评估算术表达式的函数的代码：

evalA (Plus a b) = evalA a + evalA b
evalA (Const a) = a 

我试图弄清楚应该给哪种类型的签名以evalA使其完整。但是，我不知道对一个类型签名进行总计意味着什么。任何见解都表示赞赏。

Answer 1

另一个答案说明“合计”是函数的属性，而不是类型签名。然后继续说，如果您希望函数总计，则必须涵盖GADT的其他构造函数。但这还不是全部。

真正的故事是，对于具有高级类型系统（如Haskell）的语言，“总计”是函数和类型签名之间的关系。因此，它确实不是类型签名的属性（说“这种类型签名是总计”是没有道理的）；但是它也不是函数的属性（单独说“这个函数是合计的！” ¹）没有意义。

现在，让我们回到您的问题。你说：

data Exp a where
 Plus :: Exp Int -> Exp Int -> Exp Int
 Const :: (Show a) => a -> Exp a 
 Not :: Exp Bool -> Exp Bool
 And :: Exp Bool -> Exp Bool -> Exp Bool
 Greater :: Exp Int -> Exp Int -> Exp Bool

evalA (Plus a b) = evalA a + evalA b
evalA (Const a) = a 

有了我们最新的理解，我们现在可以提出一个新的更好，更精确的问题，那就是：evalA与该实现配对时，是否存在用于这种配对的类型签名？更好的问题的答案是是，与另一个答案中的说法相反，该说法要求您必须实施更多的案例evalA。特别是如果我们写

evalA :: Exp Int -> Int
evalA (Plus a b) = evalA a + evalA b
evalA (Const a) = a

那么evalA对有限输入的任何类型正确的应用都将在有限时间内产生一个非底答案。（这是功能“合计”的一种明智含义。）

为什么我们可以忽略的Not，And以及Greater案件？为什么呢，因为我们已经要求输入有型Exp Int，任何良好的键入项，其外部构造为Not，And或Greater实际上有型Exp Bool-所以应用程序不会得到很好的类型。因此，这不会因模式匹配错误而导致崩溃，您可能会担心！

¹一种可以说“这种功能，给出的任何类型的签名哪种类型的检查，是总的”。实际上，通常说“此功能是全部功能”作为表示该功能的方便快捷方式。另一个答案显示了无论给定哪种（正确）类型签名，如何使您的函数合计。