f 1 = 1 f n | even n = f(n / 2) | otherwise = f (3*n+1) полностью определена?

Останов не гарантируется, все значения аргумента будут обработаны

Останов не гарантируется, все значения аргумента будут обработаны

что значит "обработаны" и зачем это вообще?

что было

чтобы length тотальной сделать?

Будто нерешённая проблема останова мешает определить множество частичных функций по завершаемости вычисления. Ну не будет задача определения тотальности разрешимой алгоритмом, и чо из этого?

конечно мешает, посмотри на coq или агду и насколько много функций тотальность которых они не могут доказать

Будто нерешённая проблема останова мешает определить множество частичных функций по завершаемости вычисления. Ну не будет задача определения тотальности разрешимой алгоритмом, и чо из этого?

не распарсил текст %) но про останов писали уже, это необходимое условие для тотальности

Определить множество ничего не мешает. Оно будет невычислимым, ну и ладно

доказательства уровня "чем-нибудь клянусь" это не круто

repeat - частичная?

никогда не остановится

ну она возвращает WHNF сразу и на всех входах

вообще с кодатой все всегда весело

не распарсил текст %) но про останов писали уже, это необходимое условие для тотальности

да, но вычисление останавливаемости мешает вычислять тотальность

особенно никогда она одновременно и кодата и дата

да, но вычисление останавливаемости мешает вычислять тотальность

это уже что-то про (автоматическое?) доказательство вопрос все же был что есть тотальная и частичная

в общем, length на WHNF (1 : ones) не даёт результат в WHNF. @astynax неправ

это уже что-то про (автоматическое?) доказательство вопрос все же был что есть тотальная и частичная

и надо все же разделять классическую мат функцию и то что в яп (какой-нить более специфичной математики), потому что в первом случае нет понятия о длительности вычисления, результат либо существует, либо нет

можно сказать, что length — «функция с полным определением» (кстати, это называется total в Liquid Haskell)

и надо все же разделять классическую мат функцию и то что в яп (какой-нить более специфичной математики), потому что в первом случае нет понятия о длительности вычисления, результат либо существует, либо нет

тезис Чёрча—Тьюринга говорит, что не надо разделять

totalLength c !p [] = Right (p+c) totalLength c p (_:xs) | p < chunkSize = totalLength c (p+1) xs | otherwise = Left $ \() -> totalLength (c+p) 0 xs

(писал с тапка)

тезис Чёрча—Тьюринга говорит, что не надо разделять

можно носом?

удобно бы было работать?

можно носом?

а оно так и зовется, сорри, нашел

length определена на всех значениях аргумента

Ты под значениями только конструкторы понимаешь? Такое. Всё-таки значения -- это набор термов, удовлетворяющих данному типу

оке, был неправ - в первый раз что ли :)

можно сказать, что length — «функция с полным определением» (кстати, это называется total в Liquid Haskell)

вот я как-то так и думал

Вопрос: а обилие частично определённых функций в стандартной библиотеке хаскеля это баг или фича?

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

тезис Чёрча—Тьюринга говорит, что не надо разделять

этот тезис как раз подразумевает существование понятия вычислимость (если верить вики), чего нет в определении функции математической

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

так, а если теперь забыть о length и прочих свёртках бесконечных списков?

так, а если теперь забыть о length и прочих свёртках бесконечных списков?

Я за то, что всё ещё фича

Но лучше конкретные функции обсуждать, чем судить в целом

Какие-то полезны своей частичностью, какие-то нет

Нельзя сказать, что частичность это фича. Частичность это неизбежность, если внутри языка нет пруф-асистент подмножества, явно разделяющего тотальное и нетотальное

Нельзя сказать, что частичность это фича. Частичность это неизбежность, если внутри языка нет пруф-асистент подмножества, явно разделяющего тотальное и нетотальное

Явно разделяющего точно тотальное и возможно нетотальное

Ну в общем моя претензия в блахе изначально была к тому, что такие функции как head, (!!), read, tail, etc выбрасывают ексепшн, вместо того, чтобы возвращать Maybe/Either

Так-то ты прав конечно, про неизбежность

Я тут именно про дизайн библиотеки

Ну в общем моя претензия в блахе изначально была к тому, что такие функции как head, (!!), read, tail, etc выбрасывают ексепшн, вместо того, чтобы возвращать Maybe/Either

uncons и readMaybe есть, а если ты уверен, что они не понадобятся -- для тех случаев и head с read

Явно разделяющего точно тотальное и возможно нетотальное

Не очень корректно написал. Конечно возможно нетотальное

Ну в общем моя претензия в блахе изначально была к тому, что такие функции как head, (!!), read, tail, etc выбрасывают ексепшн, вместо того, чтобы возвращать Maybe/Either

этим всем можно не пользоваться :)

Библиотеки типа safe и сторонние прелюдии - вот это всё

в Хаскелле всегда можно говорить про тотальность только с оговорками, иначе у нас тотальными только id, const и подобные будут, из-за боттомов в каждом типе

Отличная функция id

Практически у всех этих функций есть стандартные safe аналоги, либо их можно одним case'ом заменить

этим всем можно не пользоваться :)

Да оно понятно, что стандартной библиотекой с самыми что ни на есть стандартными функциями можно не пользоваться, а взять вместо этого что-то стороннее. Но меня беспокоит то, что оно unsafe by default

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

