Ответ на »сообщение 4069« (Денис Зайцев)
___________________________

0/0 == 0 ? Оригинально, как говаривал поручик Ржевский! Это называется довести хорошую идею до абсурда

...

Да, с делением на ноль у меня тоже глаза на лоб полезли.
Катастрофы с такими программами просто неизбежны. Ведь сообщения об ошибке нет.

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

В статье Colin Runciman - "What About the Natural Numbers?" сопоставляется со списками -- вариант арифметики Пеано. Вспомним, как будет выглядеть функция отбрасывания одного (скажем, первого) элемента списка, ну и сам тип списков:

data List a = []
            | a : (List a)

drop :: Int -> List a -> List a

drop    0      xs    =  xs        -- не надо ничего отбрасывать
drop    n      []    =  []        -- неоткуда отбрасывать
drop  (n+1)  (x:xs)  =  drop n xs -- один элемент отбросили, отбрасываем остальные

То есть при попытке отбросить сколько-то элементов из пустого списка получаем снова пучтой список.

Теперь представим себе реализацию натуральных чисел:

data Nat  = 0
          | Nat + 1

Как произвести вычитание? Ну, по аналогии со списками вот так, например:

sub :: Nat -> Nat -> Nat

sub  a    0  = a        -- не надо ничего вычитать
sub  0    b  = 0        -- неоткуда вычитать
sub (a+1) (b+1) = sub a b  -- вычли из a одну единичку, вычитаем оставшиеся в b

Получается, в натуральной арифметике 0-n == 0.

С делением на ноль посложнее... Тут два решения -- либо x/0 == x.
Либо x/0 == infinity, где infinity = infinity + 1. Т.е. получается вполне логично, но увы -- противоречащее Total FP -- недопустимая бесконечно зациклившаяся рекурсия...

Ответ на »сообщение 4067« (Lisp Hobbyist)
___________________________

А что касается ошибок периода выполнения программ, то опять же, если мне не изменяет память, Лука Карделли утверждал, что type-sound program таковых не имеет?

Я пролистал по диагонали его статью "Type Systems", там он как раз об этом рассуждает.

Type soundness: The property stating that programs do not cause forbidden errors.

1 Introduction

The fundamental purpose of a type system is to prevent the occurrence of execution errors during the running of a program. This informal statement motivates the study of type systems, but requires clarification. Its accuracy depends, first of all, on the rather subtle issue of what constitutes an execution error, which we will discuss in detail. Even when that is settled, the absence of execution errors is a nontrivial property. When such a property holds for all of the program runs that can be expressed within a programming language, we say that the language is type sound. It turns out that a fair amount of careful analysis is required to avoid false and embarrassing claims of type soundness for programming languages. As a consequence, the classification, description, and study of type systems has emerged as a formal discipline.

Вот только я не совсем понял, как он предлагает учесть и предотвратить в системе типов такие ошибки? как деление на ноль или попытка взятия первого элемента пустого списка... Единственное, что я там заметил, это запрет на доступ к неправильным ячейкам памяти и перехват исключений?
Предлагается изучать теорию типов (замену бестиповых предикатной логики и теории множеств)...
Вапще у Карделли черезчур много статей, когда бы их изучить ещё... :о(

Ответ на »сообщение 4069« (Денис Зайцев)
___________________________
Да, с делением на ноль у меня тоже глаза на лоб полезли.
Катастрофы с такими программами просто неизбежны. Ведь сообщения об ошибке нет.

0/0 == 0 ? Оригинально, как говаривал поручик Ржевский! Это называется довести хорошую идею до абсурда... Доказательство правильности вычислений, конечно, с таким подходом сильно упростится :)))
А какой простор для оптимизации, например: A = A/1 = (A*0)/(1*0) = 0/0 = 0, поэтому значением любого выражения будет ноль! Прямо дух захватывает :)

Ответ на »сообщение 4066« (Geniepro)
___________________________
Нет и исключений/авостов при выполнении функций. Любая валидная функция возвращает именно то значение, которое прописано в её типе.
В хаскеле этого же эффекта добиваются при помощи типов Maybe и Either.
То есть функция всегда гарантировано возвращает прописанное в описании значение вместо исключения.

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

Ответ на »сообщение 4066« (Geniepro)
___________________________

Если мне не изменяет память, подобные проблемы уже возникали при переходе к типизированному лямбда-исчислению. Для него была справедлива теорема о сильной нормализации, обратной стороной которой является потеря Тьюринг-полноты. Тогда с этим справились, введя особую трактовку Y-комбинатора.

А что касается ошибок периода выполнения программ, то опять же, если мне не изменяет память, Лука Карделли утверждал, что type-sound program таковых не имеет?

В последнее время всё больший интерес вызывает сравнительно новое течение в ФП - Total Functional Programming.
Подробнее -- в работе Дэвида Тёрнера (создателя языков KRC, SASL, Miranda, оказавших огромное влияние на Хаскелл) "Total Functional Programming"

В чём отличие Total FP (или по другому Strong FP, сильное ФП) от обычного ФП (Weak FP)?

