Haskell 中的多态性

问题描述

我是 Haskell 的新手,从第一原则开始阅读 Haskell。

顺便说一句,这个问题与本书无关,我以以下问题为例

在第 10 章,第 10.5 节,问题 5,第 f 部分

问题:

以下是与您已经完成的非常相似的简单折叠 看到了,但每个都有至少一个错误。请修复它们并测试 你的 REPL

f) foldr const 'a' [1..5]

并给出以下错误 没有从文字“1”中产生的 (Num Char) 实例

enter image description here

简单的意思就是这里不能用1作为Char

但我在本章中读到折叠就像文本重写器,用函数替换 cons(:) 并用累加器替换空列表 所以结果是(我已经缩短了列表)

foldr const 'a' [1..2] 
to 
(1 `const` (2 `const` 'a')) 

并且它的工作没有编译器错误

那么可能出什么问题了? 为什么第一个不工作,它的重写工作?

但我看到重写的形式 const 有两种形式

Int -> Int -> Int 
and 
Int -> Char -> Int

也许这是它的 bcs 所以我像这样修复 const 的类型

cont :: Int -> Int -> Int
cont = const

现在当我说使用它

(1 `cont` (2 `cont` 'a'))

Couldn't match expected type `Int' with actual type `Char'

好像我们在使用多态函数时 Haskell 固定了它的类型,我们不能以其他形式使用它

也许应该是列表折叠描述应该是这样的

folds like Text Rewriter,用函数替换 cons(:),修复函数类型,用累加器替换空列表

分享您的想法。

不仅 Haskell,其他类型语言也有相同的行为?

也许我完全错了?

解决方法

在表达式中

(1 `const` (2 `const` 'a')) 
   ---A---    ---B---

我们两次使用多态函数const。每次使用都会导致多态函数类型被实例化为进行所有类型检查所需的任何类型。

const 的一般类型是:

const :: a -> b -> a

让我们假设数字文字的类型为 Int 以保持解释简单。 当我们写2 `const` 'a'(上面的--B--点)时,Haskell明白上面的类型变量a必须是Int,而b必须是Char ,所以我们在这里使用

const :: Int -> Char -> Int

因此,2 `const` 'a' 的结果属于 Int 类型。

知道了这一点,我们现在可以意识到上面const点使用的--A--只能在我们选择类型变量ab作为{{ 1}}。所以,我们使用

Int

这是可能的,因为类型系统允许在使用函数的每个点都有不同的多态类型实例化。


注意到表达式可能很有趣

const :: Int -> Int -> Int

是一种简化(技术上:beta-reduces)原始表达式的表达式,但不可可键入。这里,(\c -> 1 `c` (2 `c` 'a')) const 只使用一次,所以它的类型只能实例化一次,但是没有一个类型实例化可以在两个 const 点使用。这是类型推断引擎的一个已知限制,在执行 Hindley-Milner 推断的所有函数式语言之间共享。

您对 c 的使用存在相同的问题。

一开始看到我们可能有两个表达式可能会令人困惑,一个简化为另一个,但只有一个是可键入的。然而,这是生活中的事实。理论上,Haskell 满足以下“主题缩减”属性:

  • 如果输入表达式 foldr const ....,并且 e1 简化为表达式 e1,则输入表达式 e2

然而,Haskell(与大多数语言一样)无法满足以下“主题扩展”属性:

  • 如果输入表达式 e2,并且 e2 简化为表达式 e1,则输入表达式 e2

因此,虽然类型表达式不可能还原为错误类型,但错误类型表达式可能还原为类型表达式。一个例子就是你找到的那个。更简单的 e1 是错误类型的(它使用字符串作为函数)但简化为 (\x -> True) ("ill-typed" "term") 是类型良好的。

,

您的分析是正确的,尽管在细节上有点欠缺。如果您愿意,您可以在更高的级别查看问题。

foldr :: (a -> r -> r) -> r -> [a] -> r
const :: b -> c -> b

(如果我选择了与您习惯不同的类型变量,请原谅我 - alpha 等价表示变量名称无关紧要,保持名称不同可以更容易地看到发生了什么。)

如果您使用这些类型并统一使 foldr const 工作,您会得到如下结果:

(a -> r -> r) ~ (b -> c -> b)
a ~ b (first arg)
r ~ c (second arg)
r ~ b (result)
r ~ a (by transitivity)

foldr const :: a -> [a] -> a (substitution)

其中 ~ 表示“这些类型是相同的”。

因此您可以仅从 foldrconst 看出列表元素的类型必须与其他参数的类型统一。

不过,您是对的,如果 foldr 在类型检查之前完全内联,则结果表达式将成功检查。但这有点不足。如果你做了foldr const 'a' []怎么办?由于这会减少到 'a',因此它也会进行类型检查 - 但它会使用与传递给它的列表非空不同的类型来进行检查。

而这正是 Haskell 类型系统旨在防止的那种问题。表达式的类型应完全从其子表达式的类型派生。永远不应该考虑值(*),因此无论子表达式是空列表还是非空,表达式都需要具有相同的结果类型。

(*) 好吧,GHC 支持的比 Haskell 2010 多一点。像 GADT 这样的扩展可以启用依赖于值的类型形式,但只能以非常具体的方式来保持更大的连贯属性。

,

我认为,它更简单,而且函数 const 只是不符合 foldr 预期的签名:

Prelude> :t foldr
foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
Prelude> :t const
const :: a -> b -> a

所以haskell 尝试对ab 进行泛化(以发现它们都有足够的类型类集),最后发现1 是一个数字,但 'c' 没有实现这个类型类。

,

那么可能出什么问题了?为什么第一个不工作,它的重写工作?

这是一个有趣的问题,我觉得值得稍微解释一下。

首先,foldr 示例不起作用,因为正如编译器告诉您的那样,类型不匹配。 foldr 具有以下类型,当仅限于列表时,我将以一种与您尝试提供的参数“匹配”的方式编写

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr    const           'a'   [1..2]

从中我们看到类型变量 ab 必须采用特定值 - a 必须是一个数字(您可以将其视为只是 Int,尽管它实际上具有“多态数”类型,Num a => a,即它可以是任何数字类型),而 b 必须是 char。所以这只适用于 const 可以有像

这样的类型
Int -> Char -> Char

或相同的 Int 替换为任何数字类型。

但是,您选择哪种数字类型并不重要,除非(正如编译器指出的那样)您以某种方式为 Num 定义了一个 Char 实例。那是因为 const 有类型

a -> b -> a

所以为了与上面的匹配,ab 都必须是 Char,这意味着数字类型(我在上面假设是 Int,为简单起见)必须是 Char。由于这不是一个(但理论上可以成为一个,而不是一个明智的想法),我希望编译器错误消息现在有意义。

那么为什么你引用的“简写”形式:

(1 `const` (2 `const` 'a')) 

工作?如果编译,这当然也是上面的 foldr 等价的。但是从逻辑上讲,当 foldr 无法编译时,上面的内容也必须如此。它有效是因为 const 是一个多态函数 - 它可以应用于任何类型的任何 2 个参数,并返回第一个。所以它连续减少到(我再次通过简单地对任何数字类型使用 Int 来简化):

1 `const` 2

(使用 const :: Int -> Char -> Int

1

(使用 const :: Int -> Int -> Int

请注意,const 的 2 次调用实际上有 2 种不同的类型。这很好,因为 const 是多态的。但是,将 const 传递给 foldr 并期望它每次在 foldr 内调用时都具有不同的类型是不好的。

这不是任何一种通用规则,至少在您使用 RankNTypes 语言扩展时是这样。使用该扩展,您可以定义接受多态函数作为参数的函数,然后将其应用于不同的类型:

example :: (forall a. a -> a) -> (Int,Bool)
example f = (f 1,f True)

但是 foldr 的签名(如上所示)与此完全不同。尽管其类型签名中的 ab 可以自由变化,但 a 被强制为数字类型,因为您传递给它的是一个数字列表,而 b由于 Char 的累加器而被迫为 'a',因此 const 唯一可以工作的“版本”是一种类型(再次,为了简单起见,专门针对数字类型) Int -> Char -> Char,这不是 const 的可能类型。