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

Question

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

haskellproofcategory-theorycorrectnessidris

16

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

- David Harrison

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- gallais · Accepted Answer

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

一个代数 φ 描述了一种解释数据的结构方法，产生了一个递归应用该方法的折叠 φ 操作。毫不奇怪，φ 的调用结果树与原始数据具有相同的结构——毕竟这就是重点。但是如果这首先是重点呢？假设我们想要事先固定 fold φ 的结果，仅表示那些会产生我们想要的答案的数据。我们需要的数据必须与产生该答案的 φ 调用树匹配。如果我们按答案索引，我们当然可以将我们的数据限制为完全符合要求的数据。

现在，让我们写一些代码。我已经把整个内容放在了一个gist中，因为我将在这里插入注释。同时，我正在使用Agda，但应该很容易转换到Idris。

module reornament where

我们首先定义什么是在一组 A 上作用的代数 B。我们需要一个基本情况（类型为 B 的值），以及一种将列表头与归纳假设结合起来的方法。

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

根据这个定义，我们可以定义一种由B索引的A列表类型，其值恰好是与给定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 , _+_

疯狂想法：如果我们有两个代数在相同的元素上运作，我们可以将它们合并！这样我们就可以跟踪两个不变量而不是一个！

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)

并为四个元素集合提供这种漂亮的均匀分布：

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