Описание тега codata
1
ответ
Краткая сводка по кодатам (где комонада является "типом для входной примеси")
С точки зрения содержательных резюме - это описание Comonads, кажется, выигрывает - описывая их как "тип для входной примеси". Что такое эквивалентное содержательное (одно предложение) описание для кодаты?
11 июл '13 в 22:48
1
ответ
Есть ли идея решить проблему с плавающей точкой точности в будущем?
Мы не можем хранить десятичные числа с бесконечной точностью, но может быть какой-то способ представить их так же, как мы представляем бесконечные списки в haskell. Первая идея пришла мне в голову - представить десятичное число с помощью чего-то пох…
22 фев '17 в 18:28
2
ответа
Терминология на примере кодаты в Clojure
Вообразите следующую функцию, чтобы дать бесконечную ленивую последовательность Фибоначчи в Clojure: (def fib-seq (concat [0 1] ((fn rfib [a b] (lazy-cons (+ a b) (rfib b (+ a b)))) 0 1))) user> (take 20 fib-seq) (0 1 1 2 3 5 8 13 21 34 55 89 144…
12 июл '13 в 11:19
0
ответов
Почему не всегда использовать Inf вместо Lazy в Idris?
Я нахожу это Lazy а также Inf очень близко: Lazy и Inf тесно связаны (на самом деле базовая реализация использует один и тот же тип). Единственное отличие на практике заключается в проверке целостности, где Lazy удаляется (т.е. термины проверяются н…
13 янв '18 в 03:35
1
ответ
В чем разница между кодой и данными?
Здесь есть какое-то объяснение. Интуитивно я понимаю, как конечные структуры данных отличаются от бесконечных структур данных, таких как потоки. Тем не менее, интересно увидеть другие объяснения различий, характеристик, типов кодов. Я наткнулся на т…
03 мар '15 в 20:24
1
ответ
Почему в idris нет функции фильтрации Stream?
Есть filter : (a -> Bool) -> List a -> List a для списка, но нет filter : (a -> Bool) -> Stream a -> Stream a для стрима, почему? Есть ли альтернативы для выполнения подобных работ?
24 апр '17 в 14:38
1
ответ
Agda: упрощение рекурсивных определений с использованием Thunk
Я пытаюсь реализовать тип, который представляет (возможно) бесконечный путь в бесконечном двоичном дереве. Определение в настоящее время напоминает определение Conat в stdlib. open import Size open import Codata.Thunk data BinaryTreePath (i : Size) …
25 мар '19 в 23:36
1
ответ
Что представляют собой codata в контексте программирования?
Это базовый алгоритм, потому что с каждой итерацией он вызывает себя для данных, которые больше, чем были раньше: iterate f x = x : iterate f (f x) Он похож на стиль накопителя хвостовой рекурсии, но его накопитель неявный, а не передается в качеств…
10 май '20 в 22:42
1
ответ
Как закодировать corecursion/codata в строго оцененной настройке?
Corecursion означает обращение к данным на каждой итерации, которые больше или равны тем, что были у вас раньше. Corecursion работает с codata, которые представляют собой рекурсивно определенные значения. К сожалению, рекурсия значений невозможна в …
04 мар '20 в 18:29
1
ответ
CoNat: доказательство того, что 0 нейтрален слева
Я экспериментирую с определением CoNatвзято из этой статьи Джеспера Кокса и Андреаса Абеля: open import Data.Bool open import Relation.Binary.PropositionalEquality record CoNat : Set where coinductive field iszero : Bool pred : .(iszero ≡ false) -&g…
19 сен '19 в 20:14
0
ответов
Должен ли NFData иметь дуал?
В Haskell есть тип, который имеет следующую форму: class NFData a where rnf :: a -> () Типы, которые больше похожи на данные, чем на функциональные, могут быть оснащены экземплярами NFData. Каждый такой экземпляр тщательно анализирует данное знач…
26 окт '21 в 06:02
1
ответ
Является ли единственная разница между Inductive и CoInductive проверками правильности их использования (в Coq)?
Сформулируем вопрос по-другому: если мы удалим проверку завершения и условие защищенности при использовании индуктивных и коиндуктивных типов данных, соответственно, исчезнет ли фундаментальное различие между индуктивным/коиндуктивным и фиксированны…
11 дек '20 в 10:51
0
ответов
Обнаружение самого дешевого способа создания независимых итераторов
Предположим, я пишу функцию, принимающую итерацию, и моя функция хочет быть независимой от того, является ли эта итерация на самом деле итератором или нет. (Это обычная ситуация, верно? Я думаю, что в основном все функции itertools написаны таким об…
12 мар '22 в 13:05