为什么 Haskell 将类型族的卡住应用程序视为有效类型？

Question

拿这个代码片段（在各种评论和答案提到它之后，我将类型系列更改为封闭类型）：

-- a closed type family for which I won't define any instances
type family EmptyTypeFamily t where

-- 1. this type doesn't exist, since there's no `instance EmptyTypeFamily ()`
type NotAType = EmptyTypeFamily ()

-- 2. this value has a type that doesn't exist
untypedValue :: NotAType
untypedValue = undefined

main :: IO ()
main = do
  -- 3. the value with no type can be used in expressions
  return untypedValue
  return . id . fix $ \x -> untypedValue
  
  -- ERROR, finally! No instance for `Show (EmptyTypeFamily ())`
  print untypedValue

我发现我可以命名类型族的卡住应用程序 (1)，甚至为其定义值 (2) 并在表达式 (3) 中使用它们，这非常违反直觉。当然，我无法为其定义任何类型类实例，因为该类型甚至不存在。但是，仅仅通过命名该非类型，我不应该得到一个错误，更不用说使用它了？这使得检测代码中的问题变得更加困难。我读了GHC 文档，其中提到“卡住”两次，但没有回答我的问题。

为什么 Haskell 将其视为EmptyTypeFamily ()有效类型，您甚至可以为其定义值等，但实际上并非如此？

Answer 1

正如 chi 所说：说你的类型族是空的并不是很准确，而是它只是碰巧不包含任何已知的实例。
但我认为这没有抓住问题的重点，所以让我们讨论一下类型族

\n

type family EmptyTypeFamily t where {}\n

\n

这个确实是空的：您无法为其编写任何实例。

\n

尽管如此，这会导致与您观察到的行为完全相同的行为。为什么？

\n

好吧，GHC 在编译期间对类型所做的事情在某些方面与我们在所有 Haskell 程序中处理值的方式类似：惰性求值和模式匹配。众所周知，该程序是如何

\n

f :: Int -> Int\nf _ = 624\n\nmain :: IO ()\nmain = print $ f undefined\n

\n

运行没有问题，即使它将 \xe2\x80\x9ce 评估 \xe2\x80\x9dundefined作为 的参数f。没关系，因为f实际上不需要了解其参数的任何信息。

\n

类似地，如果您编写return untypedValue，则类型检查器不需要了解有关EmptyTypeFamily ()\xe2\x80\x93 的任何信息，它只是将其视为抽象实体。它甚至可以将不同类型的变量统一为EmptyTypeFamily (). 这只需要这样的假设：无论EmptyTypeFamily幕后是什么，它肯定是确定性的。这是有保证的，因为如果您为其编写了两个冲突的实例，编译器会抱怨。

\n

因此，只要您只使用untypedValue无约束多态函数，它的类型实际上不存在就没关系，因为它永远不需要进一步评估。

\n

换句话说，NotAType纯粹是象征性的。这有点像数学，你可以写一个以 \xe2\x80\x9clet S开始的定理，x \xe2\x88\x88 S，然后bla bla \xe2\x80\x9d ，而不需要实际确定这个集合是什么是 或x的值。

\n

仅当您需要额外的约束时才会改变，例如将其与具体类型统一

\n

f :: Int -> Int\nf x = x + 1\n\nmain = print $ f untypedValue\n

\n

    \xe2\x80\xa2 无法将类型 \xe2\x80\x98EmptyTypeFamily ()\xe2\x80\x99 与 \xe2\x80\x98Int\xe2\x80\x99\n 匹配类型: Int\n 实际类型: NotAType \n \xe2\x80\xa2 在\xe2\x80\x98f\xe2\x80\x99的第一个参数中，即\xe2\x80\x98untypedValue\xe2\x80\x99\n

\n

...或者，正如您所观察到的，对其使用类型类方法。在每种情况下，编译器都必须首先对类型级别值执行实际的模式匹配EmptyTypeFamily ()。好吧，事实上这是一个更通用的过程：编译器跟踪的是命题。它有一个知识数据库，其中此类类型是相等的，并且此类类型与此类相匹配，在这种情况下，GHC 只是确定它没有允许决定任何已知Show实例的信息。

\n

请注意，实际上可以有一个假设的上下文，其中该信息可用，无论多么荒谬：

\n

