连贯性是什么意思？

Question

在Simon Peyton Jones、Mark Jones 和 Erik Meijer的论文“类型类：探索设计空间”中，他们非正式地定义了连贯性如下：

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

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

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

1. Int -> Int不是有效的类型派生，该术语\x -> x获得推断类型a -> a，它比Int -> Int.

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

其中哪些是真的？还有其他反驳吗？

现在让我们考虑类型类，因为在该上下文中经常使用一致性。

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

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

然后还有更多看似无辜的扩展，例如通过OverlappingInstances扩展或Overlapping,Overlaps和Overlappablepragma重叠实例，但即使是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. 所以结果打印了一个有一百个零的 1。但是如果我们现在添加一个自定义的默认规则：

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 () ()。特别是，一种派生使用instance A () b，而另一种派生使用instance A a ()。我强调：这两种派生都导致顶级标识符x :: Either () ()的相同类型和表达式aorb中的相同（静态）类型x = aorb（即Either () ()），但它们导致aorb在为 生成的代码中使用不同的术语级别定义x。也就是说，x根据使用两个有效类型派生中的哪一个，将展示具有相同静态语义（类型级计算）的不同动态语义（术语级计算）。

这就是不连贯的本质。

所以，回到你最初的问题......

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

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

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

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

main = print (10 ^ 100)

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