Haskell/Idris 中的开放类型级别证明

Question

在 Idris/Haskell 中，可以通过注释类型和使用 GADT 构造函数来证明数据的属性，例如使用 Vect，但是，这需要将属性硬编码到类型中（例如，Vect 必须是与列表）。 是否可以拥有具有一组开放属性的类型（例如同时包含长度和运行平均值的列表），例如通过重载构造函数或使用 Effect 中的某些东西？

Answer 1

我相信 McBride 在他的 ornament paper (pdf) 中已经回答了这个问题（对于类型理论）。您正在寻找的概念是代数装饰之一（强调我的）：

代数 φ 描述了一种解释数据的结构方法，给出 上升到折叠 φ 操作，递归地应用该方法。 不出所料，调用 φ 的结果树具有相同的 结构作为原始数据——毕竟这就是重点。但 如果这首先是重点呢？假设我们想修复 预先折叠 φ 的结果，仅代表那些数据 提供我们想要的答案。我们应该需要数据来适应 提供该答案的 φ 调用树。 我们可以限制我们的数据吗 到底是什么？当然可以，如果我们按答案索引的话。

现在，让我们编写一些代码。我把整个东西都放了in a gist，因为我要在这里交错cmets。另外，我正在使用 Agda，但它应该很容易翻译成 Idris。

module reornament where

我们首先定义什么是代数，传递Bs 作用于As 的列表。我们需要一个基本情况（B 类型的值）以及将列表头部与归纳假设结合起来的方法。

ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)

根据这个定义，我们可以定义一种由Bs 索引的As 列表，其值恰好是对应于给定ListAlg A B 的计算结果。在nil 的情况下，结果是代数提供给我们的基本情况 (proj₁ alg)，而在cons 的情况下，我们只需使用第二个投影将归纳假设与新的头相结合：

data ListSpec (A : Set) {B : Set} (alg : ListAlg A B) : (b : B) → Set where
  nil  :  ListSpec A alg (proj₁ alg)
  cons : (a : A) {b : B} (as : ListSpec A alg b) → ListSpec A alg (proj₂ alg a b)

好的，让我们导入一些库，现在看几个示例：

open import Data.Product
open import Data.Nat
open import Data.List

计算列表长度的代数由0 作为基本情况给出，const suc 作为组合A 和尾部长度来构建当前列表长度的方式。因此：

AlgLength : {A : Set} → ListAlg A ℕ
AlgLength = 0 , (λ _ → suc)

如果元素是自然数，那么它们可以相加。对应的代数将0 作为基本情况，_+_ 作为将ℕ 与尾部包含的元素之和组合在一起的方式。因此：

AlgSum : ListAlg ℕ ℕ
AlgSum = 0 , _+_

疯狂的想法：如果我们有两个代数处理相同的元素，我们可以组合它们！这样我们将跟踪 2 个不变量而不是一个！

Alg× : {A B C : Set} (algB : ListAlg A B) (algC : ListAlg A C) →
       ListAlg A (B × C)
Alg× (b , sucB) (c , sucC) = (b , c) , (λ a → λ { (b , c) → sucB a b , sucC a c })

现在是例子：

如果我们跟踪长度，那么我们可以定义向量：

Vec : (A : Set) (n : ℕ) → Set
Vec A n = ListSpec A AlgLength n

并且有，例如，这个长度为 4 的向量：

allFin4 : Vec ℕ 4
allFin4 = cons 0 (cons 1 (cons 2 (cons 3 nil)))

如果我们要跟踪元素的总和，那么我们可以定义一个分布的概念：统计分布是总和为 100 的概率列表：

Distribution : Set
Distribution = ListSpec ℕ AlgSum 100

例如，我们可以定义一个统一的：

uniform : Distribution
uniform = cons 25 (cons 25 (cons 25 (cons 25 nil)))

最后，通过结合长度和和代数，我们可以实现大小分布的概念。

SizedDistribution : ℕ → Set
SizedDistribution n = ListSpec ℕ (Alg× AlgLength AlgSum) (n , 100)

并为 4 个元素集提供这种良好的均匀分布：

uniform4 : SizedDistribution 4
uniform4 = cons 25 (cons 25 (cons 25 (cons 25 nil)))