{-# LANGUAGE RankNTypes, FlexibleContexts #-}\n\nhypothetically :: (Show NotAType => r) -> ()\nhypothetically _ = ()\n\nmain = return $ hypothetically (print untypedValue)\n

\n

在这种情况下，证明责任Show NotAType被推迟到实施hypothetically。当编译器处理它时，print untypedValue它只是浏览上下文并看到Show NotAType最终使用 的参数的任何代码都将证明这一点hypothetically。...这当然永远不会发生，但编译器在类型检查时不会担心这一点main。

\n

在数学类比中，这就像编写一个以 \xe2\x80\x9clet x \xe2\x88\x88 \xe2\x84\x9d 开头的证明，使得x ² = -1...\xe2\x80\x9d \ xe2\x80\x93 这是完全有效的，可以让你证明令人兴奋的事情。只是，没有人能够使用该定理来计算某些东西，因为不存在具有所需属性的实数。

\n

Answer 2

有两个因素意味着 GHC 需要能够考虑陷入困境的类型族，而不会立即抛出错误并放弃。

首先，正如 chi 的回答所指出的，通过单独type instance声明定义的类型族是open 的。理论上，您的模块可以定义EmptyTypeFamily、NotAType和untypedValue并将它们全部导出，而其他模块则可以导入您的模块并添加type instance EmptyTypeFamily ()有意义的声明。

但也存在封闭类型族，其中任何导入该类型族的模块都静态地知道实例集。人们很容易说，如果无法解决这些问题，至少应该立即抛出错误，实际上，在像您这样的情况下，类型系列的所有参数都是完全具体的类型，这可以想象可以完成。但是 GHC 需要卡住类型族概念的第二个原因是，类型族通常用于具有类型变量的更复杂的情况。考虑一下：

{-# LANGUAGE TypeFamilies #-}

type family TF t
  where TF Bool = Int
        TF Char = Bool

foo :: t -> TF t -> TF t
foo = flip const

类型TF t为foo卡顿式家庭应用；GHC 无法在这里解决它。for 的声明类型是否foo错误取决于变量t，而变量取决于使用的foo上下文，而不仅仅是其定义。

因此，GHC需要这种能力来处理具有由类型表达式给出的类型的事物，但它现在无法实际解析。鉴于此，我并不太担心它在像OP这样的情况下不会急切地抛出错误（假设EmptyTypeFamily被重写为一个封闭的家庭；它绝对不应该与开放的家庭一起）。我不太清楚，但我一直认为是：

1. 不可能为 GHC 制定一个通用程序来区分卡住的应用程序（可能需要更多信息才能摆脱卡住）和绝对不能的应用程序。
2. 这是可能的，但不一致和不可预测性并不被认为是可取的。请记住，其他一些 GADT 或类型族可能能够解析任何类型（很像非严格函数不一定需要定义其参数），并应用于卡住的族应用程序；如果 GHC 区分立即引发错误的“绝对卡住”应用程序和“可能无法卡住”应用程序，那么程序员需要始终能够在头脑中做出相同的决定，以判断何时允许复杂情况。我真的不确定这是否能让工作愉快。
3. 它是可能实现的，并且可以很好地预测，但它是类型族一般处理中的一种特殊情况，目前还没有人添加。我相当确定，最初的功能只有开放族，因此类型族处理的原始内容将在没有任何真正可能检测到“绝对卡住”的应用程序的情况下编写。

如果您使用封闭类型系列，您可以做的一件事是添加一个解析为TypeError. 就像这样：

{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}

-- These are in GHC.TypeError as of base 4.17, but the current
-- default on my system is base 4.16. GHC.TypeLits still exports
-- them for backwards compatibility so this will work, but might
-- eventually be deprecated?
import GHC.TypeLits ( TypeError
                    , ErrorMessage ( Text, ShowType, (:<>:) )
                    )
type family TF t
  where TF t = TypeError (Text "No TF instance for " :<>: ShowType t)

bad :: TF ()
bad = undefined

这有帮助，但它并不能捕获卡住的TF应用程序的所有可能的使用情况。它不会捕获像 之类的定义bad，因为它对于实际评估仍然“懒惰” TF ()；你告诉它类型是TF ()，并且实现是undefined，它可以是任何类型，因此它很高兴地与TF ()类型检查相结合并通过类型检查，而编译器不需要实际评估TF ()。但它确实比卡住类型系列应用程序捕获更多的情况，因为它没有卡住：它解决了类型错误。如果您有任何其他绑定必须推断类型并且这取决于 的类型bad，那么它似乎会遇到错误；甚至像boom = bad您认为它同样能够在没有任何评估的情况下统一的地方。bad甚至询问ghci 中的类型也会:t生成类型错误。

至少它会为您提供更好的错误消息，No instance for Show (EmptyTypeFamily ())因为它将类型族解析为类型错误，而不是去寻找可以匹配卡住类型族的实例并抱怨丢失的实例。