в Хаскелле всегда можно говорить про тотальность только с оговорками, иначе у нас тотальными только id, const и подобные будут, из-за боттомов в каждом типе

id от нетотального аргумента будет нетотальна :)

Да оно понятно, что стандартной библиотекой с самыми что ни на есть стандартными функциями можно не пользоваться, а взять вместо этого что-то стороннее. Но меня беспокоит то, что оно unsafe by default

Ну, экспешоны это типичная практика в сабже, без них никуда же

Название safe вводит в заблуждение, как будто с помощью этих headMaybe можно писать безопасные программы, пф

length тотальная, если забыть про боттомы и бесконечные списки

Да оно понятно, что стандартной библиотекой с самыми что ни на есть стандартными функциями можно не пользоваться, а взять вместо этого что-то стороннее. Но меня беспокоит то, что оно unsafe by default

Исторически сложилось

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

Strict fields же есть

Исторически сложилось

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

Название safe вводит в заблуждение, как будто с помощью этих headMaybe можно писать безопасные программы, пф

те части, которые построены сугубо из содержимого safe, вполне себе безопасны - насколько это возможно :)

А то я вообще как-бы из раста, а там паники ловить нельзя, поэтому всё стараются делать сейф. После этого Haskell немного конфьюзит

те части, которые построены сугубо из содержимого safe, вполне себе безопасны - насколько это возможно :)

Ну они безопасны только пока ими правильно пользуются

для бесконечных списков имеет смысл говорить о продуктивности. length не продуктивна, из-за того, что возвращаемый тип Int не коиндуктивен, можно написать продуктивный length', возвращающуй Nat, например

Ну они безопасны только пока ими правильно пользуются

Не делают fromJust и так далее

Так в хаскеле тоже в основном стараются всё делать safe :)

Хотя ладно, fromJust то не сейф тоже

Не делают fromJust и так далее

ну в русте вон тоже unwrap есть, но ничего, живём как-то

А матчить руками (\(Just x) -> ..) мы не будем ок

Тогда норм

Code review для такого есть :)

ERROR: S client not available

А матчить руками (\(Just x) -> ..) мы не будем ок

можно компилятор попросить громко ругаться на non exhaustive patterns

можно компилятор попросить громко ругаться на non exhaustive patterns

Ну попроси :) Он же лямбды не смотрит, по-моему

так и делаем - -Werror на CI

Это вам не идрис

Смотрит вроде

id от нетотального аргумента будет нетотальна :)

ну, id undefined не взорвется же, но если хочется убить боттом, давайте оставим только const

Ага, только боттомы друг другу не равны. id $ head [] взорвётся

можно компилятор попросить громко ругаться на non exhaustive patterns

Компилятор не всегда может проверить, рассмотрены ли все случаи в гардах

Если хочется убить боттом, то нужно пруф-асистентент в язык встраивать #ленивый_идрис

Ага, только боттомы друг другу не равны. id $ head [] взорвётся

только если в него смотреть

так же как и id undefined

Компилятор не всегда может проверить, рассмотрены ли все случаи в гардах

можно попросить ругаться на все гарды без otherwise или что-то типа того

иногда удобно писать гарды без otherwise

можно попросить ругаться на все гарды без otherwise или что-то типа того

f x | x > 0 = "foo" f 0 = "bar" f _ = "qux"

хотя в таком случае обычно есть catchall clause

проверка на pattern match exhaustiveness - штука сложная

view patterns всякие оную ломают

f x | x > 0 = "foo" f 0 = "bar" f _ = "qux"

ну как по мне лучше где-то явно написать аналог рустовского unreachable!(), чем писать сложные матчи, которые компилятор не может определить как exhaustive

идрис вот отловит такое, да

ну и наверное всякие расширения хаскеля

ну как по мне лучше где-то явно написать аналог рустовского unreachable!(), чем писать сложные матчи, которые компилятор не может определить как exhaustive

ещё не хватало из руста что-то в хаскель тащить ?

А подскажите, есть ли готовые библиотеки для расширяемых массивов, типа std::deck из C++ (состоит из списка массивов). Так, чтобы можно было с одного из концов добавлять, но не переаллоцировать каждый раз, ну и чтобы оверхеда, как в стандартных одноэлементных списках, не было?

И самому можно написать, но зачем, если готовое есть

ещё не хватало из руста что-то в хаскель тащить ?

Кек. unreachable = error "Unreachable"

А подскажите, есть ли готовые библиотеки для расширяемых массивов, типа std::deck из C++ (состоит из списка массивов). Так, чтобы можно было с одного из концов добавлять, но не переаллоцировать каждый раз, ну и чтобы оверхеда, как в стандартных одноэлементных списках, не было?

Упс, std::deque

А подскажите, есть ли готовые библиотеки для расширяемых массивов, типа std::deck из C++ (состоит из списка массивов). Так, чтобы можно было с одного из концов добавлять, но не переаллоцировать каждый раз, ну и чтобы оверхеда, как в стандартных одноэлементных списках, не было?

Data.Sequence не подходит?

Они на списках

А мне нужно поплотнее элементы располагать

-Wall, увы, далеко не all

Data.Sequence на finger tree

-Wall, увы, далеко не all

какой ключик нужен ещё?