gpt4 book ai didi

haskell - 使用类型系统检查输出与输入列表的长度

转载 作者:行者123 更新时间:2023-12-01 23:54:40 24 4
gpt4 key购买 nike

假设长度为 n 的列表 L 与长度为 n + 1 的列表 J 交错。我们想知道,对于 J 的每个元素,L 中它的邻居中哪个元素更大。以下函数将 L 作为输入,并生成一个列表 K,其长度也是n + 1,使得 K 的第 i 个元素是 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 编写)比输入的长度大 1。但是我跳到 Haskell(对我来说是一门新语言),因为我对成为能够通过类型系统证明这个不变量成立。有了。。的帮助的this previous answer , 我曾是能够达到以下目的:

{-# 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 (or TypeInType)这允许我们将任何数据提升到类型级别(具有其自己的类型),因此类型级别自然值确实值得被定义为常规数据(哎呀,这个正是前面的 GHC 文档链接给出的激励示例!)。 List 类型没有任何变化,但 (:+:) 确实应该是一个封闭类型系列(现在超过了类似的纳特)。

-- 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,定义 singleton types 很有用。对于自然数。

-- 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
<小时/>

如果这能回答您的问题,请告诉我 - 开始处理此类事情涉及很多新东西。

关于haskell - 使用类型系统检查输出与输入列表的长度,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/42148901/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com