连贯性是什么意思？

Question

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

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？）将默认对 10 和 100 使用 Integer。所以结果打印出一个带有一百个零的一。但是如果我们现在添加自定义默认规则：

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

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

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

如果您关心 x = aorb 右侧使用的表达式 aorb 的类型，则毫无疑问是 Either () ()。您可以使用类型通配符 x = (aorb :: _) 来验证这一点：

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

这个程序不连贯的原因（以及 GHC 拒绝它的原因）是 x :: Either () () 类型的多个类型 DERIVATIONS 是可能的。特别是，一个推导使用 instance A () b，而另一个使用 instance A a ()。我强调：这两种推导都会导致顶级标识符 x :: Either () () 的相同类型和 x = aorb 中表达式 aorb 的相同（静态）类型（即 Either () ()），但它们会导致在为 x 生成的代码中使用 aorb 的不同术语级定义。也就是说，x 将使用相同的静态语义（类型级计算）展示不同的动态语义（术语级计算），具体取决于使用两个有效类型推导中的哪一个。

这就是不连贯的本质。

所以，回到你原来的问题...

您应该将“程序的类型推导”视为整个类型检查过程，而不仅仅是分配给程序片段的最终类型。形式上，程序的“类型”（即其所有组成部分的类型）是一个必须证明接受程序以及类型的定理。程序的“类型推导”就是该定理的证明。程序的静态语义由定理的陈述决定。动态语义部分由该定理的证明决定。如果两个有效的推导（证明）导致相同的静态类型（定理）但不同的动态语义，则程序不连贯。

表达式 \x -> x 可能会打成 a -> a 或 Int -> Int，这取决于上下文，但可能出现多个打字这一事实与不连贯无关。事实上，\x -> x 始终是连贯的，因为根据上下文，可以使用相同的“证明”（类型推导）来证明类型 a -> a 或 Int -> Int。实际上，正如评论中指出的那样，这不太正确：proof/derivation 对于不同的类型略有不同，但 proof/derivation 总是导致相同的动态语义。也就是说，术语级别定义 \x -> x 的动态语义总是“接受一个参数并 return 它”，而不管 \x -> x 是如何键入的。

扩展 FlexibleInstances 和 MultiParamTypeClasses 可能会导致不连贯。事实上，你上面的例子被拒绝了，因为它不连贯。重叠实例提供了一种机制来重新获得连贯性，通过将一些推导优先于其他推导，但它们在这里不起作用。让您的示例编译的唯一方法是使用不连贯的实例。

违约也与连贯性无关。默认情况下，程序：

main = print (10 ^ 100)

具有将类型 Integer 分配给 10 和 100 的类型。使用不同的默认设置，同一个程序有一个将类型 Int 分配给 10 和 100 的类型。在每种情况下，程序的静态类型都是不同的（即表达式 10 ^ 100 在第一种情况下具有静态类型 Integer 而在第二种情况下具有 Int ），并且具有不同静态的程序打字（不同的类型级定理）是不同的程序，因此允许它们具有不同的动态语义（不同的术语级证明）。

连贯性是什么意思？

What does coherence mean?

haskell

type-systems

ghc