代码之家 › 专栏 › 技术社区 › Sebastian Graf

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

type-families ghc haskell

Sebastian Graf · 技术社区 · 6 年前

我有以下类型的家庭:

{-# 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本身无法推断出该属性,所以我正在寻找方法来增加公理,最好是通过一些补充证明。到目前为止我能想到的最好的办法是 coincident overlap in type families 是的。但是提议的语法似乎不再有效了( 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)

所以:

有办法使拟议的机制发挥作用吗?如何消除语法错误?
在ghc haskell中重合重叠仍然是一件事吗?
还有什么其他的机制来教导GHC必要的公理?

1 回复 | 直到 6 年前

Lucy Maya Menon 6 年前

如文献所述,在ghc haskell中确实仍然存在重合型家族重叠。 here .文档中的示例和链接到的博客文章仍然被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

这里的基本思想是,当您将 a :~: b 通过使用 Refl 构造器,ghc必须知道 a ~ b 是的。当你以后在这个上面匹配图案的时候 回流 构造函数,您正在将此等式引入ghc的类型环境中。你可以用这个来建立归纳证明。

然而,为了能够建立归纳证明,您将需要能够分支于 Nat ,当它完全处于类型级别时,不能执行此操作。为了解决这个问题,我们可以引入一个“singleton”gadt:

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

当对类型的值进行模式匹配时 SNat ,您将在类型环境中引入关于类型级别natural值的信息,这是由于 n 输入变量。

这意味着我们可以编写这样一个类型的函数:

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' (SS m) = case wrapMaybeComm' @_ @a m of Refl -> Refl

上的模式匹配 回流 告诉GHC WrapMaybes 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 -}

所以我知道 回流 在右边打支票。

如果你不想随身携带 陷阱 到处都是,您可以通过定义 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当然不能意识到所有类型的相等,因为这需要它能够决定一个相当强大的逻辑系统的任意定理,这是不可能的。然而,许多有趣的归纳定理的证明可以很容易地转换成这种风格,其中的一种变体(没有额外的单例工作)在依赖类型语言中非常常见。

附带说明:要使用上述内容,您需要一些额外的ghc haskell扩展。

-XGADTs :snat singleton必须是gadt,以确保每个 SNat n (具体来说, n个 SS 应用于 SZ )中。
-XScopedTypeVariables :这对于确保对证明函数的调用使用正确的类型是必要的。
-XTypeOperators :给定代码使用 :~: 从 数据类型相等 ,这是类型运算符。不是类型运算符的等效定义(例如 Equal a b 而不是 A:~:B )但是,可能已经被使用了。
-XAllowAmbiguousTypes :给定的定义具有ghc所称的不明确类型(需要额外类型签名和/或可见类型应用程序来消除某些tyvars的歧义的函数)。这可以通过使用更多 Proxy 参数。
-XTypeApplications :这个 @tyvar 语法)用于方便指定类型变量。但是,它应该可以替换为(更烦人/冗长的)显式类型注释。