Ну, начнём с того, что даже в хрустально чистом Хаскелле понятие функции не совпадает с математическим. Функция в Хаскелле может зациклиться, и тогда она будет иметь особое значение, обозначаемое как _|_ -- bottom, или для наглядности: (_|_)  ;-)
Также, функции в Хаскелле могут вызвать ошибки - самые разные, от деления на ноль до попытки выборки первого элемента из пустого списка.
Всё это делает функции Хаскелла (да и других ФЯ) частично определёнными (partial functions). В математике же принято работать с полностью определёнными (total) функциями.

В Total FP нет такого значения, как _|_. Нет и исключений/авостов при выполнении функций. Любая валидная функция возвращает именно то значение, которое прописано в её типе.
Из этого следует важнейшее следствие -- любая допустимая функция гарантированно завершится. То есть, проблема останова уходит в прошлое, а вместе с нею и целый класс ошибок из-за зацикливаний в алгоритмах.

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

Соответственно, транслятор имеет больше свободы при оптимизации: где надо -- выполнит вычисления энергично, где выгоднее -- отложит их...

Проще сделать сам транслятор -- не нужно вводить особые правила для тех же логических операций AND/OR/and_then/or_else, откладывающие (или не откладывающие) вычисление правого операнда...

Конечно же, упрощается доказательство программ -- ведь они полностью подчиняются законам математической логики, equational reasoning, индуктивным доказательствам...

Правда, за всё нужно платить, и если некоторые издержки забавны (0/0 == 0), терпимы (обязательное полное сопоставление с образцом при обработке списков), то другие могут поставить в тупик...

Из теоремы Halting Theorem следует, что на языке, допускающем только завершающиеся программы, нельзя написать некоторые программы, которые всегда завершаются (например, интерпретатор самого этого языка). Это весьма похоже на теорему Гёделя о неполноте.

Из этого следует, что такой язык не будет полным по Тьюрингу.
Упрощённые валидаторы завершимости программ допускают только примитивно-рекурсивные функции, а значит, такие функции, как наивная ф. Фибоначчи, функция Аккермана или быстрая сортировка не могут быть реализованы. Правда, эти ограничения можно обойти, переписав фибоначчи на линейно-итеративный вариант, функцию Аккермана -- через функции высшего порядка, а вместо quicksort использовать аналогичный по операциям и времени выполнения вариант алгоритма treesort, переведя всех их на примитивную рекурсию.

Кроме того, алгоритмы этих валидаторов не стоят на месте, и современные варианты могут проверить допустимость и аккермана, и quicksort'а.

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

Тем не менее, интересно мнение продвинутой общественности, какие перспективы могут иметь сильные ФЯ, учитывая их главное достоинство -- завершимость всех программ.
А также, насколько сильны трудности жизни, накладываемые этими ограничениями...

ЗЫ. Также обсуждение на RSDN: http://www.rsdn.ru/Forum/message/2801824.flat.aspx

Ответ на »сообщение 4063« (Илья Ермаков)
___________________________

>>> Чем Вас не устраивает общепринятый стиль - и отступы, и скобки?

А зачем плодить лишние сущности? Если можно обойтись без begin/end, лучше обойтись без них...
Окаммеры, питонщики и хаскеллеры прекрасно обходятся и горя не знают. Даже эфшарперы и немерлисты предпочитают использовать значимые отступы. А почему? Да потому что текст программ при этом очищается от лишнего мусора. Да-да, Илья, именно от мусора...

Только не говорите что это, мол, повышение полезной избыточности. Что-то вот даже Вирт не стал вводить полезно-избыточные модификаторы PUBLIC и т.п., а обошёлся какими-то непонятными звёздочками, которые были оставлены в Компонентном Паскале, что сразу нарушило его цельность -- ведь в нём появились модификаторы LIMITED, ABSTRACT и т.д...

Впрочем, все эти бессмысленные прения о вкусовщине и глуповщине не имеют прямого (да и косвенного) отношения к ФП. Предлагаю вернуться к теме топика...

Ответ на »сообщение 4056« (Geo)
___________________________

Ответ на »сообщение 4055« (Jack Of Shadows)
___________________________
Теперь некоторые объективизированные возражения. Введение формата в язык наложит ограничение на мои возможности представить текст так, как мне удобно его воспринимать. Например, сейчас при большой вложенности я могу не сдвигать какой-то короткий внутренний блок, а, например, отбить его сверху и снизу пустыми строками.

А ещё представим проблемы, которые могут возникать при копипасте :-) Особенно, если вставляемый кусок использует отступы другой глубины. Ошибкоопасность копипаста хорошо известна. Тут она ещё более возрастает... В любом случае, при подобных манипуляциях с текстом у программиста уже не будет доверия, что всё сложилось верно, он будет вынужден перепроверять структуру повторно...

Ответ на »сообщение 4053« (Jack Of Shadows)
___________________________

Ответ на »сообщение 4052« (Geo)
___________________________
Я уже говорил, что скобки кодируют эту информацию в одном месте, а нам с вами она нужна совершенно в другом.

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