Так вышло. Мне тоже не нравится

elm-graphics работае в канву. Но свою такую либу не напишешь - там нативные куски

И в elm-graphics всё всегда перерисовывается, ЕЯПП.

Ага, выбираешь себе платформу - думаешь ну всё, жс больше в глаза не увижу. А потом выясняется что платформа в какой-нибудь IntersectionObserver не умеет(

Ни разу не похож. :)

Синтаксически похож :) Концептуально - ниочень :)

Проверка может быть сделана отдельным аргументом - доказательством. Например в Idris у функции (-) для натуральных чисел три аргумента: третий - доказательство, что первый больше или равен второму. Но составлять такие доказательства - сложное исскуство.

ну да, я как понял что компилятор сам может инферить многие доказательства

На Haskell похож синтаксически.

Простейшие может, но чуть сложнее - приходится доказывать руками.

ммм, а как руками составить пруф что число не равно нулю например?

where нет, есть только let; тип аннотируется через :, а ::, это cons; всё как в ML. Вот описание типов похоже на Haskell, это правда

Сигнатуры функций отдельно пишутся, fun и val нет. Солянка. :)

Ну хоть не сишный синтаксис! И на том спасибо :)

ризон))))

Именно! Этот уже испортили

По большому счету пофиг на стиль синтаксиса, был бы чистенький + средства форматирования.

Си-подобный синтаксис убивает ML-подобные языки!

Простейший вариант - функция decEq x y , которая возвращает либо Yes (x = y) с доказательством равенства, или No (Not (x = y)) с доказетельсвом неравенства. Есть встроенные в библиотеку доказательства, типа  (LTZero x) (что все нашуральные числа больше или равны нуля) или (Refl x x) что все равно самому себе. И функции конструирования равенств, типа cong, которая из доказательства x=y получает доказательство f x = f y.

Если кому интересно, и при этом есть знание инглиша и желание пописать доки, можете про PR'ить мне в сюда: https://github.com/astynax/tea-combine - для выкладывания нужны хоть какие-то докстринги. Для функций и типов докстринги есть, нужны только для модулей. Туда накопипастить примеров кода из example projects. Ещё можно поругать код, да :)