假设长度为n的列表L插入长度为n +1的列表J中。我们想知道，对于J的每个元素，L中的哪个邻居更大。下面的函数需L作为其输入，并产生一个列表K，也长度的n + 1个，使得我的K个元素是所期望的邻居我J.的第i个元素
aux [] prev acc = prev:acc
aux (hd:tl) prev acc = aux tl hd ((max hd prev):acc)
expand row = reverse (aux row 0 [])
我可以非正式地向自己证明，此函数的结果的长度（我最初在Ocaml中写过）比输入的长度大一。但是我跳到了Haskell（对我来说是一种新语言），因为我对能够通过类型系统证明此不变式成立感兴趣。借助先前的答案，我可以做到以下几点：
{-# LANGUAGE GADTs, TypeOperators, TypeFamilies #-}
data Z
data S n
type family (:+:) a b :: *
type instance (:+:) Z n = n
type instance (:+:) (S m) n = S (m :+: n)
-- A List of length 'n' holding values of type 'a'
data List a n where
Nil :: List a Z
Cons :: a -> List a m -> List a (S m)
aux :: List a n -> a -> List a m -> List a (n :+: (S m))
aux Nil prev acc = Cons prev acc
aux (Cons hd tl) prev acc = aux tl hd (Cons (max hd prev) acc)
但是，最后一行会产生以下错误：
* Could not deduce: (m1 :+: S (S m)) ~ S (m1 :+: S m)
from the context: n ~ S m1
bound by a pattern with constructor:
Cons :: forall a m. a -> List a m -> List a (S m),
in an equation for `aux'
at pyramid.hs:23:6-15
Expected type: List a (n :+: S m)
Actual type: List a (m1 :+: S (S m))
* In the expression: aux tl hd (Cons (max hd prev) acc)
In an equation for `aux':
aux (Cons hd tl) prev acc = aux tl hd (Cons (max hd prev) acc)
* Relevant bindings include
acc :: List a m (bound at pyramid.hs:23:23)
tl :: List a m1 (bound at pyramid.hs:23:14)
aux :: List a n -> a -> List a m -> List a (n :+: S m)
(bound at pyramid.hs:22:1)
看来我需要做的就是告诉编译器(x :+: (S y)) ~ S (x :+: y)。这可能吗？
或者，是否有比类型系统更好的工具来解决此问题？
首先，一些导入和语言扩展：
{-# LANGUAGE GADTs, TypeInType, RankNTypes, TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes #-}
import Data.Type.Equality
现在，我们有了DataKinds（或TypeInType），可以将任何数据提升到类型级别（具有自己的种类），因此，真正应将类型级别的自然值定义为常规类型data（哎呀，这正是先前链接到的激励示例） GHC文档给出！）。您的List类型没有任何变化，但(:+:)实际上应该是一个封闭的类型家族（现在是实物Nat）。
-- A natural number type (that can be promoted to the type level)
data Nat = Z | S Nat
-- A List of length 'n' holding values of type 'a'
data List a n where
Nil :: List a Z
Cons :: a -> List a m -> List a (S m)
type family (+) (a :: Nat) (b :: Nat) :: Nat where
Z + n = n
S m + n = S (m + n)
现在，为了使证明适用于aux，为自然数定义单例类型很有用。
-- A singleton type for `Nat`
data SNat n where
SZero :: SNat Z
SSucc :: SNat n -> SNat (S n)
-- Utility for taking the predecessor of an `SNat`
sub1 :: SNat (S n) -> SNat n
sub1 (SSucc x) = x
-- Find the size of a list
size :: List a n -> SNat n
size Nil = SZero
size (Cons _ xs) = SSucc (size xs)
现在，我们已经准备好开始证明一些东西。来自Data.Type.Equality，a :~: b表示的证明a ~ b。我们需要证明关于算术的一件事。
-- Proof that n + (S m) == S (n + m)
plusSucc :: SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSucc SZero _ = Refl
plusSucc (SSucc n) m = gcastWith (plusSucc n m) Refl
最后，我们可以gcastWith在中使用此证明aux。哦，您错过了Ord a约束。:)
aux :: Ord a => List a n -> a -> List a m -> List a (n + S m)
aux Nil prev acc = Cons prev acc
aux (Cons hd tl) prev acc = gcastWith (plusSucc (size tl) (SSucc (size acc)))
aux tl hd (Cons (max hd prev) acc)
-- append to a list
(|>) :: List a n -> a -> List a (S n)
Nil |> y = Cons y Nil
(Cons x xs) |> y = Cons x (xs |> y)
-- reverse 'List'
rev :: List a n -> List a n
rev Nil = Nil
rev (Cons x xs) = rev xs |> x
让我知道这是否回答了您的问题-这类事情的开始涉及很多新事物。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句