R
> вывод полиморфных типов не нужен
лол
лол
где он нужен?
Size: a a a
2020 May 23
AA
Смотрю кто-то опять ретвитнул какой-то комент дегуза, хотел посмотреть чо за индус снова - а это клапауций
очень люблю разговоры про то что НА САМОМ ДЕЛЕ язык это ГУГОЛПЛЕКС языков
AA
где он нужен?
везде
R
везде
ну например?
VZ
id x = x
AA
ну например?
ну например я сделал
quux = foo bar baz и теперь хочу узнать какого он типаR
id x = x
и зачем тип этого выводить?
к
вывод типа компизации линз и призм
R
ну например я сделал
quux = foo bar baz и теперь хочу узнать какого он типаспрашиваешь агду, она тебе выводит мономорфный тип с метапеременными там, где подразумевается полиморфизм
AA
и зачем тип этого выводить?
чтоб знать как его проаннотировать, например
AA
и зачем тип этого выводить?
или чтоб в репле написать можно было
VZ
спрашиваешь агду, она тебе выводит мономорфный тип с метапеременными там, где подразумевается полиморфизм
Если она метапеременные показывает, то что мешает еще один шаг сделать и обобщить их в forall?
VZ
Если у тебя есть
[tau], замени на forall t. [t]R
Если она метапеременные показывает, то что мешает еще один шаг сделать и обобщить их в forall?
разумное нежелание авторов это делать
AA
ну я так и сказал, что академики просто потеряли интерес к выводу типов и не делают его потому что могут не делать
VZ
разумное нежелание авторов это делать
Этот ответ ноль информации содержит. “Что мешает” = “откуда у авторов нежелание”, т.е. что плохо будет, если сделать.
R
они могут его делать, че там делать-то, вон Влад написал простую стратегию
AA
они могут его делать, че там делать-то, вон Влад написал простую стратегию
так я не говорю, что они не могут его делать. я говорю что они могут не делать и не делают
Oℕ
В идрисе сделано, но напоминаю, что тайп в агде сложнее, чем в хошкеле
R
Этот ответ ноль информации содержит. “Что мешает” = “откуда у авторов нежелание”, т.е. что плохо будет, если сделать.
ну не ноль. Он показывает, что нет каких-то технических ограничений. Просто с зависимыми типами (да и не с зависимыми, как по мне) удобнее не выводить полиморфные типы