haskell 中的单调序列类型

Question

我想为 haskell 中的无限数列定义一个类型。我的想法是：

type MySeq = Natural -> Ratio Integer

不过，我也希望能够在类型级别上定义序列的一些属性。一个简单的例子就是像这样的非递减序列。使用 GHC 的当前依赖类型功能可以做到这一点吗？

编辑：我想出了以下想法：

type PositiveSeq = Natural -> Ratio Natural
data IncreasingSeq = IncreasingSeq {
  start :: Ratio Natural,
  diff :: PositiveSeq}

type IKnowItsIncreasing = [Ratio Natural]

getSeq :: IncreasingSeq -> IKnowItsIncreasing
getSeq s = scanl (+) (start s) [diff s i | i <- [1..]]

当然，这基本上是一种 hack，实际上根本不安全。

Answer 1

这并没有对类型做任何特别的事情，但您可以改变解释自然数序列的方式以获得基本相同的保证。

我认为您在编辑问题时的思路是正确的。考虑

data IncreasingSeq = IncreasingSeq (Integer -> Ratio Natural)

其中每个比率表示它比之前的数字增加了多少（从 0 开始）。

那么你可以提供一个单一的功能

applyToIncreasing :: ([Ratio Natural] -> r) -> IncreasingSeq -> r
applyToIncreasing f (IncreasingSeq s) = f . drop 1 $ scanl (+) 0 (map (s $) [0..])

这应该允许您以任何方式解构它，而不允许函数检查真实结构。

您只需要一种构造它的方法：可能是 fromList 只是对其进行排序，而 insert 是执行标准有序插入。

这么说让我很痛苦，但我认为使用花哨的类型技巧你不会从中获得任何好处：只有三个函数可能出错，而且它们相当简单正确实施。实现是隐藏的，因此由于这些函数是正确的，所以使用它们的任何东西都是正确的。只是不要导出 IncreasingSeq.

的数据构造函数

我还建议考虑将 [Ratio Natural] 作为基础表示。它简化了事情并保证序列中没有"gaps"（所以它保证是一个序列）。

如果您想要更高的安全性并且可以承受性能损失，您可以使用 data Nat = Z | S Nat 而不是 Natural。

我会说，如果这是 Coq 或类似的语言，而不是 Haskell，我更有可能建议做一些更高级的类型级别的东西（取决于你想要完成的事情）出于几个原因：

在像 Coq 这样的系统中，您通常是在证明关于代码的定理。因此，拥有某个属性成立的类型级证明可能很有用。由于 Haskell 并没有真正内置的方法来证明这些类型的定理，因此实用性降低了。
另一方面，我们可以（有时）构造本质上必须具有我们的属性的数据类型想要使用少量可信函数和隐藏实现。在具有更多定理证明能力的系统的上下文中，例如 Coq，这可能比我们使用依赖类型（可能，至少）更难说服属性的定理证明者。然而，在 Haskell 中，我们一开始就没有这个问题。

haskell 中的单调序列类型

Monotonic sequence type in haskell

haskell

dependent-type