haskell - 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使其完全。但是，我不知道类型签名完全意味着什么。任何见解都值得赞赏。

标签： haskellfunctional-programming

Answer 1

另一个答案解释说“总计”是函数的属性，而不是类型签名；然后继续说，如果你希望你的函数是完整的，你必须覆盖 GADT 的其他构造函数。但这还不是全部。

真实的故事是，对于像 Haskell 这样具有高级类型系统的语言，“total”是函数和类型签名之间的关系。所以它确实不是类型签名的属性（说“这个类型签名是完全的”是没有意义的）；但它也不是函数的属性（孤立地说“这个函数是全部的”！¹是没有意义的）。

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

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情况？为什么，因为我们要求输入具有 type Exp Int，以及任何其外部构造函数为 、 或实际上将具有 type 的类型良好的术语Not——And因此Greater应用Exp Bool程序将不是类型良好的。所以这不会因为不详尽的模式匹配错误而崩溃，因为人们可能会担心！

¹可以说“这个函数，给定任何类型检查的类型签名，是全部的”。事实上，通常说“这个函数是全部的”是一种方便的简写方式。另一个答案显示了无论给出什么（正确的）类型签名，如何使您的函数总计。