在Haskell / Idris中打开类型级别证明 [英] Open Type Level Proofs in Haskell/Idris
问题描述
是否有可能拥有一组开放属性的类型（例如带有长度和平均运行时间的列表），例如通过重载构造函数或使用效果函数中的某些东西？ $ b $我相信麦克布莱德已经在他的装饰纸（pdf）。你正在寻找的概念是一个代数装饰（重点是我的）：
代数φ描述了解释数据的结构方法，给
上升到一个折叠操作，递归地应用该方法。
不出所料，调用φ的结果树与原始数据具有相同的
结构 - 毕竟这就是要点。但
如果那是最重要的，那么该怎么办？假设我们想要预先确定折线φ的
结果，仅表示那些
将提供我们想要的答案的数据。我们应该需要这些数据以适应φ调用的
树，从而提供该答案。 我们可以将数据限制在
吗？当然，我们可以，如果我们索引答案。
现在，我们来编写一些代码。我将整件事放在了要点上，因为我要在这里插入评论。另外，我使用的是Agda，但它应该很容易转换到Idris。
模块重新定位其中
code> 我们首先定义一个代数的含义，即 B s作用于 A s的列表。我们需要一个基本情况（类型为 B 的值）以及将列表头与归纳假设相结合的方法。
ListAlg：（AB：Set）→Set
ListAlg AB = B×（A→B→B）
给定这个定义，我们可以定义一个由<$ $索引的 A 列表c $ c> B s，其值恰好是对应给定 ListAlg AB 的计算结果。在 nil 情况下，结果是由代数提供给我们的基本情况（ proj 1 alg ），而在 cons 的情况下，我们简单地将归纳假设与使用第二个投影的新头结合起来：
data ListSpec（A：Set）{B：Set}（alg：ListAlg AB）：（b：B）→Set where
nil：ListSpec A alg（proj 1 alg）
cons ：（a：A）{b：B}（如：ListSpec A alg b）→ListSpec A alg（proj 2 alg ab）
好吧，现在我们导入一些库并查看一些示例：
打开import Data.Product
打开导入Data.Nat
打开导入Data.List
代数计算列表的长度由 0 作为基本情况给出，
AlgLength：{A：Set}→ListAlg A
AlgLength = 0，（λ_→suc ）
如果元素是自然数，那么它们可以相加。与之相对应的代数具有 0 作为基本情况并且 _ + _ 作为结合ℕ以及尾部元素的总和。因此：
AlgSum：ListAlgℕℕ
AlgSum = 0，_ + _
Alg×：{ABC：Set}（algB：ListAlg AB） （algC：ListAlg AC）→
ListAlg A（B×C）
Alg×（b，sucB）（c，sucC）=（b，c），（λa→λ{ c）→sucB ab，sucC ac}）
一个现在的例子：
如果我们正在追踪长度，那么我们可以定义Vectors：
Vec：（A ：Set）（n：ℕ）→Set
Vec A n = ListSpec A AlgLength n
有，例如，这个长度为4的矢量：
allFin4：Vecℕ4
allFin4 = cons 0（如果我们正在跟踪元素的总和，那么我们可以使用这些元素的总和来衡量一个元素的总和，那么我们可以定义一个分布的概念：一个统计分布是一个概率列表，其总和为100：
分布：集合
Distribution = ListSpecℕAlgSum 100
A我们可以定义一个统一的例子：
uniform：分配
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）））
In Idris/Haskell, one can prove properties of data by annotating the types and using GADT constructors, such as with Vect, however, this requires hardcoding the property into the type (e.g. a Vect has to be a separate type from a List).
Is it possible to have types with an open set of properties (such as list carrying both a length and running average), for example by overloading constructors or using something in the vein of Effect?
解决方案 I believe that McBride has answered that question (for Type Theory) in his ornament paper (pdf). The concept you are looking for is the one of an algebraic ornament (emphasis mine):
An algebra φ describes a structural method to interpret data, giving
rise to a fold φ oper- ation, applying the method recursively.
Unsurprisingly, the resulting tree of calls to φ has the same
structure as the original data — that is the point, after all. But
what if that were, before all, the point? Suppose we wanted to fix the
result of fold φ in advance, representing only those data which would
deliver the answer we wanted. We should need the data to fit with a
tree of φ calls which delivers that answer. Can we restrict our data
to exactly that? Of course we can, if we index by the answer.
Now, let's write some code. I've put the whole thing in a gist because I'm going to interleave comments in here. Also, I'm using Agda but it should be easy to tranlate to Idris.
module reornament where
We start by defining what it means to be an algebra delivering Bs acting on a list of As. We need a base case (a value of type B) as well as way to combine the head of the list with the induction hypothesis.
ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)
Given this definition, we can define a type of lists of As indexed by Bs whose value is precisely the result of the computation corresponding to a given ListAlg A B. In the nil case, the result is the base case provided to us by the algebra (proj₁ alg) whilst in the cons case, we simply combine the induction hypothesis with the new head using the second projection:
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)
Ok, let's import some libraries and see a couple of examples now:
open import Data.Product
open import Data.Nat
open import Data.List
The algebra computing the length of a list is given by 0 as the base case and const suc as the way to combine an A and the length of the tail to build the length of the current list. Hence:
AlgLength : {A : Set} → ListAlg A ℕ
AlgLength = 0 , (λ _ → suc)
If the elements are natural numbers then they can be summed. The algebra corresponding to that has 0 as the base case and _+_ as the way to combine an ℕ together with the sum of the elements contained in the tail. Hence:
AlgSum : ListAlg ℕ ℕ
AlgSum = 0 , _+_
Crazy thought: If we have two algebras working on the same elements, we can combine them! This way we'll track 2 invariants rather than one!
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 })
An now the examples:
If we are tracking the length, then we can define Vectors:
Vec : (A : Set) (n : ℕ) → Set
Vec A n = ListSpec A AlgLength n
And have, e.g., this vector of length 4:
allFin4 : Vec ℕ 4
allFin4 = cons 0 (cons 1 (cons 2 (cons 3 nil)))
If we are tracking the sum of the elements, then we can define a notion of distribution: a statistical distribution is a list of probabilities whose sum is 100:
Distribution : Set
Distribution = ListSpec ℕ AlgSum 100
And we can define a uniform one for instance:
uniform : Distribution
uniform = cons 25 (cons 25 (cons 25 (cons 25 nil)))
Finally, by combining the length and sum algebras, we can implement the notion of sized distribution.
SizedDistribution : ℕ → Set
SizedDistribution n = ListSpec ℕ (Alg× AlgLength AlgSum) (n , 100)
And give this nice uniform distribution for a 4 elements set:
uniform4 : SizedDistribution 4
uniform4 = cons 25 (cons 25 (cons 25 (cons 25 nil)))
这篇关于在Haskell / Idris中打开类型级别证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
