我有这些类型家族：
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
我曾经把它推到某些构造函数的上下文中。
我如何普遍证明此属性？
好的，所以您的类型家族很好，您的财产也差不多。
您要证明的是：
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。我使用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 #-}