Haskell如何知道`xs`是函数定义中的列表？

Posted 2021-04-05

在book.realworldhaskell.org中，条件评估部分下的类型和函数部分给出了以下示例：

 -- file: ch02/myDrop.hs
 myDrop n xs = if n <= 0 || null xs
               then xs
               else myDrop (n - 1) (tail xs)

我确实理解了函数的实现，但我的问题是Haskell如何知道xs是一个列表？

答案

Type inference

你写：

myDrop n xs = if n <= 0 || null xs
              then xs
              else myDrop (n - 1) (tail xs)

因此，Haskell首先假设函数具有类型myDrop :: a -> (b -> c)（它首先不对类型做出任何假设）。所以在内存中我们存储：

myDrop :: a -> b -> c
n :: a
xs :: b

但现在它将开始派生类型。

我们看到例如n <= 0。现在功能(<=)有签名(<=) :: Ord d => d -> d -> Bool。所以这意味着0 :: d，我们现在，对于数字文字，它认为0 :: Num e => e。所以我们可以将Num a添加到类型约束中。

我们也看到null xs，null有签名null :: [f] -> Bool，所以这意味着a ~ [f]（这里~意味着类型相等）。我们还必须检查表达式n <= 0 || null xs导致Bool（因为它是if-then-else的条件。由于(||)具有类型(||) :: Bool -> Bool -> Bool，这意味着n <= 0和null xs应该返回Bools。这有：因为(<=)有输入Ord d -> d -> Bool和null :: [f] -> Bool。所以在第一行的类型推断之后，我们有：

myDrop :: (Num a, Ord a) => a -> [f] -> c
n :: (Num a, Ord a) => a
xs :: [f]

现在我们仍然需要检查第二和第三行。在if-then-else条款中，then表达式和else表达式需要具有相同的类型，因此我们现在认为xs的类型与myDrop (n-1) (tail xs)相同。所以，即使不知道myDrop (n-1) (tail xs)的签名我们已经知道它需要有类型myDrop :: g -> h -> [f]（这里我们目前不知道g和h的类型。

由于我们正在推导出myDrop的类型，我们可以检查到目前为止构造的类型与我们调用的类型，因此我们比较它：

myDrop :: (Num a, Ord a) => a -> [f] -> c  -- currently derived
myDrop ::                   g -> h   -> [f] -- called

所以我们推导出：a ~ g和c ~ h ~ [f]。所以现在我们知道myDrop有类型：

myDrop :: (Num a, Ord a) => a -> [f] -> [f]

我们现在仍然需要对这些论点进行类比检查。例如，我们看到调用中的第一个参数是n - 1，(-)的签名是(-) :: Num i => i -> i -> i，1是一个数字文字，所以1 :: Num j => j，所以我们在这个特定的上下文i ~ j ~ a得到它，因此n - 1 :: a，因此持有函数的派生类型。

我们也知道tail有签名tail :: [k] -> [k]。因为我们用xs :: [f]称它，我们知道f ~ k，因此tail xs :: [f]，这再次成立。我们没有必要进一步派生a或f，所以我们可以将类型设置为：

myDrop n xs :: (Num a, Ord a) => a -> [f] -> [f]

Improving the function

上述功能有效，无论我们提供什么输入，它都能正常工作。但是我认为它有点“不安全”，因为我们使用契约我们称之为契约（tail和null）。例如，如果我们提供一个空列表，tail将会出错。是的，这种情况永远不会发生，因为null会检查这一点。但我们必须自己推理。通常最好只使用总函数：始终返回有效输出的函数。

我们可以在函数的头部执行模式匹配。 Haskell编译器可以推导出我们缺少模式，因此如果我们打开该功能，那么我们可以验证是否涵盖了所有情况。

我们可以把它写成：

myDrop :: (Num a, Ord a) => a -> [f] -> [f]
myDrop _ [] = []
myDrop n xa@(_:xs) | n <= 0 = xa
                   | otherwise = myDrop (n-1) xs

所以这里第一行转换列表为空的情况（无论n是什么，我们返回一个空列表）。如果列表不为空，则它具有模式(_:xs)（我们还保留对xa的引用，整个列表。如果是n <= 0，我们返回xa，否则我们减少n，并在尾部进行递归调用。

另一答案

你在null上打电话给tail和xs。

null :: [a] -> Bool
tail :: [a] -> [a]

两者的参数都是列表，所以Haskell可以推断，如果你调用null xs或tail xs，xs的类型必须是[a]。

另一答案

它没有。在尝试编译调用之前，Haskell不知道xs是一个列表。

当你调用myDrop 3 someList时，Haskell知道null someList可以接受someList，并且可以在tail someList上调用someList并返回一个列表。 Haskell（魔法）类型系统可以推断（在编译时）如何使用它已经知道的编译myDrop n xs。

从理论上讲，如果你为tail和null制作了一些“无名单”的东西，你可以打电话给myDrop 3 notList并得到明智的结果。