Ответ 1
Я считаю, что Макбрайд ответил на этот вопрос (для теории типов) в своей бумаге для украшения (pdf). Концепция, которую вы ищете, - это алгебраический орнамент (выделение мое):
Алгебра φ описывает структурный метод интерпретации данных, дающий перейдя к операции сгибания φ, применяя метод рекурсивно. Неудивительно, что полученное дерево вызовов на φ имеет одинаковое структура как исходные данные - вот и точка, в конце концов. Но что, если это было, прежде всего, точка? Предположим, мы хотели исправить результат сгиба φ заранее, представляя только те данные, которые доставить ответ, который мы хотели. Нам нужны данные, чтобы они соответствовали дерево вызовов φ, которое доставляет этот ответ. Можем ли мы ограничить наши данные точно это? Конечно, мы можем, если проиндексировать ответ.
Теперь напишите код. Я поставил все в gist, потому что здесь я буду чередовать комментарии. Кроме того, я использую Agda, но это должно быть легко транслировать в Idris.
module reornament where
Начнем с определения того, что значит быть алгеброй, поставляющей B, действующей в списке A s. Нам нужен базовый регистр (значение типа B), а также способ объединения заголовка списка с гипотезой индукции.
ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)
Учитывая это определение, мы можем определить тип списков A, индексированных по B, значение которого является точно результатом вычисления, соответствующего данному 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)))