连贯性是什么意思？

Question

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

程序的每个不同的有效类型派生都会导致生成的程序具有相同的动态语义。

首先，程序没有类型；表达式、变量和函数都有类型。所以我想我会把它解释为每个程序片段（表达式、变量或函数）必须有一个唯一的类型推导。

那我想知道 Haskell（比如 Haskell2010）是否真的连贯？例如。表达式\x -> x 可以赋予类型a -> a，也可以赋予Int -> Int。这是否意味着连贯性被破坏了？我能想到两个反驳：

1. Int -> Int 不是一个有效的类型推导，术语\x -> x 得到推断类型a -> a，它比Int -> Int 严格更通用。

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

以下哪些是正确的？还有其他反驳吗？

现在让我们考虑类型类，因为在这种情况下经常使用连贯性。

GHC 实现的 Haskell 有多种方式可能会破坏一致性。显然IncoherentInstances 扩展和相关的INCOHERENT pragma 似乎相关。孤儿实例也会浮现在脑海中。

但是如果上面的第 1 点是正确的，那么我会说即使这些也不会破坏连贯性，因为我们可以说 GHC 选择的实例是应该选择的一个真实实例（以及所有其他类型推导无效），就像 GHC 推断的类型是必须选择的真实类型一样。所以第 1 点可能不正确。

还有更多看似无害的扩展，例如通过OverlappingInstances 扩展或Overlapping、Overlaps 和Overlappable pragma 重叠实例，但即使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 () ()

如果您担心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，具体取决于上下文。实际上，正如 cmets 中所指出的，这并不完全正确：不同类型的证明/推导略有不同，但证明/推导总是导致相同的动态语义。也就是说，术语级别定义\x -> x 的动态语义始终是“接受一个参数并返回它”，而不管\x -> x 是如何输入的。

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

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

main = print (10 ^ 100)

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