(
Да нет, я просто не хотел грустить, а теперь загрустил
Size: a a a
2021 April 01
(
Ну как видишь, Котлин пока достаëт туда, куда скала не достаёт
(
Мобилки, саенс
(
СПРИНГ нахуй
U
Быстрая сборка!
AK
субъективно, да. многим оно нужно, есть немало любителей работать в данном стиле и оперировать подобными фичами. объективно - думаю нет, если мы будем рассматривать скорость и стоимость разработки, поддерживаемость итд продуктовые показатели. может объективно только на каком-то узком множестве специфических задач, но для языка общего назначения таки нет, имхо
с#
Антон, блин, хкт в языке не мешает тем, кому оно не нужно, пойми!
АХ
Чем они могут повредить-то? Расжижат мозг разработчиков, не готовых к фичам, которые не придуманы ещё дидами?
с#
навредить можно, если сделать котлин академическим языком
с#
поэтому надо уважать разработчиков, не готовых к фичам, которые не придуманы ещё дидами
АХ
Для этого надо начать тащить фичи с которыми непонятно как работать: зависимые типы, линейные типы и прочую маргинальщину
IP
а в программировании зависимые типы по итогу ни для чего не нужны
IP
ну то есть, в когах да арендах им без сигма- и пи-типа нельзя, но только потому что это уже верификация доказательств
IP
тут ты не прав. хкт добавляет несколько килограмм боли в разработку компилятора
IP
ну и замедляет внесение других фич
ch
Хкт это что?
IP
дженерики на максималках
АХ
Нельзя сказать. Использовать зависимые типы _для программирования_ никто толком не пытался. Лучший пример на сегодня — это маргинальный идрис. Их вотчина сейчас — доказыватели теорем
(
Дратути приехали, "без Сигма и Пи типа нельзя", это тащемта почти определение завтипности
IP
так coq, arend и идрисня вот эта - не для программирования. это так, теоремы подоказывать