JS
это что значит?
Size: a a a
2021 July 13
2021 July 15
АП
Кто читал эту книгу? Стоит ли её рекомендовать?
У меня это была первая книга по хаскелю.
У меня это была первая книга по хаскелю.
АП
JS
есть более подходящий чат @haskellru
JS
JS
При самостоятельном изучении программисту с опытом в других языках программирования лучше всего подойдёт Курт
2021 July 17
L
Вот ещё пейпер по теме подвернулся http://ps.informatik.uni-tuebingen.de/publications/ostermann20decompositiondiversity.pdf
Decomposition Diversity with Symmetric Data and Codata
Concretely, this paper makes the following contributions:
• We present the first full symmetric programming language that allows invertible destructorization and constructorization.
• We have fully formalized the language in the Coq theorem prover and mechanically verified that the language is type-sound. We have implemented the transposition algorithms in Coq and have proven that they are total, preserve typing and behavior, and are inverses of each other. All łdifficultž parts of the proofs have been mechanically verified in Coq, with a few rather obvious but very laborious to mechanize ‘plumbing’ proofs left as ordinary paper proofs.1 The Coq proofs, which consumed by far the largest part of the authors’ time investment, constitute more than 60 kloc.
• We synthesize a mechanically verified implementation of the language from our Coq formalization and have integrated it into a browser-based IDE that supports constructorization and destructorization
Decomposition Diversity with Symmetric Data and Codata
Concretely, this paper makes the following contributions:
• We present the first full symmetric programming language that allows invertible destructorization and constructorization.
• We have fully formalized the language in the Coq theorem prover and mechanically verified that the language is type-sound. We have implemented the transposition algorithms in Coq and have proven that they are total, preserve typing and behavior, and are inverses of each other. All łdifficultž parts of the proofs have been mechanically verified in Coq, with a few rather obvious but very laborious to mechanize ‘plumbing’ proofs left as ordinary paper proofs.1 The Coq proofs, which consumed by far the largest part of the authors’ time investment, constitute more than 60 kloc.
• We synthesize a mechanically verified implementation of the language from our Coq formalization and have integrated it into a browser-based IDE that supports constructorization and destructorization
2021 July 18
AG
дефункционализация на марше
ЗП
Дефункцонализация прикольная вещь, элиминирование hof
2021 July 22
JS
2021 August 02
ПК
Ну и что я, спрашивается, написал?
Почему это вообще работает? Почему поворот по 3 оси, а не по первой во внешней функции? Зачем там ⊃⊃?
Почему
+/⊃+/⊃+/{ω⌽[3]⊃⊃¨{ω⌽[2]¨{ω⌽[3]CUBE}¨(¯1 0 1)}¨(¯1 0 1)}¨(¯1 0 1)
ρCUBE = 3 3 3
(Получение суммы по всем соседям элемента трёхмерного массива)Почему это вообще работает? Почему поворот по 3 оси, а не по первой во внешней функции? Зачем там ⊃⊃?
Почему
{ω⌽[1]¨{ω⌽[2]¨{ω⌽[3]CUBE}¨(¯1 0 1)}¨(¯1 0 1)}¨(¯1 0 1) не даёт нужный результат?˸A
Ух ты. Что за язык?
ПК
APL