AA
Когда уже завтипный хаскель вмержат, чтобы можно было над ним издеваться
гранин говорит, что никогда
Size: a a a
2020 May 23
DF
Почему так?
AG
впрочем у агды есть и другая стдлиб. С ней может получше это все
https://github.com/agda/agda-stdlib эта или ещё более другая?
Oℕ
Dollar Føølish
Почему так?
Давайте да, ради разнообразия обсудим, наконец, почему Александр говорит то, что говорит
R
https://github.com/agda/agda-stdlib эта или ещё более другая?
это самая стандартная и есть еще менее стандартная: https://github.com/UlfNorell/agda-prelude
AG
Dollar Føølish
Почему так?
тайп инференц поломается
R
тайп инференц поломается
они ж их там сбоку эти зависимые типы прилепили? Реквестирую мнение @int_index
Oℕ
Эх в дотте вообще нет кайндинференса, т.е. даже по сравнению с тайпинференсом
VZ
они ж их там сбоку эти зависимые типы прилепили? Реквестирую мнение @int_index
Можно уточнить вопрос?
АГ
Давайте да, ради разнообразия обсудим, наконец, почему Александр говорит то, что говорит
Я ни разу не специалист в завтипах, вообще полный ноль. Но у меня есть большие сомнения в том, что их впилят.
R
Можно уточнить вопрос?
в смысле, поломается тайп инференс от добавления зависимых типов или нет?
АГ
Причина, что их скорее всего не впилят, примерно о том же, о чем Второй Закон Клапауция
VZ
в смысле, поломается тайп инференс от добавления зависимых типов или нет?
Зависимые типы выводиться не будут
VZ
Там цель ставится четко: не сломать, что уже есть.
R
Зависимые типы выводиться не будут
это понятно. Обычные продолжат выводиться?
R
Там цель ставится четко: не сломать, что уже есть.
во
VZ
А пи-типы никто выводить не будет, так же как rank-n не выводятся
АГ
Если завтипы выводиться не будут, разве это не означает, что текущие тайплевелофичи на них выражать никто не будет? В лучшем случае библиотекописатели переведут часть своих кодобаз на завтипы
VZ
Ну примерно это от них и ожидается, чтобы вместо тайпфемили-синглтоно-страданий можно было писать библиотеки с завтипами
АГ
Но вообще, я задаю, конечно, дилетантские вопросы, так как мне совсем неясно ничего по этому направлению