Haskell类型系统的细微差别

Question

我已经深入研究了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.

我不明白为什么.

注意:请不要问"你想做什么？" 我希望很明显,我只是在一个抽象的上下文中乱搞,以探究这种语言的工作方式.除了学习新东西之外,我没有其他目标.

谢谢

Answer 1

这是一个有趣的玩具发挥作用的地方.考虑标准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需要知道生成代码的类型.

Answer 2

这是臭名昭着的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而不是读取a String,但问题基本相同.

类型系统爱好者会注意到欠约束类型变量本身并不重要.这是一个模糊的实例推理,这就是问题所在.考虑

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

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

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

在构造中roo,永远不会确定中间的类型必须是什么,也不是roo该类型的多态.类型推断既不解决也不概括变量!即使是这样,

> roo "magoo"
""

这不是问题,因为构造在未知类型中是参数化的.无法确定类型的事实导致类型无关紧要.

但未知情况下,显然做的事.Hindley-Milner类型推断的完整性结果依赖于参数,因此在我们添加重载时会丢失.让我们不要为此哭泣.

Answer 3

在

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可以使用)的实例.就这样!类型变量名称a的定义f和定义g并不重要.因此编译器无法在instance C Char和之间进行选择instance C Integer(或在其他模块中定义的任何实例,因此删除这些实例不会使程序编译).