我有这些类型的家庭:
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. I use as
instead 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 #-}
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句