连贯性是什么意思？

问题描述

在 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 编译指示似乎是相关的。孤儿实例也会浮现在脑海中。

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

然后有更多看似无辜的扩展，例如通过 OverlappingInstances 扩展或 Overlapping、Overlaps 和 Overlappable 编译指示重叠实例，但即使是 {{1} 的组合}} 和 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 扩展包含在 GHC2021 中，所以我当然希望它们不会破坏连贯性。但我不认为上面的第 1 点是正确的，第 2 点似乎不适用于这里，因为动态语义确实不同。

我还想提一下默认系统。考虑：

MultiParamTypeClasses

默认情况下，GHC（可能还有 Haskell2010？）将默认为 main = print (10 ^ 100) 和 Integer 使用 10。所以结果打印了一个有一百个零的 1。但是如果我们现在添加一个自定义的默认规则：

100

然后 default (Int) main = print (10 ^ 100) 和 10 都默认为类型 100 并且由于包装它只打印一个零。因此表达式 Int 在不同的上下文中具有不同的动态语义。不连贯吗？

所以我的问题是：是否有更正式或更详细的一致性定义可以解决上述问题？

解决方法

不连贯不是因为类型缺乏唯一性。举个例子：

{-# 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），并且具有不同静态类型的程序打字（不同的类型级定理）是不同的程序，所以允许它们有不同的动态语义（不同的术语级证明）。