Haskell 类型系统的细微差别答案

【问题标题】：Haskell type system nuancesHaskell 类型系统的细微差别
【发布时间】：2011-10-27 19:24:10
【问题描述】：

我一直在深入了解 haskell 类型系统的本质，并试图了解类型类的精髓。我已经学会了一堆，但是我在下面的代码中遇到了困难。

使用这些类和实例定义：

class Show a => C a where
  f :: Int -> a

instance C Integer where
  f x = 1

instance C Char where
  f x = if x < 10 then 'c' else 'd'

为什么这会通过类型检查：

g :: C a => a -> Int -> a
g x y = f y

yes :: C a => a -> Int -> String
yes x y = show (g x y)

但这不是吗？

g :: C a => a -> Int -> String
g x y = show(f y)

我发现第二种选择更具可读性，而且似乎只有很小的区别（注意类型签名）。但是，试图通过类型检查器会导致：

*Main> :l typetests.hs
[1 of 1] Compiling Main             ( typetests.hs, interpreted )

typetests.hs:11:14:
    Ambiguous type variable `a0' in the constraints:
      (C a0) arising from a use of `f' at typetests.hs:11:14
      (Show a0) arising from a use of `show' at typetests.hs:11:9-12
    Probable fix: add a type signature that fixes these type variable(s)
    In the first argument of `show', namely `(f y)'
    In the expression: show (f y)
    In an equation for `g': g x y = show (f y)
Failed, modules loaded: none.

我不明白为什么。

注意：请不要问“你想做什么？”我希望很明显，我只是在一个抽象的上下文中乱搞，以探索这种语言的工作方式。除了学习新知识之外，我没有其他目标。

谢谢

【问题讨论】：

该死的！第一篇关于 SO 的帖子，我在不到 24 小时内得到了三个很棒且有见地的答案。这个地方太棒了。谢谢大家

标签： class haskell types system

【解决方案1】：

在

g :: C a => a -> Int -> a
g x y = f y

f y 的返回类型由类型签名固定，因此如果您调用，例如将使用g 'a' 3、instance C Char。但是在

g :: C a => a -> Int -> String
g x y = show(f y)

f 的返回类型有两个限制：它必须是C 的实例（以便可以使用f）和Show 的实例（以便可以使用show）。就这样！ f 和 g 的定义中类型变量名称 a 的巧合并不意味着什么。因此编译器无法在instance C Char 和instance C Integer 之间进行选择（或在其他模块中定义的任何实例，因此删除这些实例不会使程序编译）。

【讨论】：

【解决方案2】：

这是一个有趣的玩具发挥作用的地方。考虑标准 Prelude 函数asTypeOf。

asTypeOf :: a -> a -> a
asTypeOf = const

它只返回它的第一个参数，不管第二个参数是什么。但是它上面的类型签名附加了一个约束，即它的两个参数必须是相同的类型。

g :: C a => a -> Int -> String
g x y = show (f y `asTypeOf` x)

现在，GHC 知道f y 的类型。它与g 的第一个参数的类型相同。如果没有这些信息，那么您会收到您看到的错误消息。只是没有足够的信息来确定f y 的类型。而且因为类型很重要（它用于确定show 使用哪个实例），所以GHC 需要知道您要生成代码的类型。

【讨论】：

【解决方案3】：

这是臭名昭著的show . read 问题的变体。经典版使用

read :: Read a => String -> a
show :: Show a => a -> String

所以组合可能看起来是一个普通的旧字符串转换器

moo :: String -> String
moo = show . read

除了程序中没有确定中间类型的信息，所以read然后show。

Ambiguous type variable `b' in the constraints:
  `Read b' arising from a use of `read' at ...
  `Show b' arising from a use of `show' at ...
Probable fix: add a type signature that fixes these type variable(s)

请不要让 ghci 做一堆疯狂的额外默认设置，任意解决歧义。

> (show . read) "()"
"()"

您的C 类是Read 的变体，除了它解码Int 而不是读取String，但问题本质上是相同的。

类型系统爱好者会注意到，受限类型变量本身并不是什么大问题。这是模棱两可的实例推断，这就是这里的问题。考虑

poo :: String -> a -> a
poo _ = id

qoo :: (a -> a) -> String
qoo _ = ""

roo :: String -> String
roo = qoo . poo

在roo的构造中，从来没有确定中间的类型必须是什么，roo在那个类型中也不是多态的。类型推断既不能解决也不能泛化变量！即便如此，

> roo "magoo"
""

这不是问题，因为构造是未知类型的参数。无法确定类型的事实导致类型不重要。

但未知的实例显然很重要。 Hindley-Milner 类型推断的完整性结果依赖于参数性，因此在我们添加重载时会丢失。让我们不要为此哭泣。

【讨论】：