如何证明 haskell 中的类型级列表属性？

Question

我有这些类型的家庭：

type family xs ++ ys where
  '[]      ++ ys = ys
  (x : xs) ++ ys = x : (xs ++ ys)

type family Drop n xs where
  Drop  O         xs  = xs
  Drop (S n) (_ : xs) = Drop n xs

type family Length xs where
  Length '[] = O
  Length  (x : xs) = S (Length xs)

在某些时候，GHC 需要证明

forall a. Drop (Length a) (a ++ c) ~ c

我曾经将其推入某些构造函数的上下文中。

我如何证明这个属性具有普遍性？

Answer 1

好的，所以你的字体家族很好，你的属性几乎是正确的。

你要证明的是：

proof :: Drop (Length a) (a ++ c) :~: c

除非你真的不知道 a 和 c 是什么。它们是隐式量化的。您希望它们是明确的，以便我们可以对它们进行归纳。

proof :: (a :: [ k ]) -> (c :: [ k ]) -> Drop (Length a) (a ++ c) :~: c

你会意识到这不会进行类型检查，因为 Haskell 没有真正的依赖类型，但有一个解决方法：单例类型。这个想法是创建一个索引类型，以便每个术语对应于用作类型索引的不同类型的一个术语。我知道这听起来有点令人困惑，但示例应该可以澄清这一点。

您可以使用 singletons 库或从头开始构建它们，这就是我在这里所做的。

data family Sing (x :: k)

data SList xs where
  SNil  :: SList '[]
  SCons :: Sing x -> SList xs -> SList (x ': xs)

这里 Sing 是一个数据族，因此我可以泛指具有单例的事物。 SList 是列表类型的单例版本，如您所见，SNil 构造函数对应于类型级别 []。同样，SCons 反映了 :.

然后（假设你在某处也有 data Nat = O | S Nat 的定义）你所追求的证明的签名是

proof :: SList a -> SList c -> Drop (Length a) (a ++ c) :~: c

请注意，我将您的 ~ 更改为 :~:，这是 Data.Type.Equality 中可用的类型运算符。它唯一的构造函数是 Refl ，只有当它的两个操作数完全相同时你才能断言。

现在我们只需要证明它。幸运的是，这是一个非常简单的属性证明，你只需要对 SList a

进行归纳

在基本情况下 SList a 是 SNil，因此您实际上是在尝试证明 Drop (Length '[]) ('[] '++ c) :~: c。因为您使用了类型族，类型检查器会立即将其减少为 c :~: c。由于两个操作数相同，我们可以使用 Refl 构造函数来证明这种情况。

proof SNil _ = Refl

现在是归纳案例。我们将再次进行模式匹配，这一次了解到 SList a 的形式是 SCons a as 以及 a :: Sing x 和 as :: Sing xs。这意味着我们需要证明的是Drop (Length (x ': xs)) ((x : xs) ++ c) :~: c。同样，您的类型族将立即开始计算并将此目标降低到 Drop (Length xs) (xs ++ c) :~: c，因为它实际上不需要知道 x 是什么来进行评估。

事实证明，proof as c（注意，我使用 as 而不是 SCons a as）具有所需的类型，所以我们用它来证明属性.

这是完整的证明。

proof :: SList a -> SList c -> Drop (Length a) (a ++ c) :~: c
proof SNil _ = Refl
proof (SCons a as) cs = proof as cs

要使这些正常工作，您需要所有这些语言扩展：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}

如何证明 haskell 中的类型级列表属性？

How do I prove type-level list properties in haskell?

haskell

types

proof

type-level-computation