gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-02 06:38:14 25 4
gpt4 key购买 nike

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

最佳答案

我相信 McBride 在他的 ornament paper (pdf) 中回答了这个问题(对于类型理论) 。您正在寻找的概念是代数装饰的概念(强调我的):

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.

现在,让我们编写一些代码。我已经把整个事情了in a gist因为我要在这里插入评论。另外,我正在使用 Agda,但它应该很容易转换为 Idris。

module reornament where

我们首先定义传递 B 作用于 A 列表的代数意味着什么。我们需要一个基本情况(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 和作为组合 A 的方式的 const suc 给出和尾部的长度来构建当前列表的长度。因此:

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

关于haskell - Haskell/Idris 中的开放类型级别证明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/27219660/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com