禁用的Haskell类型

有时，编写Haskell就像与编译器发生争执。你给它推理，它就会检查它是否有瑕疵。如果它认为它找到了一个，它会告诉你所有关于它的事情。然后，你必须仔细检查它告诉你的内容，并找出它的确切抱怨是什么。我刚才表达得不好吗？还是我真的错了？或者，在非常偶然的情况下，编译器只是脾气暴躁，您必须解决这个问题。当然，如果你真的对GHC没有接受你的合理论证的计划感到不安，你可以去告诉它的父母。

Haskell的类型系统非常棒，但它没有的一件事是递归类型，这是其他一些类型系统所没有的，我指的是直接从它们自身构造的类型。递归类型在Haskell中是被禁止的。

比方说，我们想要创建一个递归类型T=可能T。官方介绍性的Haskell对此的回答是，不能直接这样做，但是可以很容易地创建一个包含可能T的类型T，有时称为“Newtype wrapper”。就像这样：

很简单。但我们能做得比这更好吗？我们能创建一个实际上等于T的类型吗？我们可以创建禁止的递归类型吗？

type关键字为类型创建别名，别名不能是递归的，因为它们最终必须引用实际类型。

类型族是奇怪的东西。它们不完全是“真正的”类型，但也不只是类型的别名，因为它们不需要完全解析。实际上，您可以在一个模块中声明类型族，将其作为真实类型使用，然后在另一个模块中定义该族的实际实例。

不过，遗憾的是，GHC不允许我们实际使用该实例。它拒绝了T和T可能是同一类型的明显证据：

类型族T，其中T=可能T证明：：T：~：可能T证明=反射

Example.hs：10：9：错误：·Reduce堆栈溢出；简化以下类型时大小=201：t。

这是为什么？这是因为GHC不能只接受别人告诉它的东西，而是没完没了地试图“减少”(即扩大)T=也许T=也许T(可能T)等等，当它达到安全极限时就放弃。您可以将其视为一种智力黑洞，或者编译器的“信息危机”：如果它开始检查您的递归类型的奇怪秘密，它将迷失在无限深渊中，直到内置的应急机制在漩涡中扭曲200次后将其唤醒(如果您愿意，您可以更改这个数字，甚至让它永远运行)。

结果是，我们可以构造一个类型T和一个适当的(非底层)证明值T：~：可能是T，我们只需要谨慎。关键是确保GHC永远不会遇到深不可测的约束T~也许T，因为它会立即陷入对其无穷无尽的思考中。

相反，我们准备了一个既无害又更通用的引理，然后使用TypeApplications扩展仔细地将其专门化以得到我们想要的可怕结论，从而避免了任何类型的推理：

型族A p q其中A()x=可能(Ax())引理：：for all x.。(A()x)：~：可能(A x())引理=Refltype T=A()()证明：：T：~：可能T证明=引理@()。

实际上，构建和解构T的值也需要类似的谨慎。诀窍是，我们不让GHC推断类型。我们不能让GHC去思考，因为一想到坏事就会让它发疯。相反，我们手工应用所有类型。以下是完整的程序，包括所有必要的扩展：

{-#language RankNTypes，TypeApplications，TypeOperators，TypeFamilies，UnecidableInstances，AllowAmbiguousTypes#-}模块main where import Data.Type.Equalitytype family A p q其中A()x=可能(A x())引理：：for all x。(A()x)：~：可能(A x())引理=Refltype T=A()()证明：：T：~：可能T证明=引理@()Convert1：：for all a B.a：~：b->；a->；bConvert1 refl=idConvert2：：for all a B.a：~：B->；b->；aconvert2 refl=idtConvert1：：t-。TtConvert2=Convert2@T@(可能T)Proof Nothing：：TNothing=tConvert2$Nothing@Tust：：t->；tJust x=tConvert2$Just@T xcount：：t->；Intcount t=case tConvert1 t of Nothing->；0 Just t'；->；Succ$count t'；T3：TT3=Just$Just Nothingmain：：IO。

这个程序定义了一个真正的递归类型T=可能T，构造它的一个值，然后解构该值。(它确实可以正确打印“3”。)。另一方面，这比仅仅使用我们应该使用的…的新型要复杂得多