Зависимые типы, жидкие типы. Что лучше?

Ничего не понимаю, но читаю с удовольствием, продолжай.

Скорее, я имел в виду, что хаскель совсем не имеет инструментов упрощения разработки с побочными эффектами

Хаскель по-дефолту не поощряет писать в стиле с побочными эффектами. А какие инструменты ты имеешь ввиду, как они должны выглядеть?

Он отгораживает побочки, но что делать, если всё приложение слеплено из побочек? Это весь UI, это БД

У тебя, у тебя эффекты только когда в базу пишешь, а преобразования могут быть чистыми. gui может инкапсулировать (почти) всю императивщину в frp.

с интерактивностью хаскель уже не справляется

Вопрос же на каком уровне это происходит, что там под капотом никого не интересует.

И речь тут не только про корректность типов, но и банальную корректность арифметики, чтобы у меня внезапно не возникло деление на ноль или противоположный знак.

Как язык должен тебя ограждать от того, что ты поставил плюс вместо минуса? Деление на ноль невозможно, если доказано что твой делитель не может быть нулем, а доказать это возможно либо проверяй перед делением.

Не в последнюю очередь поэтому энтерпрайза на хаскеле с плавающей точкой нет или почти нет.

А при чем тут хаскель?

Хаскель по-дефолту не поощряет писать в стиле с побочными эффектами. А какие инструменты ты имеешь ввиду, как они должны выглядеть?

Адвокаты хаскеля утверждают, что ад плана «STM STRef IO a» и отсутствие возможности сделать банальный print в функции — это какое-то там удобство для упрощения контроля побочек. Однако же, если этих побочек много, то цепочки из монадических контейнеров начинают взрывать мозг. Даже в банальном Си есть свободное комбинирование функций с побочками — вот тебе и весь «инструмент упрощения». Собственно, диалекты ML являются более близким аналогом хаскеля, со статической типизацией и компиляцией, при этом позволяют свободно комбинировать чистые и грязные функции.

У тебя, у тебя эффекты только когда в базу пишешь, а преобразования могут быть чистыми. gui может инкапсулировать (почти) всю императивщину в frp

У тебя прям позиция хаскелиста. К сожалению, если у БД более одного пользователя, то может оказаться, что писание в базу растянуто по времени, и во время этой записи могут происходить параллельные записи. Даже если допустить, что запись одна, как в SQLite — параллельных чтений может быть несколько.

gui может инкапсулировать (почти) всю императивщину в frp

На эту тему я люблю говорить, что хаскель — это дергалка для сишных функций. Потому что именно они будут выполнять большую часть работы, а хаскелевая часть останется в качестве декларативного конфига, аки CSS. Ведь даже это самое FRP нужно чем-то выполнять, и это «что-то» будет иметь императивный стиль с большим числом побочек. Не говоря уже о том, что на чистом FRP не получится писать более-менее сложные интерфейсы.

Как язык должен тебя ограждать от того, что ты поставил плюс вместо минуса? Деление на ноль невозможно, если доказано что твой делитель не может быть нулем, а доказать это возможно либо проверяй перед делением.

Возможно только если эту проверку сделать во время выполнения. Но во время компиляции ты не можешь заранее предугадать, когда у тебя числа внезапно сложатся так, что дадут ноль.

Плюс вместо минуса может возникнуть, например, если ты поделишь число на че-то квадрат, забыв учесть, что квадрат минус съедает, а у делимого этот минус остается — и вот у тебя уже минус протёк туда, где ты его не ожидал. Более тонкая проблема возникла, например, на Ariane 5, где число просто вышло за предполагаемые границы, из-за чего посыпалась зависимая арифметика.

Не в последнюю очередь поэтому энтерпрайза на хаскеле с плавающей точкой нет или почти нет.

А при чем тут хаскель?

Потому что для криптографии и криптовалют с их целыми числами хаскель как раз вполне используют.

если у БД более одного пользователя, то может оказаться, что писание в базу растянуто по времени, и во время этой записи могут происходить параллельные записи. Даже если допустить, что запись одна, как в SQLite — параллельных чтений может быть несколько.

Не вижу тут в упор проблем в разрезе чистоты.

На эту тему я люблю говорить, что хаскель — это дергалка для сишных функций. Потому что именно они будут выполнять большую часть работы, а хаскелевая часть останется в качестве декларативного конфига, аки CSS.

Так можно о много чем сказать, и ты например так говоришь и о python, и о clojure. Только смысл данного утверждения от меня ускользает - потому что нас не волнует что находится внутри, ассемблер, vhdl, регистры, вообще до лампочки.

