> Конечно нет, функции между рекурсивными типами неразрешимы. Что ещё значит "неразрешимы"? Кто мешает из какого-нибудь рекурсивного дерева построить аналогичное, путём инкремента всех узлов, например? Да и приведённые тобой id с ревёрсом для листов.
Ну и да, f t = t и есть "время от времени", это и без джинна ясно. Что не так ?
Тип называется разрешимым, если него типа существует ровно одна функции, удовлетворяющая ему. Тип 'forall a. a → a' разрешимый, например. И джинн в /0 разрешает именно его, а не тип 'Time → Time'
10 comments
recommend
bookmark
subscribe
Бггг
иногда, мудак
Вообще ошибка очевидна — время это конкретный тип, а не полиморфный
id подходит всё равно
Конечно нет, функции между рекурсивными типами неразрешимы. Посмотри на ":: [a] → [a]", например. Это может быть как id, так и reverse, например
> Конечно нет, функции между рекурсивными типами неразрешимы.
Что ещё значит "неразрешимы"? Кто мешает из какого-нибудь рекурсивного дерева построить аналогичное, путём инкремента всех узлов, например?
Да и приведённые тобой id с ревёрсом для листов.
Ну и да, f t = t и есть "время от времени", это и без джинна ясно. Что не так
?
Тип называется разрешимым, если него типа существует ровно одна функции, удовлетворяющая ему. Тип 'forall a. a → a' разрешимый, например. И джинн в /0 разрешает именно его, а не тип 'Time → Time'
Ещё раз. Где начинается неподходимость id или f t = t + ГОД или ещё чего
?
Хм, в том-то и проблема, что они подходят. Джинн — автопрувер, он не приемлим, когда у тебя есть больше одного решения
Наконец-то.