在Haskell/Idris中打开类型级别证明

Question

在Idris/Haskell中,可以通过注释类型和使用GADT构造函数来证明数据的属性,例如使用Vect,但是,这需要将属性硬编码到类型中(例如,Vect必须是与List不同的类型).是否可以使用具有开放属性集的类型(例如包含长度和运行平均值的列表),例如通过重载构造函数或使用效果的静脉？

Answer 1

我相信麦克布赖德在他的装饰纸(pdf)中回答了这个问题(对于类型理论).你正在寻找的概念是一个代数装饰(强调我的):

代数φ描述了一种解释数据的结构方法,产生了折叠φ运算,递归地应用了该方法.不出所料,φ的调用树结构与原始数据具有相同的结构 - 毕竟这就是重点.但是,如果那是最重要的话呢？假设我们想要提前确定折叠φ的结果,只表示那些可以提供我们想要的答案的数据.我们应该需要数据来适应φ调用的树,这些树提供了答案.我们可以将数据限制在那吗？当然,如果我们通过答案索引,我们可以.

现在,让我们写一些代码.我把整个事情放在一个要点,因为我将在这里插入评论.另外,我正在使用Agda,但它应该很容易转换为Idris.

module reornament where

我们首先定义B代表s代表的代数是什么意思A.我们需要一个基本案例(类型的值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 A和尾部长度以构建当前列表长度的方式给出.因此:

AlgLength : {A : Set} ? ListAlg A ?
AlgLength = 0 , (? _ ? suc)

如果元素是自然数,那么它们可以相加.与之对应的代数具有0基本情况和将尾部中包含的元素的总和_+_组合?在一起的方式.因此:

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

疯狂的想法:如果我们有两个代数在相同的元素上工作,我们可以将它们组合起来!这样我们将跟踪2个不变量而不是1个!

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 })

现在的例子:

如果我们跟踪长度,那么我们可以定义Vectors:

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)))