Список с функционального мира, а вектор с императивного, по-этому и оптимизированы под разные нужды. Это нужно учитывать.
То есть если часто нужно длину списка узнавать, не лучше ли воспользоваться вектором?
Спасибо! Интересный материал, у меня кстати был выбор, что писать: merge или quck sort.
Но если честно мне синтаксис Agda больше нравиться чем Epigram. На самом деле я не сразу на Agda подсел. Была попытка с ATS, и длительное время сидел на Coq. Но Agda все же привлекает больше всего. Плюс заманчивая возможность через Haskell подключить C/C++ — боюсь даже представить, что может выйти.
В этом случае согласен. Наверное зависимые типы и суровая жизнь заставили меня больше верить типу функции чем ее названию.
Действительно без определенных ограничений на функцию сравнения ничего не получится.
Все правильно, но все же мой пример не единственный при котором не нужно доказательство линейного порядка.
То есть, я только хочу сказать, что следующее утверждать нельзя:
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
Вы не абстрагируетесь… Забудьте о том, что это функции сортировки.
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
Это нельзя утверждать — и доказательство этому мой пример с предыдущего комментария.
Вообще то не обязательно. На эти функции нужно смотреть абстрагируясь от названий: задача доказать — а это значить построить терм. Обязательное тут, как я писал — это определения функций sort и sorted, пока этого не будет, ничего точно сказать нельзя. Вот например если так:
В данной ситуации обязательно нужно иметь определения функций sort и sorted, потому как с описанного типа много информации получить нельзя. И после уже можно проступать к доказательству — это весьма реально.
… пишешь \_1 получается ₁, пишешь \<=, получается ≤, пишешь \all или \forall, получается ∀.
Еще классно, что в agda-mode есть подсказки, типа intellisense.
надо с {-# OPTIONS --no-termination-check #-}
Это проблема Agda, она хуже определяет завершаемость (чем Coq) по-этому иногда эту опцию можно использовать.
То есть если часто нужно длину списка узнавать, не лучше ли воспользоваться вектором?
да и все равно — это знания о механизмах и причинах эволюции этого [ОДНОГО] элемента.
Но если честно мне синтаксис Agda больше нравиться чем Epigram. На самом деле я не сразу на Agda подсел. Была попытка с ATS, и длительное время сидел на Coq. Но Agda все же привлекает больше всего. Плюс заманчивая возможность через Haskell подключить C/C++ — боюсь даже представить, что может выйти.
А что если на Венере уже есть жизнь? Все эти бомбардировки бактериями, водой и еще чем-то там могут уничтожить ее!
:-D бомба!!!
*буду цитировать=)
Действительно без определенных ограничений на функцию сравнения ничего не получится.
То есть, я только хочу сказать, что следующее утверждать нельзя:
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
Это нельзя утверждать — и доказательство этому мой пример с предыдущего комментария.
То есть без определений никак.
Еще классно, что в agda-mode есть подсказки, типа intellisense.
Это проблема Agda, она хуже определяет завершаемость (чем Coq) по-этому иногда эту опцию можно использовать.
{-# OPTIONS --no-termination-check #-}
Very-Bad: {A: Set} -> A
Very-Bad = Very-Bad