В эту пятницу начинается, если кому еще актуально.

https://icfpcontest2024.github.io/

Вот список имеет вид
data List a = Nil | Cons a (List a)
т.е.
F(x) = 1 + x * F(x)
а значит
F(x) - x * F(x) = 1
(1-x) * F(x) = 1
F(x) = 1 / (1-x)
и действительно, если мы такую функцию разложим в ряд, то получим
F(x) = 1 + x + x*x + x*x*x + x*x*x*x + ...
т.е. как раз тип описывает списки из х разной длины.

Но вот что любопытно,
F(F(F(x))) = 1 / (1 - (1 / (1 - 1 ( Read more... )

On Understanding Data Abstraction, Revisited
http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf

Занятный легко читаемый обзор о том, как сильно отличаются абстрактные типы данных (ML-style) от объектов (OOP-style). При выбранных определениях довольно четкая картина вырисовывается.
Показывает, в каком смысле "the typical object-oriented program ( Read more... )

Наконец-то нормальный язык подвезли. Там в описании прекрасно все:
https://github.com/Storyyeller/IntercalScript

Phantom values порадовали особенно.

По мотивам поста Никиты про разницу в производительности "высокоуровнего/функционального" и "низкоуровнего/императивного" кода. Взял буквально его пример с созданием массива пар чисел. Его оригинал на кложе:

(concat
(mapv
(fn [y] [from-x y])
(range from-y (quot to-y 2)))
(mapv
(fn [y] [to-x y])
(range (quot to-y 2) to-y)))
Как ( Read more... )

( Read more... )

Свежее выступление Майкла Сноймана ( Read more... )

Занятный доклад на свежем FP Conf про equational reasoning и теорем пруверы ( Read more... )

Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово Inf, и поле оказывается "ленивым": когда данные конструируются, ( Read more... )

This paper thoroughly analyzes three state-of-the-art, formally verified implementations of distributed systems: IronFleet (Dafny/C#), Verdi (Coq/OCaml), and Chapar (Coq/OCaml). Through code review and testing, we found a total of 16 bugs, many of which produce serious consequences, including crashing servers, returning incorrect results to clients ( Read more... )