haskell - 如何在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

好的，所以你的类型家庭很好，你的属性(property)几乎是正确的。

你要证明的是:

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反射(reflect) : .

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

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

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

现在我们只需要证明它。幸运的是，这是一个 super 简单的性质证明，你只需要对 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 #-}