Аннотация:
В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..
Re: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий Владимирович, Вы писали:
<>
В языке со статической типизацией функция out или sum вполне может существовать... если этот язык, например, С++
struct Out
{
Out const& operator()(char const* s) const { puts(s); return *this; }
} out;
struct Sum
{
int value;
Sum(int v) : value(v) {}
Sum operator()(int x) const { return Sum(value+x); }
};
struct SumLauncher
{
Sum operator()(int x) const { return Sum(x); }
} sum;
int total(Sum s) { return s.value; } // как в хаскелле, делаем функцию для доступа к недрамint main()
{
out("hello")("world")("!");
return total( sum(1)(2)(3) );
}
потому что не одним Хиндли-Милнером живы.
В хаскелле, наверно, можно придумать аппликативный функтор, который так же изолировал бы тип... но я в них ещё не до конца вкурил, а прямо сейчас разбираться не хочу.
Чтобы вот такое было легальным
out <$> "hello" <*> "world" <*> "!"
Перекуём баги на фичи!
Re: Неправильное введение в функциональное программирование
Здравствуйте, Кодт, Вы писали:
К>Здравствуйте, Воронков Василий Владимирович, Вы писали: К><> К>В языке со статической типизацией функция out или sum вполне может существовать... если этот язык, например, С++
Насколько я помню, пример с sum был немного иной. Функция sum принимает список произвольной длины, после чего принимает количество аргументов, равное длине списка и производит сложение. Т.е. тип возвращаемой функции зависит от длины списка, при этом sum работает для списков любой длины.
Re: Неправильное введение в функциональное программирование
В языке же с динамической типизацией, где вас не сдерживает система типов, ваша фантазия практически ничем не ограничена. Вот пример функции на Ela, которая принимает список и возвращает другую функцию, число параметров которой равно количеству элементов в списке
...
В языке со статической типизацией данный код был бы невозможен, так как длина списка неизвестна нам на этапе компиляции, а следовательно, мы не можем определить, сколько именно аргументов будет у функции, которую возвращает fun.
Касательно полиморфных вариантов в окамле — не все так страшно, они не делают резкого прыжка к динамике, там же можно описывать в каждом желаемом месте определенные открытые или закрытые подмножества конструкторов, т.е. работать как с обычными алгебраиками, но могущими пересекаться. Впрочем, на практике у меня никогда не возникало желания ими пользоваться.
Re[3]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
К>>В языке со статической типизацией функция out или sum вполне может существовать... если этот язык, например, С++
ВВ>Насколько я помню, пример с sum был немного иной. Функция sum принимает список произвольной длины,
Не, sum там фиксированное число имеет, а про переменное число параметров там fun, уже в другой части статьи.
Re[4]: Неправильное введение в функциональное программирование
Здравствуйте, D. Mon, Вы писали:
DM>Здравствуйте, Воронков Василий, Вы писали: К>>>В языке со статической типизацией функция out или sum вполне может существовать... если этот язык, например, С++ ВВ>>Насколько я помню, пример с sum был немного иной. Функция sum принимает список произвольной длины, DM>Не, sum там фиксированное число имеет, а про переменное число параметров там fun, уже в другой части статьи.
Я сейчас просмотрел статью. Там есть функция sum, но нигде не утверждается, что в статических языках она невозможна. Более того, приводится ее реализация на C#.
Утверждение, что "в статике такое сделать нельзя" я нашел только в отношении:
fun (x::xs) = fun' x xs
where fun' a [] = \y -> y + a
fun' a (x::xs) = \y -> fun' (y + a + x) xs
И мне кажется, что невозможность такой функции в статике можно доказать чисто логически.
Или я чего там не доглядел? Давненько все же было написано
ЗЫ. А контр-пример с воображаемым апликативным функтором вообще довольно странный:
out <$> "hello" <*> "world" <*> "!"
Как бы тут ничего изобретать не надо:
1 + 2 + 3 + 4...
Re[2]: Неправильное введение в функциональное программирование
В языке же с динамической типизацией, где вас не сдерживает система типов, ваша фантазия практически ничем не ограничена. Вот пример функции на Ela, которая принимает список и возвращает другую функцию, число параметров которой равно количеству элементов в списке
DM>...
DM>В языке со статической типизацией данный код был бы невозможен, так как длина списка неизвестна нам на этапе компиляции, а следовательно, мы не можем определить, сколько именно аргументов будет у функции, которую возвращает fun.
DM>Тут ошибка. Есть языки со статической типизацией, позволяющие такое. Это языки с зависимыми типами. Пример подобной функции: DM>http://thedeemon.livejournal.com/73006.html
Насколько я понимаю этот пример, там тип функции описывается через "компонент", который получает свое значение в рантайме. Насколько такой тип можно считать статическим?
Re[5]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
ВВ>ЗЫ. А контр-пример с воображаемым апликативным функтором вообще довольно странный:
Это не контрпример, а попытка обобщить.
Оператор применения (f $ x) имеет тип (a->b) -> a -> b, а нам требуется xz -> a -> xz, поэтому функция out именно как функция не имеет типа в системе-F.
Кстати, и в сях она тоже не имеет типа.
Но в плюсах уже можно перегружать оператор().
Обобщением функции является аппликативный функтор, вот я и предположил, что надо копать в эту сторону. Только вместо оператора применения "пробел" будет какой-нибудь явный оператор — <$> который можно перегрузить подходящим образом.
Перекуём баги на фичи!
Re[3]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
ВВ>Насколько я понимаю этот пример, там тип функции описывается через "компонент", который получает свое значение в рантайме. Насколько такой тип можно считать статическим?
Хороший вопрос. Однако традиционно подобные типы таки считают статическими, ведь компилятор не позволит использовать их неправильно, проверит все статически.
Re[4]: Неправильное введение в функциональное программирование
Здравствуйте, D. Mon, Вы писали:
DM>Здравствуйте, Воронков Василий, Вы писали: ВВ>>Насколько я понимаю этот пример, там тип функции описывается через "компонент", который получает свое значение в рантайме. Насколько такой тип можно считать статическим? DM>Хороший вопрос. Однако традиционно подобные типы таки считают статическими, ведь компилятор не позволит использовать их неправильно, проверит все статически.
Тут ведь вся фишка в том, что статически проверить все невозможно:
sum x 2 2 2 2
Значение x в компайл-тайме неизвестно. Получается, что я таки могу использовать эту функцию неправильно?
Re[5]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
ВВ>Тут ведь вся фишка в том, что статически проверить все невозможно:
ВВ>
ВВ>sum x 2 2 2 2
ВВ>
ВВ>Значение x в компайл-тайме неизвестно. Получается, что я таки могу использовать эту функцию неправильно?
Нет. Просто тип результата такого вызова зависит от х, если он дальше используется непротиворечиво, то все ок, если же компилятор в этом не убежден, то не пропустит.
Простой пример. Хрестоматийный образец зависимого типа — вектор с длиной в типе Vect n a. Есть функция zip, принимающая вектора одной длины:
zip: (Vect n a) -> (Vect n b) -> Vect n (a, b)
Мы можем прочитать вектор чисел из файла, превратить его в вектор строк, а потом склеить эти два вектора этой функцией. Конкретное значение n компилятору статически неизвестно, но он видит, что длина параметров одинаковая, и этого ему достаточно. Это статическая проверка.
Для случая выше у нас, например, может быть функция, принимающая два аргумента одного типа,
f : Bool -> a -> a -> a
f c x y = if c then x else y
и два значения:
s1 = sum x 2 2 2 2
s2 = sum x 3 5 x x
Их можно будет передать в ту функцию,
z = f some_bool s1 s2
т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.
Re[6]: Неправильное введение в функциональное программирование
Здравствуйте, D. Mon, Вы писали:
DM>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.
Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?
По-моему это не совсем аналогично моему примеру
Re[7]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
DM>>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.
ВВ>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?
Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
Re[8]: Неправильное введение в функциональное программирование
Здравствуйте, D. Mon, Вы писали:
DM>>>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет. ВВ>>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?
DM>Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
Но ведь по сути это означает, что ты не сможешь написать код на Ирдисе, аналогичный такому:
fun (x::xs) = fun' x xs
where fun' a [] = \y -> y + a
fun' a (x::xs) = \y -> fun' (y + a + x) xs
(fun [1..3] 1 2 3, fun [1..5] 1 2 3 4 5, fun [1..7] 1 2 3 4 5 6 7)
Здравствуйте, D. Mon, Вы писали:
DM>Здравствуйте, Воронков Василий, Вы писали:
DM>>>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.
ВВ>>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?
DM>Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
Проще говоря, я не понимаю, как это можно считать аналогом. Тебе, чтобы твоя функция могла использоваться, нужно фактически доказать, что значение, от которого зависит ее тип, всегда равно 4. Но зачем вообще тогда городить зависимые типы? Просто написал в коде "4" — и все Эффект тот же. А функция, которая как бы есть, но результат ее применения нельзя использовать, пока ты не напишешь подобное доказательство... Ну, по-моему, это немного не то. Фишка-то в том, что значение может быть разным, и ты в компайл-тайм можешь не знать его.
Re[9]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
DM>>Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
ВВ>Но ведь по сути это означает, что ты не сможешь написать код на Ирдисе, аналогичный такому:
ВВ>
ВВ>fun (x::xs) = fun' x xs
ВВ> where fun' a [] = \y -> y + a
ВВ> fun' a (x::xs) = \y -> fun' (y + a + x) xs
ВВ>(fun [1..3] 1 2 3, fun [1..5] 1 2 3 4 5, fun [1..7] 1 2 3 4 5 6 7)
ВВ>
ВВ>Разве нет?
Нет, отлично могу. Суммируем список и столько аргументов, сколько элементов в списке:
sumType : Nat -> Type
sumType Z = Int
sumType (S k) = Int -> sumType k
adder : (n:Nat) -> Int -> sumType n
adder Z acc = acc
adder (S k) acc = \x => adder k (x + acc)
fun : (xs : List Int) -> sumType (length xs)
fun xs = adder (length xs) (sum xs)
main : IO ()
main = print (fun [1,2,3] 1 2 3, fun [1,2,3,4,5] 10 20 30 40 50)
Выводит
(12, 165)
Re[9]: Неправильное введение в функциональное программирование
Здравствуйте, Воронков Василий, Вы писали:
ВВ>>>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?
DM>>Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
ВВ>Проще говоря, я не понимаю, как это можно считать аналогом. Тебе, чтобы твоя функция могла использоваться, нужно фактически доказать, что значение, от которого зависит ее тип, всегда равно 4.
Нет, не чтобы функция могла использоваться, а чтобы результат вызова с 4 аргументами мог использоваться как число.
В Ela абсолютно то же самое — ты можешь использовать sum x 2 2 2 2 как число только если х=4.
Но и та, и там ты можешь использовать sum x 2 2 2 2 для бОльших х как не число, а функцию.
И ни там, ни там sum x 2 2 2 2 не имеет смысла при х меньше 4.
Только Идрис это все проверяет статически.
Re[10]: Неправильное введение в функциональное программирование
Здравствуйте, D. Mon, Вы писали:
DM>Здравствуйте, Воронков Василий, Вы писали:
ВВ>>>>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?
DM>>>Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
ВВ>>Проще говоря, я не понимаю, как это можно считать аналогом. Тебе, чтобы твоя функция могла использоваться, нужно фактически доказать, что значение, от которого зависит ее тип, всегда равно 4.
DM>Нет, не чтобы функция могла использоваться, а чтобы результат вызова с 4 аргументами мог использоваться как число. DM>В Ela абсолютно то же самое — ты можешь использовать sum x 2 2 2 2 как число только если х=4. DM>Но и та, и там ты можешь использовать sum x 2 2 2 2 для бОльших х как не число, а функцию. DM>И ни там, ни там sum x 2 2 2 2 не имеет смысла при х меньше 4. DM>Только Идрис это все проверяет статически.
В Ela, как в любой динамике, ты можешь получить результат апликации, увидеть, что это функция, и продолжать ее применять, пока вызов не будет сатурирован.
Re[10]: Неправильное введение в функциональное программирование
Перекуём баги на фичи!
Эффект тот же. А функция, которая как бы есть, но результат ее применения нельзя использовать, пока ты не напишешь подобное доказательство... Ну, по-моему, это немного не то. Фишка-то в том, что значение может быть разным, и ты в компайл-тайм можешь не знать его.
