AZ
плюс это дает возможность трансмуты делать если хочется сильно ногу отстрелить
Size: a a a
2020 June 24
G
https://github.com/Pzixel/idris-playground/blob/chapt9_proove_uniqueness/chapter9.2.idr вот тут если что всё)
пздц тяжело лол
AZ
пздц тяжело лол
ну вот я говорю, одно дело - прочесть книжку, и другое - попытаться что-то из неё сделать
AZ
причем я взял задачку оттуда и усложнил ну совсем чуть чуть
G
я не про это
G
все-таки у раста лучше подход с этим
G
когда в самом начале все обобщённые типы перечисляются
G
потому что в голове я все равно составляю список всех type variables у функции
AZ
мб, но тут же трейдофы
AZ
а может и нет
AZ
мне кажется это как объявлять список всех переменных в начале в ANSI C или паскале
G
мне кажется это как объявлять список всех переменных в начале в ANSI C или паскале
может дело привычки, не знаю
DS
ну вот я говорю, одно дело - прочесть книжку, и другое - попытаться что-то из неё сделать
Это норма.
Вон, я доказывал простейшие признаки деления для целых чисел на агде.
Ничего так развлечение для вещей, которые на бумажке доказываются в три строки
Вон, я доказывал простейшие признаки деления для целых чисел на агде.
Ничего так развлечение для вещей, которые на бумажке доказываются в три строки
G
но вот переменные по ходу дела определяются обычно, а дженерики обычно сразу все идут грубо говоря в сигнатуре
AZ
но вот переменные по ходу дела определяются обычно, а дженерики обычно сразу все идут грубо говоря в сигнатуре
ну вот я думаю это дело привычки
AZ
говорю, посмотри на языки 60-70х - там тоже все переменные в начале (обычные)
AZ
с той же логикой "ой, непонятно что используется"
AZ
я думаю лет через 20 подобное отношение к генерика будет тоже анахронизмом
AZ
Что за книга?
Type-driven Development with Idris