我相信麦克布莱德（McBride）在他的著作中已经回答了这个问题（对于类型理论）装饰纸 (pdf) https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf。您正在寻找的概念是代数装饰的概念（强调我的）：
代数 φ 描述了解释数据的结构方法，给出
递归地应用该方法，上升为折叠 φ 操作。
毫不奇怪，调用 φ 的结果树具有相同的
结构作为原始数据——毕竟，这就是重点。但
如果这就是重点怎么办？假设我们想要修复
预先折叠 φ 的结果，仅代表那些将
提供我们想要的答案。我们应该需要数据来适应
传递该答案的 φ 调用树。我们可以限制我们的数据吗
到底是那个？当然可以，如果我们按答案建立索引。
现在，让我们编写一些代码。我已经把整个事情要点 https://gist.github.com/gallais/e507832abc6c91ac7cb9因为我要在这里插入评论。另外，我正在使用 Agda，但它应该很容易转换为 Idris。
module reornament where
我们首先定义代数交付意味着什么Bs 执行以下操作：As。我们需要一个基本情况（类型的值B）以及将列表头部与归纳假设相结合的方法。
ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)
给定这个定义，我们可以定义一种列表类型As 索引为Bs，其值正是给定对应的计算结果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)))