Не говоря уже о том, что на чистом FRP не получится писать более-менее сложные интерфейсы.

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

Но во время компиляции ты не можешь заранее предугадать, когда у тебя числа внезапно сложатся так, что дадут ноль.

В зависимых типах как раз можно это гарантировать, иначе зачем они вообще нужны.

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

Это логическая ошибка, а не ошибка типов. Можно вообще написать что угодно - программа не должна за тебя догадываться, что именно ты хотел.

Более тонкая проблема возникла, например, на Ariane 5, где число просто вышло за предполагаемые границы, из-за чего посыпалась зависимая арифметика.

Это просто неверное предположение о входных данных, т.е. опять же логическая ошибка. Типы от нее не застрахуют.

Потому что для криптографии и криптовалют с их целыми числами хаскель как раз вполне используют.

Какие проблема использования хаскеля для вычислений с плавающей точкой?

Простите за оффтоп, а Вы на каком дистрибутиве остановились? Я просто решил почитать Ваши темы, byko3y как Ваш оппонент тут неясен:

несколько дней провел изучая его

О чем речь, о дистрибутивах линукса? На серверах использую ubuntu, родственникам ставлю mint и guix, а у меня весь софт привязан к венде.

Спасибо за развёрнутый ответ.
А в чём пишете код на Windows? VS? И, наверное, java dotnet?

python, common lisp и немного clojure. Использую emacs и eclipse (по историческим причинам, скорее всего буду полностью с него спрыгивать на emacs).

На Windows? Вы меня положительно удивили!

Для haskell есть какой-то аналог slime? Хотелось бы отправлять выражения в репл по хоткеям хотя бы, чтобы не весь модуль и прочие полезные штуки.

если у БД более одного пользователя, то может оказаться, что писание в базу растянуто по времени, и во время этой записи могут происходить параллельные записи. Даже если допустить, что запись одна, как в SQLite — параллельных чтений может быть несколько.

Не вижу тут в упор проблем в разрезе чистоты

А я вижу: читатель читает индекс, писатель пришел, удалил некоторое значение из этого индекса, а потом читать охреневает, потому что элемент индекса только что был, а теперь его нет.

На эту тему я люблю говорить, что хаскель — это дергалка для сишных функций. Потому что именно они будут выполнять большую часть работы, а хаскелевая часть останется в качестве декларативного конфига, аки CSS

Так можно о много чем сказать, и ты например так говоришь и о python, и о clojure. Только смысл данного утверждения от меня ускользает - потому что нас не волнует что находится внутри, ассемблер, vhdl, регистры, вообще до лампочки

Исходная работа по реактивному программированию где-то из девяностых как раз и применяла декларации на хаскеле для декларативного программирования анимации. Только дело в том, что это уже пользователськие данные, конфиги, а не программы. Да, ты можешь поспорить, что картинка JPEG — это тоже программа, по которой компьютер рисует картинку, но эта «программа» жутко примитивна и ограничена, и не Тьюринг-полна при условии соблюдения этих ограничений. Тот же React.js изначально был просто шаблонизатором, а перестал быть лишь шаблонизатором, когда в нем появилась императивщина плана setState.

Не говоря уже о том, что на чистом FRP не получится писать более-менее сложные интерфейсы.

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

Это тоже фактор, иначе бы операционные системы писали на питоне. Те же БД пишут с параллельным доступом из соображений производительности — иначе бы все сервера работали на SQLite с единственной глобальной блокировкой чтения и записи. В конце-концов машину Тьюринга можно представить как чистую функцию, которая берет предыдущее состояние и вычисляет следующее чистой функцией — мы просто приходим к абстрактным коням в вакууме. Я же говорю с прагматичной позиции, оцениваю то, что можно реализоваать и что будет хоть как-то полезно, и с прагматичной позиции у FRP очень ограниченные возможности, а чтобы их расширить — нужно уйти от FRP, оно становится третьей ногой.

Но во время компиляции ты не можешь заранее предугадать, когда у тебя числа внезапно сложатся так, что дадут ноль.

В зависимых типах как раз можно это гарантировать, иначе зачем они вообще нужны

Неужели есть такие зависимые типы, которые умеют распознавать радости аппаратных реализаций вещественных чисел, вроде 3.129999999?

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

Это логическая ошибка, а не ошибка типов. Можно вообще написать что угодно - программа не должна за тебя догадываться, что именно ты хотел

