haskell - 连贯性是什么意思？

Question

在论文"Type classes: exploring the design space"由 Simon Peyton Jones、Mark Jones 和 Erik Meijer 所著，他们非正式地定义了连贯性如下:

Every different valid typing derivation for a program leads to a resulting program that has the same dynamic semantics.

首先，程序没有类型；表达式、变量和函数都有类型。所以我想我会把它解释为每个程序片段(表达式、变量或函数)必须有一个唯一的类型派生。
然后我想知道Haskell(比如Haskell2010)是否真的连贯？例如。表达式 \x -> x可以给出类型 a -> a , 还有 Int -> Int .这是否意味着连贯性被破坏了？我可以想到两个反驳:

Int -> Int不是有效的类型推导，术语 \x -> x获取推断类型 a -> a这比 Int -> Int 更一般。 .

两种情况下的动态语义相同，只是类型 Int -> Int不太通用，在某些情况下会被静态拒绝。

以下哪些是真的？还有其他反驳吗？
现在让我们考虑类型类，因为在这种情况下经常使用连贯性。
GHC 实现的 Haskell 有多种方式可能会破坏一致性。显然 IncoherentInstances扩展和相关 INCOHERENT pragma 似乎相关。孤儿实例也浮现在脑海中。
但是如果上面的第 1 点是正确的，那么我会说即使这些也不会破坏连贯性，因为我们可以说 GHC 选择的实例是应该选择的一个真实实例(并且所有其他类型派生都是无效的)，就像 GHC 推断的类型是必须选择的真实类型一样。所以第1点可能不正确。
然后通过 OverlappingInstances 出现更多看似无害的扩展，例如重叠实例。扩展名或 Overlapping , Overlaps和 Overlappable编译指示，但即使是 MultiParamTypeClasses 的组合和 FlexibleInstances可以产生重叠的实例。例如。

class A a b where
  aorb :: Either a b

instance A () b where
  aorb = Left ()

instance A a () where
  aorb = Right ()

x :: Either () ()
x = aorb

FlexibleInstances和 MultiParamTypeClasses扩展名包含在 GHC2021 中所以我当然希望他们不会破坏连贯性。但我不认为上面的第 1 点是正确的，第 2 点在这里似乎并不适用，因为动态语义确实不同。
我还想提一下默认系统。考虑:

main = print (10 ^ 100)

默认情况下，GHC(可能还有 Haskell2010？)将默认使用 Integer两个 10和 100 .所以结果打印出一个有一百个零的一。但是如果我们现在添加一个自定义的默认规则:

default (Int)

main = print (10 ^ 100)

然后两个 10和 100默认类型为 Int并且由于包装它只打印一个零。所以表达式 10 ^ 100在不同的上下文中具有不同的动态语义。这不连贯吗？
所以我的问题是:是否有更正式或更详细的连贯性定义可以解决上述问题？

Answer 1

不连贯不是由于缺乏类型的唯一性造成的。举个例子:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

class A a b where
  aorb :: Either a b

instance A () b where
  aorb = Left ()

instance A a () where
  aorb = Right ()

x :: Either () ()
x = aorb

在这里唯一分配类型没有问题。具体来说，模块中定义的顶级标识符的类型/种类是:

A :: Type -> Type -> Constraint
aorb :: (A a b) => Either a b
x :: Either () ()

如果您关心表达式的类型 aorb用于 x = aorb 的右侧，这是明确的 Either () () .您可以使用类型通配符 x = (aorb :: _)验证这一点:

error: Found type wildcard '_' standing for 'Either () ()'

该程序不连贯的原因(以及 GHC 拒绝它的原因)是 x :: Either () () 类型的多个类型 DERIVATIONS是可能的。特别是，一种推导使用 instance A () b ，而另一个使用 instance A a () .我强调:两个派生导致顶级标识符 x :: Either () () 的相同类型。和表达式 aorb 的相同(静态)类型在 x = aorb (即 Either () () )，但它们导致 aorb 的不同术语级定义在为 x 生成的代码中使用.也就是说， x将表现出不同的动态语义(术语级计算)和相同的静态语义(类型级计算)，具体取决于使用了两个有效类型派生中的哪一个。
这就是不连贯的本质。
所以，回到你最初的问题......
您应该将“程序的类型派生”视为整个类型检查过程，而不仅仅是分配给程序片段的最终类型。形式上，程序的“类型化”(即其所有组成部分的类型)是一个定理，必须证明该定理才能接受程序的类型化。程序的“类型推导”就是该定理的证明。程序的静态语义由定理的陈述决定。动态语义部分由该定理的证明决定。如果两个有效的推导(证明)导致相同的静态类型(定理)但不同的动态语义，则程序是不连贯的。
表达式 \x -> x可以键入 a -> a或 Int -> Int , 取决于上下文，但可能有多种类型的事实与不连贯性无关。事实上， \x -> x总是连贯的，因为可以使用相同的“证明”(类型推导)来证明类型 a -> a或 Int -> Int ，取决于上下文。实际上，正如评论中指出的那样，这并不完全正确:不同类型的证明/推导略有不同，但证明/推导总是导致相同的动态语义。即术语级别定义的动态语义 \x -> x无论 \x -> x 如何，总是“接受一个参数并返回它”是键入的。
扩展 FlexibleInstances和 MultiParamTypeClasses可以引入不连贯性。事实上，你上面的例子被拒绝了，因为它不连贯。重叠实例提供了一种重新获得连贯性的机制，通过优先考虑某些派生而不是其他派生，但它们在这里不起作用。让您的示例编译的唯一方法是使用不连贯的实例。
违约也与连贯性无关。默认情况下，程序:

main = print (10 ^ 100)

有一个分配类型 Integer 的类型至 10和 100 .使用不同的默认值，同一程序具有分配类型 Int 的类型。至 10和 100 .在每种情况下，程序的静态类型都不同(即表达式 10 ^ 100 在第一种情况下具有静态类型 Integer，在第二种情况下具有 Int)，并且具有不同静态类型的程序(不同的类型级别定理)是不同的程序，因此允许它们具有不同的动态语义(不同的术语级证明)。