На самом деле для того, чтобы поиграться с зависимыми типами и получить базовое представление о них советую посмотреть на интерактивный онлайн туториал по F*, он достаточно понятный и при этом основные идеи донесет:
https://www.fstar-lang.org/tutorial/
Плюсую.
gsomix
gsomix
Хотя, конечно, непонятно откуда взялся неакадемический хайп вокруг зависимых типов.
gsomix
Откуда?
Doge
Откуда?
Возможно из-за Agda и Idris'а и того, что их грозятся когда-нибудь в хаскель добавить. Это если про ФП сообщество говорить.
gsomix
Ну, ок, наверное все-таки Idris.
gsomix
Как идея языка общего назначения с зависимыми типами.
Doge
К тому же некоторые их элементы (пусть и очень сильно обрезанные) в другие языки иногда просачиваются, типа скаловских и dotty'скиех singleton types и того, что народ творит там же в refined и shapeless.
Klei
F* относительно F# обладает эффектом аналогичным F# относительно C#, когда после "я только попробую" не хочешь прикасаться к C# вообще? Не хочу провести отстаток жизни в мечтах об языке, который никогда не пойдет в прод.
Klei
gsomix
F* про другое.
gsomix
В первую очередь это инструмент для формальной верификации.
Klei
Он умеет все, что умеет F#?
gsomix
F* про другое.
Doge
Он умеет все, что умеет F#?
Нет. Это не надмножество или подмножество F#, это другой (просто ML-подобный) язык
Klei
Интересно.
gsomix
Это неверно.
gsomix
Все, что связывает F* и F# — факт того, что когда-то он был написан на подмножестве F#.
Vasily
Тем не менее, после 15 лет c#, эффект с фшарпом именно такой, как выше @Kleidemos описал
Doge
Тем не менее, после 15 лет c#, эффект с фшарпом именно такой, как выше @Kleidemos описал
Ну если честно, вот тут удивлялись, почему всё приходят люди, которые жалуются на отсутствие фич в F#. Так это по той же причине.
После опыта языков с HKT, тайпклассами и т.п., очень сложно писать на языках без них. Кажется, как будто очень важный инструмент у тебя просто отобрали.
gsomix
Ну, в том плане, что C# и F# по фичам практически не отличаются.
gsomix
Дело только в дизайне языков.
Vasily
Паршиал апплай
Klei
Вообще до всех этих штук народ допирает сам собой даже без знания ФП или какой-либо иной теории. Хотелки подобного рода возникали даже не у самых даровитых одногруппников на 3 курсе. Но то как они называются и т.п., я узнал лишь в последний год.
gsomix
Поэтому сравнение не очень корректное.
Doge
Ну, в том плане, что C# и F# по фичам практически не отличаются.
Ну нет, не согласен, разница всё ещё очень ощутима. Начиная от нормального паттерн-матчинга, АТД, вывода типов и заканчивая полноценным квазицитированием и type provider'ами. (И это я ещё очень-очень много всего пропустил между двумя этими гранями)
gsomix
Ну нет, не согласен, разница всё ещё очень ощутима. Начиная от нормального паттерн-матчинга, АТД, вывода типов и заканчивая полноценным квазицитированием и type provider'ами. (И это я ещё очень-очень много всего пропустил между двумя этими гранями)
- квазицитирование сложно назвать полноценным
- тайппровайдеры сложно писать, поддерживать, использовать в продакшене
gsomix
Все остальное — сахар.
gsomix
Ну, вывод типов приятненький, да.
Doge
- квазицитирование сложно назвать полноценным
- тайппровайдеры сложно писать, поддерживать, использовать в продакшене
Оно сильно полноценее, чем в C#, этого уже хватает.
Vasily
Да будет битва
Vasily
У @gsomix появился достойный оппонент
Doge
- квазицитирование сложно назвать полноценным
- тайппровайдеры сложно писать, поддерживать, использовать в продакшене
А тайппровадеры играют супер важную роль, в целях написания скриптов и исследования досупных источников данных.
gsomix
А тайппровадеры играют супер важную роль, в целях написания скриптов и исследования досупных источников данных.
А, забыл, еще и ломаются с невменяемыми ошибками.
Klei
Ну нет, не согласен, разница всё ещё очень ощутима. Начиная от нормального паттерн-матчинга, АТД, вывода типов и заканчивая полноценным квазицитированием и type provider'ами. (И это я ещё очень-очень много всего пропустил между двумя этими гранями)
А паттерн матчинг у нас точно лучше? Где-то видел, что в C# можно будет по любому пропу любого объекта матчить, а не только по F#-специфичным типам.
gsomix
Минусы что-то перевешивают над плюсами использования при анализе данных, которым на F# занимается очень малый процент фанатов.
gsomix
Klei
Ты про шаблоны?
Doge
Минусы что-то перевешивают над плюсами использования при анализе данных, которым на F# занимается очень малый процент фанатов.
Ну я именно в плане анализа данных и написания небольших скриптов их очень продуктивно использовал. Да, в больших приложениях не использовал, и с CI не пробовал интегрировать.
gsomix
gsomix
Но почему именно HKT или тайпклассы должны попасть в F#?
gsomix
Почему не любые другие фичи, которых нет в F#?
gsomix
🤔
Klei
Какие например?
Vladislav
Почему не любые другие фичи, которых нет в F#?
например куча рефакторингов, пусть я и не знаю каких.
Vladislav
Doge
Но почему именно HKT или тайпклассы должны попасть в F#?
Потому что они отлично работают вместе с ФП стилем. (да и вне его тоже, конечно же)
Я был бы не прочь и чтобы они в С# попали, если честно.
Doge
Причем те же HKT - это вещь с достаточно низкой дополнительной когнитивной нагрузкой на программиста (потому что очень логичная штука), но при этом открывающая кучу возможностей для того же DRY и типобезопасности.
Vasily
Шо есть dry?
Vasily
А, понял
Vasily
Монадки на глобус натягивать
Doge
И без них полезны.
Vasily
Ну я имею в виду общее поведение для типов
gsomix
Какие например?
Макросы, алгебраические эффекты, row polymorphism, refinement types, контракты, модули ML, untagged unions, корутины, session types, linear types, гетерогенный параллелизм, dynamic, reference capabilities, unsafe, structural typing, lifetimes/regions, dependent types, мультиметоды, STM, ленивость, model checking...
gsomix
Как же выбрать из многообразия дизайнов?
¯\_(ツ)_/¯
gsomix
Разговоры про HKT в F# чатах — это очень скучно.
gsomix
Из раза в раз одно и то же, одни и те же аргументы.
gsomix
Больше обсудить нечего?
gsomix
Это не Elm чат, не нужно думать, что здесь никто не понимает, в чем суть и плюсы HKT.
gsomix
И нести "благие вести".
Doge
Больше обсудить нечего?
Потому что больная тема. Большая часть современного ФП сообщества и приемов сложилось именно вокруг этих фич.
Да и не "благая весть", а просто само собой ожидаемые вещи от ФП языка в 2018м году.
gsomix
gsomix
Про это все пишут, но никто не вдумывается.
Doge
F# — это не ФП язык, ну.
Ну а я не говорю, что эти вещи полезны только для ФП языка. Для мультипарадигменного тоже отлично работают. Вон, смотри ту же скалу.
gsomix
gsomix
Вон там сверху еще куча фич, которые хорошо работают.
gsomix
Я уж не говорю о том, что, внезапно, "современное ФП" — это обязательно статически строго типизированное ФП, со сложной системой типов.
Doge
Вон там сверху еще куча фич, которые хорошо работают.
Большая часть из них мейнстримовой рабочей реализации не имеет. (Кроме разве что совсем очевидных вещей)
gsomix
Большая часть из них мейнстримовой рабочей реализации не имеет. (Кроме разве что совсем очевидных вещей)
Да? Больше половины имеет.
gsomix
Сейчас начнется скучный разговор про определения.