在 Idris/Haskell 中,可以通过注释类型并使用 GADT 构造函数(例如 Vect)来证明数据的性质,但这需要将性质硬编码到类型中(例如,Vect 必须是与 List 不同的单独类型)。
是否可能拥有具有开放属性集的类型(例如同时携带长度和运行平均值的列表),例如通过重载构造函数或使用类似 Effect 的东西?
现在,让我们写一些代码。我已经把整个内容放在了一个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)))
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)))
fold
从元素列表计算不变量。这是我得到的链接:https://github.com/gallais/potpourri/blob/2d346c10ece927dc9cfa7fab8e7d7c41f37cac7e/agda/poc/ListSpec.agda - gallais