用自己的证明丰富约束求解器

Question

我有以下类型族：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
data Nat = Z | S Nat
type family WrapMaybes (n :: Nat) (a :: *) :: *
type instance WrapMaybes Z a = a
type instance WrapMaybes (S n) a = Maybe (WrapMaybes n a)

这基本上如预期的那样工作，例如WrapMaybes (S (S Z)) Int ~ Maybe (Maybe Int)。

现在，很明显(好吧，除了可能因为终止的原因？！)以下通勤身份成立：WrapMaybes n (Maybe a) ~ Maybe (WrapMaybes n a)

GHC本身无法推断该性质，所以我正在寻找添加该公理的方法，最好是通过一些补充证明。到目前为止，我想出的最好的方法是类型族中的重合重叠。但是所提出的语法似乎已经不起作用了(type instance where触发了语法错误)，所以我只使用了这个：

type instance WrapMaybes n (Maybe a) = Maybe (WrapMaybes n a)

但这让GHC再次抱怨：

Conflicting family instance declarations:
WrapMaybes 'Z a = a
WrapMaybes n (Maybe a) = Maybe (WrapMaybes n a)
Conflicting family instance declarations:
WrapMaybes ('S n) a = Maybe (WrapMaybes n a)
WrapMaybes n (Maybe a) = Maybe (WrapMaybes n a)

因此：

1. 有没有办法使拟议的机制发挥作用？例如，我该如何消除语法错误
2. 重合重叠仍然是GHC Haskell中的一件事吗
3. 还有什么其他机制来教授GHC必要的公理

Answer 1

如本文所述，GHC Haskell中确实存在重合型族重叠。GHC 8.4.3仍然接受文档中的示例以及您链接到的博客文章。

---

然而，我认为重合重叠在这里对你没有帮助，因为根据GHC使用的语法相等性检查，RHS不(不能)相等。基本上，对于重合重叠型族的想法，GHC必须知道你想要"证明"的属性。

为了真正证明这一点，无论何时需要使用这个事实，都需要将您想要的类型平等引入到类型环境中。一种方法是使用Data.Type.Equality:中的:~:

data a :~: b where  -- See Note [The equality types story] in TysPrim
Refl :: a :~: a

这里的基本思想是，当您使用Refl构造函数生成a :~: b类型的值时，GHC必须知道a ~ b。当您稍后在此Refl构造函数上进行模式匹配时，您正在将此等式重新引入GHC的类型环境中。你可以用它来建立一个归纳证明。

然而，为了能够建立归纳证明，您需要能够对Nat的值进行分支，而这在完全处于类型级别时是无法做到的。为了解决这个问题，我们可以引入一个"singleton"GADT:

data SNat (n :: Nat) where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)

当您对类型为SNat的值进行模式匹配时，由于n类型变量的GADT结构，您将向类型环境中引入有关类型级别自然值的信息。

这意味着我们可以编写一个类型如下的函数：

wrapMaybeComm' :: forall n a. SNat n
-> WrapMaybes n (Maybe a) :~: Maybe (WrapMaybes n a)

这里的想法是，如果给它一个(值级别的见证)类型级别的自然n，它将返回一个见证，证明WrapMaybes n (Maybe a)与Maybe (WrapMaybes n a)是一样的。当你在证人身上进行模式匹配时，GHC将确信事实是真实的，并能够使用它。

我们现在可以为wrapMaybeComm'写一个定义，看起来很像是必要事实的归纳证明。基本情况是0:

wrapMaybeComm' SZ = Refl

当n = 0时，GHC立即能够看到Maybe a ~ Maybe a。

在归纳的情况下，我们需要拨打wrapMaybeComm':

wrapMaybeComm' (SS m) = case wrapMaybeComm' @_ @a m of Refl -> Refl

Refl上的模式匹配告诉GHCWrapMaybes m (Maybe a) ~ Maybe (WrapMaybes m a)，其中n ~ 'S m。有了这个，GHC可以看到

WrapMaybes n (Maybe a)
~ WrapMaybes ('S m) (Maybe a)            {- defn. of m -}
~ Maybe (WrapMaybes m (Maybe a))         {- defn. of WrapMaybes -}
~ Maybe (Maybe (WrapMaybes m (Maybe a))) {- IH -}
~ Maybe (WrapMaybes ('S m) (Maybe a))    {- defn. of WrapMaybes -}
~ Maybe (WrapMaybes n (Maybe a))         {- defn of m -}

因此知道右侧的Refl进行了类型检查。

---

如果你不想到处携带SNat，你可以通过定义KnownNat类来用(有时更安静)类型类词典来代替它们，比如

class KnownNat (n :: Nat) where
getSNat :: SNat n
instance KnownNat 'Z where
getSNat = SZ
instance KnownNat n => KnownNat ('S n) where
getSNat = SS getSNat
wrapMaybeComm :: forall n a. (KnownNat n)
=> WrapMaybes n (Maybe a) :~: Maybe (WrapMaybes n a)
wrapMaybeComm = wrapMaybeComm' @n @a getSNat

为了实际使用这个定理，每当你有一个表达式e，GHC因为不知道它与n和a的期望相等性而拒绝进行类型检查时，你可以写case wrapMaybeComm @n @a of Refl -> e，它应该可以工作。

---

这种方法可以用来教授GHC关于各种有趣的归纳事实。在一般情况下，GHC当然不可能知道所有类型都是相等的，因为这需要它能够决定一个相当强大的逻辑系统的任意定理，这是不可能的。然而，许多有趣的归纳定理的证明可以很容易地转换成这种风格，其中的一种变体(没有额外的singletons工作)在依赖类型语言中很常见。

---

附带说明：要使用以上内容，您需要一些额外的GHC Haskell扩展。

• -XGADTs：SNat单例必须是GADT，以确保每个SNat n都有一个值(特别是nSS应用于SZ的值)
• -XScopedTypeVariables：这对于确保使用正确的类型调用证明函数是必要的
• -XTypeOperators：给定的代码使用Data.Type.Equality中的:~:，这是一个类型运算符。然而，可以使用不是类型运算符的等效定义(例如Equal a b而不是a :~: b)
• -XAllowAmbiguousTypes：给定的定义具有GHC所称的不明确类型(需要额外类型签名和/或可见类型应用程序来消除某些tyvar的歧义的函数)。这可以通过使用更多的Proxy参数来解决
• -XTypeApplications：使用此语法(@tyvar语法)是为了方便指定类型变量。但是，应该可以用显式类型注释(有些烦人/冗长)代替