Это задачи «результат не должен выходить за определенные диапазон», в число которых входит также «результат не должен быть равен нулю», которую нужно решить для исключения деления на ноль. Может у тебя есть на примете язык, который будет через связанные типы данных гарантировать, что для переменных x и y всегда будет выполняться условие (cos x)²+(sin y)² = 1?

Неужели есть такие зависимые типы, которые умеют распознавать радости аппаратных реализаций вещественных чисел, вроде 3.129999999?

http://flocq.gforge.inria.fr/theos.html

Может у тебя есть на примете язык, который будет через связанные типы данных гарантировать, что для переменных x и y всегда будет выполняться условие (cos x)²+(sin y)² = 1?

Для IEEE-754 это неверное условие.

Для haskell есть какой-то аналог slime?

leksah

http://haskell.github.io/haskell-mode/manual/latest/Completion-support.html#Completion-support

http://flocq.gforge.inria.fr/theos.html

Ы-ы-ы, они превращают вещественные числа в целые с округлениями.

Для IEEE-754 это неверное условие

Каким образом неверное? IEEE-754 запрещает тригонометрию?

Ы-ы-ы, они превращают вещественные числа в целые с округлениями.

Так если вещественные в компьютере так представлены.

Каким образом неверное? IEEE-754 запрещает тригонометрию?

Ага. И местами арифметику. x / y * y == x, где y > 0 тоже не выполняется.

Ы-ы-ы, они превращают вещественные числа в целые с округлениями.

Так если вещественные в компьютере так представлены

Нет, они именно округляют их с потерей точности.

Нет, они именно округляют их с потерей точности.

Чтобы произвольное математическое вещественное вещественное число получить в IEEE-754, его необходимо округлить с потерей точности.

Вот есть у нас функция f, yield-ящая цифры числа пи. Было бы здорово, если бы sin[f] по термам внутри f выводил, что это ноль. И так для любых (ну ок, почти любых) полезных f и sin.

От тогда-то (никогда) и заживём.

Было бы здорово, если бы sin[f] по термам внутри f выводил, что это ноль

В общем случае это вполне выводится. На зависимых типах можно доказать почти любую математическую теорему. Соответственно, доказать что-то типа sin(f) стремится к нулю при увеличении точности разложения вполне можно.

А можно там все-таки отправлять выражения в репл по хоткеям? Дока объемная, если ты пользуешься постоянно по-идее должен быть в курсе. После slime мне сложно даже заставить себя что-то на петончеке писать из-за вот этих вот штук. leksah как я понял это отдельный редактор для прожжоных хаскелюг.

А мы могли бы с тобой какими-то более короткими сообщениями общаться?

«Нужно больше золота!»

Спасибо за удивительный топик!
Как не прийдёшь после тяжелого дня, а тут перепись продолжается.

После slime мне сложно даже заставить себя что-то на петончеке писать из-за вот этих вот штук. leksah как я понял это отдельный редактор для прожжоных хаскелюг.

Simon Peyton Jones used Emacs, really.

https://www.youtube.com/watch?v=iSmkqocn0oQ

Я больше не могу, честно.
После Вашего врыва в тред мне стало слегка не по себе.

Есть дядечка, который пишет интересые книги.
Рекомендую некую абстракцию, чтобы на минимальном уровне причаститься. https://www.youtube.com/watch?v=t1e8gqXLbsU

Надеюсь в дальнейшем с Вами плодотворно общаться в FP.

А можно там все-таки отправлять выражения в репл по хоткеям?

В leksah в фоне ghci работает и выражения отправляются туда в процессе печатания. Там сразу пытаются выполниться и показывают ошибку. Можно также зайти в REPL явно и посмотреть какие значения получаются при вызове написанных функций.

Второй не пробовал, но по документации должен работать похоже.

жидкие типы

Чтобы вас не называли жидким типом, нужно записаться в спортзал …

Владимир

Чтобы вас не называли жидким типом, нужно записаться в спортзал …

Тогда будут называть жудким типом.

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

Владимир

да ты и щас чухан..

Владимир

А в чём пишете код на Windows?

Я пишу в блокноте с парой плагинов. Старая школа, знаете ли …

Владимир

Ему бы ещё переносимый GUI…

https://hackage.haskell.org/package/gi-gtk-declarative уже упомянули?

Нужен переносимый. Вот скомпилировал я программу с gi-gtk. Для этого Haskell выкачал msys с половиной линукса.

Если бинарник переложить в другую папку и положить рядом все библиотеки, которые показал ldd, начинает падать в неожиданные моменты (например по пункту меню «вставить emoji» в textview, отключить пункт меню нельзя) и матерится про отсутствующий dbus. Распространять программу со всей папкой msys2 на 7 гигабайт?