如何在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(nb. I use asinstead of 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 #-}