为什么Haskell将类型家族的阻塞应用程序视为有效类型?

zlwx9yxi  于 2023-01-31  发布在  其他
关注(0)|答案(3)|浏览(157)

以下面的代码片段为例(在各种评论和答案提到它之后,我将类型族更改为封闭的):

-- 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 doc,其中提到“卡住”两次,但没有回答我的问题。
为什么Haskell把EmptyTypeFamily ()当作一个有效的类型,你甚至可以为它定义值等等,当它不是的时候?

6yt4nkrj

6yt4nkrj1#

正如迟浩田所说:说您的类型家族是 * empty * 并不十分准确,它只是碰巧不包含任何已知的示例。
但我认为这没有抓住问题的重点,所以让我们来讨论类型族

type family EmptyTypeFamily t where {}

这个真的是空的你不能为它写任何示例。
但是,这导致了和你观察到的完全一样的行为。为什么?
好吧,GHC在编译过程中对类型的处理在某些方面类似于我们在所有Haskell程序中处理值的方式:惰性求值和模式匹配。众所周知

f :: Int -> Int
f _ = 624

main :: IO ()
main = print $ f undefined

运行时没有问题,即使它将undefined "求值"为f的参数。这没问题,因为f实际上不需要知道关于其参数的任何信息。
类似地,如果你写return untypedValue,那么类型检查器不需要知道关于EmptyTypeFamily ()的任何事情--它只是把它当作一个抽象实体。它甚至可以把不同类型的变量统一为EmptyTypeFamily ()。这只需要假设,不管EmptyTypeFamily是什么,它肯定是确定性的。这一点是有保证的。因为如果你为它写了两个冲突的示例,编译器就会抱怨。
因此,只要您只将untypedValue与无约束多态函数一起使用,它的类型实际上不存在就没有关系,因为它永远不需要进一步求值。
换句话说,NotAType纯粹是 * 符号 *,这有点像数学,你可以写一个定理,以"设 * S * 是一个集合,并且 * x * ∈ * S *,那么 * bla bla *"开始,而不需要确定这个集合是什么,或者 * x * 的值。
只有当您需要附加约束时才会更改,例如将其与具体类型统一
一个二个一个一个
......或者,正如您所观察到的,在它上面使用类型类方法。在每种情况下,编译器都必须从对类型级值EmptyTypeFamily ()执行实际的 * 模式匹配 * 开始。实际上,这是一个更一般的过程:编译器跟踪的是"命题",它有一个知识数据库,其中包含这样和那样的类型是相等的,并且这样和那样的类型匹配这样和那样的类,在这种情况下,GHC只是确定它没有允许对任何已知的Show示例进行决策的信息。
请注意,实际上有可能有一个假设的上下文,其中的信息是可用的,但荒谬的是:

{-# LANGUAGE RankNTypes, FlexibleContexts #-}

hypothetically :: (Show NotAType => r) -> ()
hypothetically _ = ()

main = return $ hypothetically (print untypedValue)

在这种情况下,证明Show NotAType的责任被推迟到hypothetically的实现。当编译器处理print untypedValue时,它只是浏览上下文,并看到Show NotAType将由最终使用hypothetically的参数的任何代码来证明......当然,这永远不会发生。但是编译器在检查main类型时并不担心这个问题。
这在数学上类似于写一个证明,以"让 * x * ∈ R,使得 * x * 2 = -1..."开始--这是完全有效的,并允许你证明令人兴奋的事情。只是,没有人能够 * 使用 * 该定理来计算一些东西,因为不存在具有所需性质的实数。

sr4lhrrt

sr4lhrrt2#

有两个因素意味着GHC需要能够在不立即抛出错误和放弃的情况下考虑卡住的类型族。
首先,正如chi的回答所指出的,通过单独的type instance声明定义的类型族是 open 的,理论上你的模块可以定义EmptyTypeFamilyNotATypeuntypedValue并将它们全部导出,而某个 * 其他 * 模块可以导入你的模块并添加一个使其有意义的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

foo类型中的TF t是一个粘滞型家庭应用;GHC不能在这里解析它,foo声明的类型是否是一个错误取决于变量t,* 变量t取决于foo被**使用的上下文,而不仅仅是它的定义 *。
所以GHC * 需要 * 这种能力来处理由类型表达式给定的类型,而它现在实际上不能解析。考虑到这一点,我并不过分担心它在OP这样的情况下不急于抛出错误(假设EmptyTypeFamily被重写为一个封闭的家族;开放家庭绝对不应该)。我不知道确切的答案,但我一直认为要么是:
1.不可能为GHC制定一个通用的过程,以便能够区分一个有可能因更多信息而摆脱困境的应用程序和一个肯定不能摆脱困境的应用程序。
1.这是可能的,但是不一致性和不可预测性被认为是不可取的。请记住,一些其他的GADT或类型家族可能能够解析任何类型(很像一个非严格函数,不需要定义它的参数),并被应用到一个卡住的家族应用程序中;如果GHC要区分立即抛出错误的“明确卡住”应用程序和“可能无法卡住”的应用程序,程序员就需要始终能够在头脑中做出相同的决定,以判断何时允许复杂情况。
1.这是可能实现的,并且可以很好地预测,但它是一个特殊情况,在一般的处理类型家族,还没有人添加。原始的功能只有开放的家族,我相当肯定,所以原始的胆量类型家族处理将被写没有任何真实的的可能性“绝对卡住”的应用程序存在被检测到。
如果你使用的是封闭类型族,你可以做的一件事就是添加一个解析为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这样的东西,你可能认为它同样可以统一,而不需要任何求值,甚至在ghci中用:t来请求bad的类型,都会产生类型错误。
至少它比No instance for Show (EmptyTypeFamily ())提供了更好的错误消息,因为它会将类型家族解析为类型错误,而不是去寻找可能与卡住的类型家族匹配的示例并抱怨缺少示例。

rdlzhqv9

rdlzhqv93#

因为没有instance EmptyTypeFamily ()
现在还没有这样的例子。
当编译一个模块时,我们还不知道另一个模块是否真的定义了这样的示例,因此我们必须做好准备,这被称为“开放世界假设”。
Haskell允许单独编译,即单独编译每个模块。而且,Haskell允许每个模块添加任意示例。一致地,我们永远不能确定在编译期间示例不存在。
迂腐地说,Haskell也允许 closed 类型族,它不能以这种方式扩展,但是IIRC处理stuck closed类型族就像处理stuck open类型族一样。也许它应该拒绝那些类型族。然而,在closed类型族中,可以通过在closed类型族的定义中添加一个显式的TypeError ".." final case来强制拒绝。

相关问题