ну, я не понял просто, тут нет у списка последнего элемента

О, прикольно
На степике писали про это, но не сказали, почему так

Такие бесконечные списки можно и с императипочкой сделать😂

ну да, только отсутствие иммутабельности сломает структуру

тут мы точно знаем, что элементы не поменяются, поэтому можно завязывать узел, а без иммутабельности мы получим повторение мутации во всех повторах

Я просто шизоид плюсовой, думаю указателями

сделать гет-онли элементы на изи же можно)

ну тогда мы получим просто опять иммутабельность

я же не говорил что это на хаскеле так можно, я сказал что с иммутабельностью так можно

Я кстати ещё по расту начал почитывать материалы, там красиво реализовано всё с безопасностью от мутабельности)

кстати кроме иммутабельности есть более слабые версии персистентности...

да где тут TCO

тут же ленивая структура генерируется, зачем тут TCO, с ним будет только хуже

точнее даже так, с TCO в этой функции не получится даже первый элемент прочитать, нужно будет дождаться, пока бесконечное применение сожрет всю память

Гит-система в пример, ага

Кстати, я вроде видел, что в идрисе надо доказать, что рекурсия в любом случае имеет конечное количество итераций. Означает ли это, что в нём невозможно реализовать матемтические последовательности, для которых не доказана их конечность для любого стартового n?
взять хотя бы стандартную штуку, в  которой если n - чётное, то n/2, если нечётное, то n*3+1, если 1, то выйти из последовательности

1. в простых случаях доказывать не нужно, тотальность следует из структурной рекурсии (когда мы рекурсируемся на части значения из аргумента, то есть аргумент всегда убывает)
2. в более сложных случаях да, нужно доказывать
3. функция не обязательно должна быть тотальной, это свойство которое идрис может проверять, но можно и явно указать, что функия нетотальная
4. данные могут быть тоже лениво-бесконечные, кодата

Второй вариант избыточен или всё же улучшает перформанс функции?

Так, если что, вопрос снимается, реверс белого человка реализуется на фолдах, а фолды это аккум, т.е. мой второй вариант

а был какой-то трюк чтобы $ в паттернах использовать?

или нет?

улучшает. бенчмаркайте