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

Question

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

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

我也理解函数的实现,但我的问题是,如何哈斯克尔知道xs是一个列表？

Answer 1

类型推断

你写:

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导致a 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]

改善功能

上述功能有效,无论我们提供什么输入,它都能正常工作.但是我认为它有点"不安全",因为我们使用契约来处理函数(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,并在尾部进行递归调用.

Answer 2

您呼叫null和tail上xs.

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

两者的参数都是列表,因此Haskell可以推断出,如果您正在调用null xs或者必须是tail xs类型.xs[a]