什么是一致性？

Question

什么是一致性？

haskellghctype-systems

7

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

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

首先，程序没有类型；表达式、变量和函数具有类型。因此，我认为它的含义是每个程序片段（表达式、变量或函数）必须具有唯一的类型推导。

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

Int -> Int不是有效的类型推导，术语\x -> x获得了推断类型a -> a，严格来说比Int -> Int更通用。
动态语义在两种情况下都相同，只是类型Int -> Int不够通用，在某些情况下会被静态拒绝。

这些哪些是真的？还有其他反驳观点吗？

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

在GHC实现的Haskell中，有几种可能破坏一致性的方法。显然，IncoherentInstances扩展和相关的INCOHERENT pragma似乎很相关。孤儿实例也值得一提。

如果上面的第一点是真的，那么我会说即使这些也不会破坏一致性，因为我们可以说 GHC 选择的实例是应该被选择的唯一真实实例（所有其他类型推导都是无效的），就像 GHC 推导出的类型是必须被选择的真实类型一样。所以第一点可能不成立。

然后还有更加无害的扩展，比如通过 OverlappingInstances 扩展或 Overlapping、Overlaps 和 Overlappable pragmas 实现的重叠实例，但是即使是 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中，因此我希望它们不会破坏一致性。但我认为上面的第一点不正确，第二点似乎不适用于这里，因为动态语义确实不同。

我还想提到默认系统。请考虑：

main = print (10 ^ 100)

默认情况下，GHC（和可能是Haskell2010？）将默认使用Integer来表示10和100。因此，结果会打印一个带有一百个零的数字。但是，如果我们现在添加自定义默认规则：

default (Int)

main = print (10 ^ 100)

那么，10和100都默认为类型Int，由于包装，这只打印一个零。因此，在不同的上下文中，表达式10 ^ 100具有不同的动态语义。这是否不连贯？

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

- Noughtmare

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- K. A. Buhr · Accepted Answer

不一致性并不是类型缺乏唯一性导致的。以你的例子为例：

{-# 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 () ()的多个类型派生可能性。特别是，一个导出使用instance A()b，而另一个导出使用instance A a()。我强调：这两个导出都导致顶级标识符x :: Either ()()和x = aorb中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) 该程序有一个类型指定，将10和100指定为Integer类型。在不同的默认设置下，同一程序有一个类型指定，将10和100指定为Int类型。在每种情况下，程序的静态类型是不同的（即，表达式10 ^ 100在第一种情况下具有静态类型Integer，而在第二种情况下具有静态类型Int），并且具有不同静态类型（不同类型级别的定理）的程序是不同的程序，所以它们可以具有不同的动态语义（不同的项级证明）。