Неправильное введение в функциональное программирование
От: Воронков Василий Владимирович Россия  
Дата: 27.11.13 14:39
Оценка: 1425 (16)
Статья:
Неправильное введение в функциональное программирование
Автор(ы): Воронков Василий Владимирович
Дата: 03.04.2013
В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..


Авторы:
Воронков Василий Владимирович

Аннотация:
В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..
Re: Неправильное введение в функциональное программирование
От: Кодт Россия  
Дата: 27.11.13 22:10
Оценка:
Здравствуйте, Воронков Василий Владимирович, Вы писали:

<>
В языке со статической типизацией функция 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: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 06:52
Оценка:
Опечатка:

Таким образом, каррирование – это преобразование функции вида (a -> b) -> c в функцию вида a->b->c

Должно быть "функции вида (a, b) -> c".
Re[2]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 07:07
Оценка:
Здравствуйте, Кодт, Вы писали:

К>Здравствуйте, Воронков Василий Владимирович, Вы писали:

К><>
К>В языке со статической типизацией функция out или sum вполне может существовать... если этот язык, например, С++

Насколько я помню, пример с sum был немного иной. Функция sum принимает список произвольной длины, после чего принимает количество аргументов, равное длине списка и производит сложение. Т.е. тип возвращаемой функции зависит от длины списка, при этом sum работает для списков любой длины.
Re: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 07:23
Оценка:

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


Тут ошибка. Есть языки со статической типизацией, позволяющие такое. Это языки с зависимыми типами. Пример подобной функции:
http://thedeemon.livejournal.com/73006.html


Касательно полиморфных вариантов в окамле — не все так страшно, они не делают резкого прыжка к динамике, там же можно описывать в каждом желаемом месте определенные открытые или закрытые подмножества конструкторов, т.е. работать как с обычными алгебраиками, но могущими пересекаться. Впрочем, на практике у меня никогда не возникало желания ими пользоваться.
Re[3]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 07:28
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

К>>В языке со статической типизацией функция out или sum вполне может существовать... если этот язык, например, С++


ВВ>Насколько я помню, пример с sum был немного иной. Функция sum принимает список произвольной длины,


Не, sum там фиксированное число имеет, а про переменное число параметров там fun, уже в другой части статьи.
Re[4]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 08:03
Оценка:
Здравствуйте, 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]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 08:14
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>

В языке же с динамической типизацией, где вас не сдерживает система типов, ваша фантазия практически ничем не ограничена. Вот пример функции на Ela, которая принимает список и возвращает другую функцию, число параметров которой равно количеству элементов в списке
DM>...
DM>В языке со статической типизацией данный код был бы невозможен, так как длина списка неизвестна нам на этапе компиляции, а следовательно, мы не можем определить, сколько именно аргументов будет у функции, которую возвращает fun.

DM>Тут ошибка. Есть языки со статической типизацией, позволяющие такое. Это языки с зависимыми типами. Пример подобной функции:
DM>http://thedeemon.livejournal.com/73006.html

Насколько я понимаю этот пример, там тип функции описывается через "компонент", который получает свое значение в рантайме. Насколько такой тип можно считать статическим?
Re[5]: Неправильное введение в функциональное программирование
От: Кодт Россия  
Дата: 28.11.13 08:35
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>ЗЫ. А контр-пример с воображаемым апликативным функтором вообще довольно странный:


Это не контрпример, а попытка обобщить.
Оператор применения (f $ x) имеет тип (a->b) -> a -> b, а нам требуется xz -> a -> xz, поэтому функция out именно как функция не имеет типа в системе-F.
Кстати, и в сях она тоже не имеет типа.
Но в плюсах уже можно перегружать оператор().
Обобщением функции является аппликативный функтор, вот я и предположил, что надо копать в эту сторону. Только вместо оператора применения "пробел" будет какой-нибудь явный оператор — <$> который можно перегрузить подходящим образом.
Перекуём баги на фичи!
Re[3]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 08:49
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Насколько я понимаю этот пример, там тип функции описывается через "компонент", который получает свое значение в рантайме. Насколько такой тип можно считать статическим?


Хороший вопрос. Однако традиционно подобные типы таки считают статическими, ведь компилятор не позволит использовать их неправильно, проверит все статически.
Re[4]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 09:26
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>Насколько я понимаю этот пример, там тип функции описывается через "компонент", который получает свое значение в рантайме. Насколько такой тип можно считать статическим?
DM>Хороший вопрос. Однако традиционно подобные типы таки считают статическими, ведь компилятор не позволит использовать их неправильно, проверит все статически.

Тут ведь вся фишка в том, что статически проверить все невозможно:

sum x 2 2 2 2


Значение x в компайл-тайме неизвестно. Получается, что я таки могу использовать эту функцию неправильно?
Re[5]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 10:01
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Тут ведь вся фишка в том, что статически проверить все невозможно:


ВВ>
ВВ>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]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 10:53
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.


Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?

По-моему это не совсем аналогично моему примеру
Re[7]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 11:05
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

DM>>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.


ВВ>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?


Только в том случае, если дальше в коде мы на это полагаемся (используя результат как число). Т.е. только тогда, когда это необходимо для корректности программы.
Re[8]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 11:38
Оценка:
Здравствуйте, 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)


Запустить в браузере

Разве нет?
Re[8]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 11:47
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


DM>>>т.к. компилятор будет уверен, что эти значения имеют одинаковый тип, но какой именно — полностью статически неизвестно. Если же где-то мы захотим эти значения использовать как числа, тут-то и появится новое условие: результат должен быть числом, а значит нужно доказательство, что x=4, в противном случае компилятор такую программу не примет.


ВВ>>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 4?


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


Проще говоря, я не понимаю, как это можно считать аналогом. Тебе, чтобы твоя функция могла использоваться, нужно фактически доказать, что значение, от которого зависит ее тип, всегда равно 4. Но зачем вообще тогда городить зависимые типы? Просто написал в коде "4" — и все Эффект тот же. А функция, которая как бы есть, но результат ее применения нельзя использовать, пока ты не напишешь подобное доказательство... Ну, по-моему, это немного не то. Фишка-то в том, что значение может быть разным, и ты в компайл-тайм можешь не знать его.
Re[9]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 12:15
Оценка: 3 (1)
Здравствуйте, Воронков Василий, Вы писали:

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]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 12:19
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>>>Иначе говоря, мы должны статически доказать, что "значение, известное только в рантайме" должно быть равно именно 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]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 12:29
Оценка:
Здравствуйте, 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]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 12:40
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>
DM>sumType : Nat -> Type
DM>sumType Z = Int
DM>sumType (S k) = Int -> sumType k

DM>adder : (n:Nat) -> Int -> sumType n
DM>adder Z acc = acc
DM>adder (S k) acc = \x => adder k (x + acc)

DM>fun : (xs : List Int) -> sumType (length xs)
DM>fun xs = adder (length xs) (sum xs)

DM>main : IO ()
DM>main = print (fun [1,2,3] 1 2 3, fun [1,2,3,4,5] 10 20 30 40 50)
DM>


А если вот так:

main = print (fun [1,2,3] 1 2 3 4, fun [1,2,3,4,5] 10 20 30 40 50)


Сгенерирует ли компилятор ошибку и что это будет за ошибка?
Re[11]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 12:41
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>В Ela, как в любой динамике, ты можешь получить результат апликации, увидеть, что это функция, и продолжать ее применять, пока вызов не будет сатурирован.


И? Все равно ты не получишь число, пока не применишь должное число аргументов, хоть бы и в цикле. Язык со статическими типами заставит тебя сделать примерно то же, и проверит при этом, что цикл правильный. Фактически, и там и там типы могут зависеть от рантайм значений, разница лишь в том, что язык со статической типизацией заставляет с ними обращаться корректно.
Re[11]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 12:45
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>А если вот так:

ВВ>main = print (fun [1,2,3] 1 2 3 4, fun [1,2,3,4,5] 10 20 30 40 50)

ВВ>Сгенерирует ли компилятор ошибку и что это будет за ошибка?


Да, конечно, в этом весь смысл статической проверки типов.
Говорит:
Type checking .\add.idr
add.idr:23:When elaborating right hand side of main:
fun [1,2,3] 1 2 3 does not have a function type (Int)
Re[12]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 13:02
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>А если вот так:

ВВ>>main = print (fun [1,2,3] 1 2 3 4, fun [1,2,3,4,5] 10 20 30 40 50)

ВВ>>Сгенерирует ли компилятор ошибку и что это будет за ошибка?

DM>Да, конечно, в этом весь смысл статической проверки типов.
DM>Говорит:
DM>Type checking .\add.idr
DM>add.idr:23:When elaborating right hand side of main:
DM>fun [1,2,3] 1 2 3 does not have a function type (Int)

Вот, собственно, интересно — откуда компилятор узнал, что "fun [1,2,3]"? У нас же по легенде это рантайм значение? Закрадывается подозрение, что Ирдис просто достаточно умен для того, чтобы обращаться с константами как с константами.
А если усложнить задачу:


fun (x::xs) = fun' x xs
                where fun' a [] = \y -> y + a
                      fun' a (x::xs) = \y -> fun' (y + a + x) xs

saturate x f = if f is Fun then saturate x (f x) else f

process [] = []
process [x] = [x]
process (x::xs) = saturate x (fun xs) :: process xs

process [1..10]
Re[13]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 13:51
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>А если усложнить задачу


Легко. Только вместо хранения тэга внутри динамически типизированного значения f, у нас f имеет тип sumType n для некоторого n, и чтобы осмысленно с ним работать придется передать и само n. В остальном очень похоже:
saturate : (n:Nat) -> Int -> sumType n -> Int
saturate Z x f = f
saturate (S k) x f = saturate k x (f x)

process : List Int -> List Int
process [] = []
process [x] = [x]
process (x::xs) = saturate (length xs) x (fun xs) :: process xs

Проверяем:
Type checking .\add.idr
*add> process [1..10]
[63,68,70,69,65,58,48,35,19,10] : List Int
Re[13]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 15:44
Оценка: 9 (1)
Здравствуйте, Воронков Василий, Вы писали:

ВВ> У нас же по легенде это рантайм значение?


Чтобы развеять путаницу, возьмем поистине рантайм значение — будем читать список из аргументов командной строки.

fun : (xs : List Int) -> sumType (length xs)
fun xs = adder (length xs) (sum xs)

saturate : (n:Nat) -> Int -> sumType n -> Int
saturate Z x f = f
saturate (S k) x f = saturate k x (f x)

convertArgs : List String -> List Int
convertArgs [] = []
convertArgs (x::xs) = map cast xs

main : IO ()
main = do 
  as <- getArgs
  let xs = convertArgs as
  let f = fun xs                      -- вот тут тип f зависит от длины прочитанного списка
  print $ saturate (length xs) 100 f  -- но это не проблема

Вызываем из командной строки
add.exe 1 2 3
получаем ответ
306

При этом если мы последнюю строчку заменим на
print $ saturate (length xs + 1) 100 f
то компилятор ругнется:
add.idr:35:When elaborating right hand side of main:
Can't unify
        sumType (Prelude.List.length xs)
with
        sumType (Prelude.List.length xs + 1)

Т.е. таки проверяет понаписанное на корректность.
Re[14]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 15:51
Оценка:
Здравствуйте, D. Mon, Вы писали:

Ну да, легко. Отложенная типизация в действии =)
А ты попробуй передать список через командную строку или сформировать его на основе пользовательского ввода. Ведь на самом деле здесь же нет зависимости типа функции от *рантайм* значений, правда?
Re[15]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 28.11.13 16:02
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>А ты попробуй передать список через командную строку или сформировать его на основе пользовательского ввода. Ведь на самом деле здесь же нет зависимости типа функции от *рантайм* значений, правда?


От значений нет, конечно. Если список будет из командной строки, то компилятор наверняка просто потребует наличие чего-то типа "if (list.length == 4)" перед его использованием.
Re[14]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 16:09
Оценка:
Здравствуйте, D. Mon, Вы писали:

Ну это пример такой получился удобный, который работает для списка любой длины; главное, чтобы length xs было именно длиной списка. А вот тут, я так понимаю, ругнется сразу:

fun [1..arg] 1 2 3


arg соответственно из командной строки.
Re[15]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 16:13
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Ну да, легко. Отложенная типизация в действии =)


Никакой отложенной.

ВВ>А ты попробуй передать список через командную строку или сформировать его на основе пользовательского ввода.


Уже.

ВВ>Ведь на самом деле здесь же нет зависимости типа функции от *рантайм* значений, правда?


Не правда. Зависимые типы реально зависят от рантайм значений. И делают это статически. Такой вот коан.
Re[15]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 16:19
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ> А вот тут, я так понимаю, ругнется сразу:

ВВ>fun [1..arg] 1 2 3
ВВ>arg соответственно из командной строки.

Да, ведь и без запуска видно, что программа содержит баг: при arg меньше 3 будет фигня. А программы с багами не компилируются в приличных языках, для этого статическая типизация и нужна.
Re[16]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 16:21
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>Ну да, легко. Отложенная типизация в действии =)

DM>Никакой отложенной.


Мне кажется, это она и есть.

ВВ>>А ты попробуй передать список через командную строку или сформировать его на основе пользовательского ввода.

DM>Уже.
ВВ>>Ведь на самом деле здесь же нет зависимости типа функции от *рантайм* значений, правда?

DM>Не правда. Зависимые типы реально зависят от рантайм значений. И делают это статически. Такой вот коан.


Ну ты сам-то не понимаешь, что это невозможно?
Я просто пример привел такой удачный, что Идрис смог построить зависимость от длины списка. В итоге смог доказать корректность saturate статически, без всякой зависимости от рантайма.
Re[17]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 28.11.13 16:59
Оценка: 6 (1)
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Мне кажется, это она и есть.


Что именно ты называешь отложенной типизацией и как она может работать в идрисе?

ВВ>>>Ведь на самом деле здесь же нет зависимости типа функции от *рантайм* значений, правда?

DM>>Не правда. Зависимые типы реально зависят от рантайм значений. И делают это статически. Такой вот коан.
ВВ>Ну ты сам-то не понимаешь, что это невозможно?

Это еще как возможно. Вот еще простой пример:
module Main
import System

myType : Bool -> Type  -- тип, зависящий от значения
myType False = Int
myType True = String

create : (n:Bool) -> myType n   -- создадим значение, тип которого зависит от переданного аргумента
create False = 22
create True = "zebra"

useValue : (p:Bool) -> myType p -> String  -- тип второго аргумента зависит от рантайм значения первого
useValue False v = show $ 20 + v           -- если это инт, складываем с 20 и переводим в строку
useValue True v = "a " ++ v                -- если это строка, склеиваем с другой строкой

main : IO ()
main = do
  args <- getArgs          -- читаем аргументы командной строки, рантайм значение
  let p = length args > 1  -- передано ли что-то? рантайм значение
  let v = create p         -- тип v зависит от рантайм значения p, это или Int или String 
  print $ useValue p v     -- передаем значение типа, который мы не знаем статически, но точно можем обработать все равно


ВВ>Я просто пример привел такой удачный, что Идрис смог построить зависимость от длины списка. В итоге смог доказать корректность saturate статически, без всякой зависимости от рантайма.


Это и есть важнейшее свойство таких языков — компилируются лишь те программы, для которых доказана корректная работа на любых данных. Типы могут быть внутри самые разные и выбираться динамически в рантайме, но какие бы они не были, все должно сойтись, все случаи корректно рассмотрены и обработаны, и вот эта полнота рассмотрения статически доказана.
Re[18]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 28.11.13 19:25
Оценка: -1
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>Мне кажется, это она и есть.
DM>Что именно ты называешь отложенной типизацией и как она может работать в идрисе?

Функция типизируется в момент первого применения. В общем это не только для зависимых типов полезно. Полиморфные функции во многих языках есть.
ВВ>>>>Ведь на самом деле здесь же нет зависимости типа функции от *рантайм* значений, правда?
DM>>>Не правда. Зависимые типы реально зависят от рантайм значений. И делают это статически. Такой вот коан.
ВВ>>Ну ты сам-то не понимаешь, что это невозможно?

DM>Это еще как возможно. Вот еще простой пример:

DM>
DM>module Main
DM>import System

DM>myType : Bool -> Type  -- тип, зависящий от значения
DM>myType False = Int
DM>myType True = String

DM>create : (n:Bool) -> myType n   -- создадим значение, тип которого зависит от переданного аргумента
DM>create False = 22
DM>create True = "zebra"

DM>useValue : (p:Bool) -> myType p -> String  -- тип второго аргумента зависит от рантайм значения первого
DM>useValue False v = show $ 20 + v           -- если это инт, складываем с 20 и переводим в строку
DM>useValue True v = "a " ++ v                -- если это строка, склеиваем с другой строкой

DM>main : IO ()
DM>main = do
DM>  args <- getArgs          -- читаем аргументы командной строки, рантайм значение
DM>  let p = length args > 1  -- передано ли что-то? рантайм значение
DM>  let v = create p         -- тип v зависит от рантайм значения p, это или Int или String 
DM>  print $ useValue p v     -- передаем значение типа, который мы не знаем статически, но точно можем обработать все равно
DM>


Здесь нет зависимости от рантайм значений, ведь эта программа доказывается статически. "Доказывается статически" означает, что возможный диапазон значений нам известен в компайл тайм, и мы можем доказать, что ни при каких случаях не выйдем из этого диапазона. Откуда здесь взяться зависимости от рантайма? Тут ее нет

А вот тут есть:

open core monad io

calc max acc n 
  | x < max = calc max x
  | else = Some x
  where x = n + acc

iterate f = do
  putStrLn "Need value:"
  x <- readAny
  match f x with
        Some x = mkIO x
        x = iterate x

do
  putStrLn "Max:"
  max <- readAny
  x <- iterate $ calc max 0
  putStrLn $ show x



Running module test3

Max:
42
Need value:
29
Need value:
11
Need value:
123
163

Session ended. Session taken: 00:00:08.4393606


DM>Это и есть важнейшее свойство таких языков — компилируются лишь те программы, для которых доказана корректная работа на любых данных. Типы могут быть внутри самые разные и выбираться динамически в рантайме, но какие бы они не были, все должно сойтись, все случаи корректно рассмотрены и обработаны, и вот эта полнота рассмотрения статически доказана.


"Зависимость от рантайм-значений" означает "Зависимость от значений, который становятся *известны* только в рантайме". А для того, чтобы программа была доказуема статически, ее нужно свести к набору значений, который известен уже в период компиляции. Никаких "нежданчиков" там быть не может. Так что это, мягко говоря, не одно и то же
Re: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 28.11.13 20:38
Оценка:

f = fun [1,2,3]
f 1 2 3
//Вывод:
//12


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


Код возможен. Но, очевидно, для runtime данных проверка будет в runtime:
#include <initializer_list>
#include <iostream>
#include <cstddef>
#include <cassert>
#include <vector>
using namespace std;

struct Variadic
{
    size_t n;
    template<typename ...Args>
    void operator()(Args ...args)
    {
        assert(n == sizeof...(args) );
    }
};

Variadic fun(vector<int> x)
{
    return {x.size()};
}

int main()
{
    vector<int> x{1,2,3};
    fun(x)(1,2,3); // Runtime OK
    cout << "OK" << endl;
    fun(x)(1); // assert fail
}
Re: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 28.11.13 21:08
Оценка:

Ответ прост. Мы считаем ее чистой, потому что списки в функциональных языках сравниваются не ссылочно (как, к примеру, массивы в C#), а структурно. Поэтому результаты двух вызовов этой функции эквивалентны, что несложно проверить в GHCi:

Equivalence != Equality

Вовсе нет. Давайте представим, что массивы в C# сравниваются именно структурно. Таким образом, два массива с одинаковым набором элементов будут считаться равными. И тогда мы сможем написать такой код:

var arr1 = new int[] { 1,2,3 };
var arr2 = new int[] { 1,2,3 };

if (arr1 == arr2)
  Console.WriteLine("arr1 и arr2 это один и тот же массив.");

arr1[0] = 10;

if (arr1 != arr2)
  Console.WriteLine("arr1 и arr2 это разные массивы.");


В результате выведется:

arr1 и arr2 это один и тот же массив.
arr1 и arr2 это разные массивы.

Как же так? Мгновение назад массивы были одинаковыми, а теперь они разные?

Как вы понимаете, во всем виновата «изменчивая природа» массивов. Так как вы можете поменять значения «по месту» (в отличие от связных списков в Хаскелле, любая операция над которыми приводит к созданию нового списка), то структурная эквивалентность уже не годится.


Неверно
Тот факт, что функция возвращает изменяемые объекты (но равные!) — не лишает её purity. Важно именно равенство возвращаемых значений.
Во многих примерах чистых функций, значение результата можно изменить:
double sin(double);
// ...
auto &&x = sin(0.0);
x = 0.11;


Кстати, вот тут Александр Степанов даёт определение равенству:

[...]
Definition: Two objects are equal if their corresponding parts are equal (applied recursively), including remote parts (but not comparing their addresses), excluding inessential components, and excluding components which identify related objects.
Once we have identified the parts of an object which must be tested for equality, we know from the earlier discussion that at least those parts must be copied by copy constructors or assignment operators. In particular, these operators must make copies of remote parts, rather than simply copying the pointers to them.
Now let us return to part of the logicians’ definition of equality. Recall that we would like the following statement to be true:

x == y ⇒ ∀ “reasonable” function foo, foo(x)==foo(y)

It is necessary to limit our expectations to some subset of possible functions foo.
For instance, this statement will not hold for the “address-of” function applied to distinct objects with equal values, nor will it hold for any other function which distinguishes between individual objects rather than between their values.
Considering an example will demonstrate some of the challenges facing a designer of generic components.
[...]

Re: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 28.11.13 22:58
Оценка:

К тому же в большинстве популярных объектно-ориентированных языков, включая C#, понятие алгебраический тип попросту отсутствует.


Справедливости ради стоит отметить, что в C++1998 tagged union прекрасно реализуется в виде библиотеки:
#include <boost/variant.hpp>
#include <iostream>
#include <ostream>

using namespace std;
using namespace boost;


struct Cellphone { bool touch_screen; };
struct Laptop { double screen_size; };

typedef variant<Cellphone, Laptop> Product;

struct Print: static_visitor<>
{
    void operator()(const Cellphone &x) const
    {
        cout << "Cellphone, touch_screen:" << x.touch_screen << endl;
    }
    void operator()(const Laptop &x) const
    {
        cout << "Laptop, screen_size:" << x.screen_size << endl;
    }
};

int main()
{
    Cellphone phone = {true};
    Laptop laptop = {11.1};
    
    Product x = phone;
    apply_visitor(Print(), x);
    x = laptop;
    apply_visitor(Print(), x);
}
Причём можно реализовать и "полиморфные варианты", а-ля Boost.Any, Boost.TypeErasure, и смешивать их как угодно с closed variant'ами или с обычным ООП. Например:
variant<ConcreteClass1, ConcreteClass2, function<void()>, unique_ptr<IAbstract>> x;


А в языке D он есть в стандартной библиотеке std.VariantN
Re[19]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 04:02
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

DM>>Что именно ты называешь отложенной типизацией и как она может работать в идрисе?

ВВ>Функция типизируется в момент первого применения.

Звучит как немерлизм, ни в одном нормальном языке такого нет (чтобы именно первого). Формально это ересь, тип функции тут указан уже при определении, а потом лишь используется. Но если речь просто про полиморфизм, то да, тут одна из его форм, параметризованный тип.

DM>>

useValue : (p:Bool) -> myType p -> String  -- тип второго аргумента зависит от рантайм значения первого
useValue False v = show $ 20 + v           -- если это инт, складываем с 20 и переводим в строку
useValue True v = "a " ++ v                -- если это строка, склеиваем с другой строкой

  let p = length args > 1  -- передано ли что-то? рантайм значение
  let v = create p         -- тип v зависит от рантайм значения p, это или Int или String 
  print $ useValue p v     -- передаем значение типа, который мы не знаем статически, но точно можем обработать все равно


ВВ>Здесь нет зависимости от рантайм значений, ведь эта программа доказывается статически. "Доказывается статически" означает, что возможный диапазон значений нам известен в компайл тайм, и мы можем доказать, что ни при каких случаях не выйдем из этого диапазона. Откуда здесь взяться зависимости от рантайма? Тут ее нет


Ну что значит нет? Значение v тут один раз создается и передается. Какого оно типа? Зависит от того, как мы программу запустили, что ей передали. Это и есть зависимость от рантайма в чистом виде, а не твои странные определения.

ВВ>"Зависимость от рантайм-значений" означает "Зависимость от значений, который становятся *известны* только в рантайме".


Ровно так и есть же в этом примере. Есть зависимость типа от булевого значения, истина там или ложь — будет известно только в рантайме.

BB>А для того, чтобы программа была доказуема статически, ее нужно свести к набору значений, который известен уже в период компиляции. Никаких "нежданчиков" там быть не может. Так что это, мягко говоря, не одно и то же


Да, "набор" значений должен быть известен статически, но он может быть бесконечным. В примере выше, где список читался извне, тип функции зависел от длины списка, который мог быть сколь угодно длинным (если закрыть глаза на технические ограничения ОС). Т.е. в зависимости от переданных данных могло получиться значение типа
Int
Int -> Int
Int -> Int -> Int
Int -> Int -> Int -> Int
...
хоть Int -> ... 100500 раз -> Int

Но ты прав, что обо всех этих множествах мы должны быть способны рассуждать статически, именно это зависимые типы и позволяют, описать рантайм зависимость статически. "Нежданчиков" там быть не может быть, потому что любой настоящий "нежданчик" это баг, это то, что твоя программа не способна обработать и упадет или выдаст мусор. Такие баги-нежданчики статическая типизация уничтожает. Незачем позволять компилировать программы с такими явными багами.
Re[2]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 04:11
Оценка: -1
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Кстати, вот тут Александр Степанов даёт определение равенству:

EP>Definition: Two objects are equal if their corresponding parts are equal (applied recursively), including remote parts (but not comparing their addresses), excluding inessential components, and excluding components which identify related objects.
EP>Once we have identified the parts of an object which must be tested for equality, we know from the earlier discussion that at least those parts must be copied by copy constructors or assignment operators. In particular, these operators must make copies of remote parts, rather than simply copying the pointers to them.

Это похоже на С++ головного мозга, а не определение. Вот несколько значений, какие из них равны и почему?
a = \x -> 2 * x
b = \x -> 2 * x
c = \x -> x * 2
d = \x -> a x
e = \x -> x + x
Re[2]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 04:21
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

BB>>К тому же в большинстве популярных объектно-ориентированных языков, включая C#, понятие алгебраический тип попросту отсутствует.

EP>Справедливости ради стоит отметить, что в C++1998 tagged union прекрасно реализуется в виде библиотеки

К сожалению, это лишь жалкое подобие, потому что при поддержке алгебраиков в языке важно не только умение их конструировать, но и паттер-матчинг, в том числе вложенный:
has55 :: [Maybe Int] -> Bool
has55 [] = False
has55 (Just 5 : Just 5 : rest) = True
has55 (_ : rest) = has55 rest

На вызовах визиторов такое делать не шибко неудобно, мягко говоря.
Re[3]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 04:30
Оценка:
Errata. В посте выше читать:
"паттерн-матчинг"
"не шибко удобно"
Re[19]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 08:21
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Здесь нет зависимости от рантайм значений, ведь эта программа доказывается статически. "Доказывается статически" означает, что возможный диапазон значений нам известен в компайл тайм, и мы можем доказать, что ни при каких случаях не выйдем из этого диапазона. Откуда здесь взяться зависимости от рантайма? Тут ее нет


ВВ>А вот тут есть:


ВВ>  match f x with
ВВ>        Some x = mkIO x
ВВ>        x = iterate x


Этот пример настолько примитивный, что даже зависимых типов не просит, хватает обычных алгебраиков. Вот эта же программа на Идрисе:

readInt : IO Int
readInt = map cast getLine 

data R = Fn (Int -> R) | Nbr Int

calc : Int -> Int -> Int -> R
calc max acc n =
  let x = n + acc in
  if x < max then Fn (calc max x) else Nbr x

iterate : (Int -> R) -> IO Int
iterate f = do
  putStrLn "Need value:"
  x <- readInt
  case f x of
    Nbr x => return x
    Fn x => iterate x

main : IO ()
main = do
  putStrLn "Max:"
  max <- readInt
  x <- iterate $ calc max 0
  print x

Просто у тебя один вид значений отличался от другого тэгом Some, а здесь для них заведены тэги Nbr и Fn, смысл тот же абсолютно.
Re[2]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 08:53
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>

EP>К тому же в большинстве популярных объектно-ориентированных языков, включая C#, понятие алгебраический тип попросту отсутствует.

EP>Справедливости ради стоит отметить, что в C++1998 tagged union прекрасно реализуется в виде библиотеки:

Справедливости ради, данная реализация ничем не отличается от той, что я привожу на C#. Статические проверки вы библиотеками не добавите. Так что, увы, отсутствуют.
Re[2]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 08:57
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Неверно

EP>Тот факт, что функция возвращает изменяемые объекты (но равные!) — не лишает её purity. Важно именно равенство возвращаемых значений.

Верно. Лишает.
Чистота — это ER. C изменяемыми типами данных никакого ER не будет. У вас просто неправильное представление о чистых функциях
Re[3]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 12:36
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Это похоже на С++ головного мозга, а не определение.


Чего шумишь, тебя обидел кто?

DM>Вот несколько значений, какие из них равны и почему?

DM>
DM>a = \x -> 2 * x
DM>b = \x -> 2 * x
DM>c = \x -> x * 2
DM>d = \x -> a x
DM>e = \x -> x + x
DM>


Зависит от свойств операций + и *, и связи между ними.
Ты статью прочитай, там как раз обсуждается пример про рациональные числа задаваемые двумя целыми.
Re[3]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 12:38
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>но и паттер-матчинг, в том числе вложенный:


Это всё понятно — в статье этого не было, там акцент совершенно на другое
Re[3]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 12:40
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Справедливости ради, данная реализация ничем не отличается от той, что я привожу на C#. Статические проверки вы библиотеками не добавите. Так что, увы, отсутствуют.


Какие именно статические проверки?
Re[3]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 12:47
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

EP>>Неверно

EP>>Тот факт, что функция возвращает изменяемые объекты (но равные!) — не лишает её purity. Важно именно равенство возвращаемых значений.
ВВ>Верно. Лишает.
ВВ>Чистота — это ER. C изменяемыми типами данных никакого ER не будет. У вас просто неправильное представление о чистых функциях

Вообще-то ER никуда не исчезает. Если функция возвращает равные значения для равных аргументов, вызов такой функции можно заменить результатом полученным ранее (для того же аргумента).
То что переменную-результат можно изменить — это вообще ортогонально.
Re[4]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 12:53
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Здравствуйте, Воронков Василий, Вы писали:


EP>>>Неверно

EP>>>Тот факт, что функция возвращает изменяемые объекты (но равные!) — не лишает её purity. Важно именно равенство возвращаемых значений.
ВВ>>Верно. Лишает.
ВВ>>Чистота — это ER. C изменяемыми типами данных никакого ER не будет. У вас просто неправильное представление о чистых функциях

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

EP>То что переменную-результат можно изменить — это вообще ортогонально.

Заменить — это значит заменить. Если "х" — чистое, и "x = y", то все "y" можно заменить на "x", и смысл программы от этого не изменится. Теперь представляем, что будет с изменяемыми структурами данных:

x = fun --Эквивалентно? Да!

--Тут мы как-то "поменяли" x
--Что дальше? ER работает, да? Можно заменить x на fun?
Re[4]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 12:54
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

DM>>Это похоже на С++ головного мозга, а не определение.

EP>Чего шумишь, тебя обидел кто?

Просто это определение годится лишь для одного языка, зачем оно в теме, где речь про другие языки?

DM>>Вот несколько значений, какие из них равны и почему?

EP>Зависит от свойств операций + и *, и связи между ними.

Упростим и допустим, что параметр x имеет тип int32, с привычной арифметикой. Какой будет ответ?
Re[4]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 12:54
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>Справедливости ради, данная реализация ничем не отличается от той, что я привожу на C#. Статические проверки вы библиотеками не добавите. Так что, увы, отсутствуют.

EP>Какие именно статические проверки?


http://www.rsdn.ru/article/funcprog/wrong_intro_FP.xml#EFAAE
Автор(ы): Воронков Василий Владимирович
Дата: 03.04.2013
В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..
Re[5]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 13:15
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Заменить — это значит заменить. Если "х" — чистое, и "x = y", то все "y" можно заменить на "x", и смысл программы от этого не изменится. Теперь представляем, что будет с изменяемыми структурами данных:

ВВ>
ВВ>x = fun --Эквивалентно? Да!
ВВ>


Да не "эквивалентно", а "равно"

ВВ>
ВВ>--Тут мы как-то "поменяли" x
ВВ>--Что дальше? ER работает, да? Можно заменить x на fun?
ВВ>


Это всё понятно. Вот пара примеров:
auto x = sin(pi);
auto y = x;
x = 11111.0;
x = y;
const auto sin_of_pi = x;

Значение sin_of_pi пришло через пару изменяемых переменных, но ER тут спокойно применим, и sin_of_pi можно везде использовать вместо sin(pi).

Далее, иммутабельность/константность для этого вообще не нужна, взять например python:
sin_of_pi = sin(pi) # invariant: sin_of_pi = sin(pi)
# ...
y = some_calc(sin(pi)) # can sin(pi) replace by sin_of_pi

ER никуда не пропал. У нас есть определённые инварианты — если они сломаны, то значит в программе баг, либо сбой в железе/компиляторе/кто-то меняет память (это кстати, может поломать инварианты и в языках с const/immutable).
То что в компиляторе/интерпретаторе нет reinforcing'а определённых инвариантов, никак не превращает функцию sin в impure.
Re[6]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 13:34
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Заменить — это значит заменить. Если "х" — чистое, и "x = y", то все "y" можно заменить на "x", и смысл программы от этого не изменится. Теперь представляем, что будет с изменяемыми структурами данных:

ВВ>>
ВВ>>x = fun --Эквивалентно? Да!
ВВ>>


EP>Да не "эквивалентно", а "равно"


ВВ>>
ВВ>>--Тут мы как-то "поменяли" x
ВВ>>--Что дальше? ER работает, да? Можно заменить x на fun?
ВВ>>


EP>Это всё понятно. Вот пара примеров:


Судя по тому, что вы ниже пишите, не очень понятно.

EP>
EP>auto x = sin(pi);
EP>auto y = x;
EP>x = 11111.0;
EP>x = y;
EP>const auto sin_of_pi = x;
EP>

EP>Значение sin_of_pi пришло через пару изменяемых переменных, но ER тут спокойно применим, и sin_of_pi можно везде использовать вместо sin(pi).

Теперь меняем х на мутабельную структуру данных и смотрим, что осталось от ER.

EP>Далее, иммутабельность/константность для этого вообще не нужна, взять например python:

EP>
EP>sin_of_pi = sin(pi) # invariant: sin_of_pi = sin(pi)
EP># ...
EP>y = some_calc(sin(pi)) # can sin(pi) replace by sin_of_pi
EP>

EP>ER никуда не пропал. У нас есть определённые инварианты — если они сломаны, то значит в программе баг, либо сбой в железе/компиляторе/кто-то меняет память (это кстати, может поломать инварианты и в языках с const/immutable).
EP>То что в компиляторе/интерпретаторе нет reinforcing'а определённых инвариантов, никак не превращает функцию sin в impure.

ER не может пропасть оттуда, где его никогда не было. ER возможен только в чистых языках.
Re[5]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 13:44
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>>>Справедливости ради, данная реализация ничем не отличается от той, что я привожу на C#. Статические проверки вы библиотеками не добавите. Так что, увы, отсутствуют.

EP>>Какие именно статические проверки?
ВВ>http://www.rsdn.ru/article/funcprog/wrong_intro_FP.xml#EFAAE
Автор(ы): Воронков Василий Владимирович
Дата: 03.04.2013
В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..


ВВ>И тут-то начинается самое интересное. Ведь стоит немного задуматься, как понимаешь, что мы в действительности понятия не имеем, экземпляр какого конкретного типа может быть передан в Foo.

Ещё раз, какие именно статические проверки?
В примере с boost::variant:
typedef variant<Cellphone, Laptop> Product;
Product содержит экземпляр либо Cellphone, либо Laptop — всё, больше никаких других типов.
Чтобы добавить новый тип, придётся менять Product. Плюс если в visitor'е нет перегрузки для нового типа (либо catch-all) — то будет ошибка компиляции.
Re[6]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 13:59
Оценка: -1
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>>>Справедливости ради, данная реализация ничем не отличается от той, что я привожу на C#. Статические проверки вы библиотеками не добавите. Так что, увы, отсутствуют.

EP>>>Какие именно статические проверки?
ВВ>>http://www.rsdn.ru/article/funcprog/wrong_intro_FP.xml#EFAAE
Автор(ы): Воронков Василий Владимирович
Дата: 03.04.2013
В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..


EP>

ВВ>>И тут-то начинается самое интересное. Ведь стоит немного задуматься, как понимаешь, что мы в действительности понятия не имеем, экземпляр какого конкретного типа может быть передан в Foo.

EP>Ещё раз, какие именно статические проверки?

Уважаемый! Если уж вы решили комментировать статью, извольте сначала прочитать ее целиком. Там ответ на ваш вопрос содержится. Я давать краткий пересказ в "каментах" я нахожу несколько странным.
Re[7]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 13:59
Оценка: -1 :)
Здравствуйте, Воронков Василий, Вы писали:

EP>>
EP>>auto x = sin(pi);
EP>>auto y = x;
EP>>x = 11111.0;
EP>>x = y;
EP>>const auto sin_of_pi = x;
EP>>

EP>>Значение sin_of_pi пришло через пару изменяемых переменных, но ER тут спокойно применим, и sin_of_pi можно везде использовать вместо sin(pi).
ВВ>Теперь меняем х на мутабельную структуру данных и смотрим, что осталось от ER.

Мутабельлную типа std::vector? Ок:
auto x = iota(2); // pure function, returns std::vector<int>{0, 1}
// (функция iota будет pure, если не считать аллокацию за изменение глобального состояния)
auto y = x;
x = {0, 0, 0, 1, 2, 3, 4, 5};
x = y;
const auto vector_with_0_1 = x;
assert( vector_with_0_1 == iota(2) );


ВВ>ER не может пропасть оттуда, где его никогда не было. ER возможен только в чистых языках.


Какое определение ER предполагается?
Re[7]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 14:08
Оценка: +1 -1 :)
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Уважаемый! Если уж вы решили комментировать статью, извольте сначала прочитать ее целиком. Там ответ на ваш вопрос содержится. Я давать краткий пересказ в "каментах" я нахожу несколько странным.


Уважаемый, я уже потратил время на прочтение этой статьи. Теперь извольте ответить на конкретный вопрос:

ВВ>>>Справедливости ради, данная реализация ничем не отличается от той, что я привожу на C#. Статические проверки вы библиотеками не добавите. Так что, увы, отсутствуют.
EP>>Какие именно статические проверки?

Дело в том, что в реализации C# есть наследование, а в реализации на основе boost::variant нет никакого наследования, типы Cellphone и Laptop вообще никак не связанны, никакого общего предка у них нет — это tagged union в чистом виде — и статических проверок там определённо больше чем в варианте C#.
Re[8]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 14:30
Оценка: -2
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Уважаемый! Если уж вы решили комментировать статью, извольте сначала прочитать ее целиком. Там ответ на ваш вопрос содержится. Я давать краткий пересказ в "каментах" я нахожу несколько странным.

EP>Уважаемый, я уже потратил время на прочтение этой статьи. Теперь извольте ответить на конкретный вопрос:

Уважаемый, я тоже потратил достаточно времени на споры с человеком, который даже не понимает, о чем он спорит.
Почитайте о том, что такое алгебраические типы, как факт их закрытости использует компилятор, а заодно и о том, что такое ER и refential transparency. А пока — DIXI.
Re[9]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 14:50
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

EP>>Теперь извольте ответить на конкретный вопрос:

ВВ>Уважаемый, я тоже потратил достаточно времени на споры с человеком, который даже не понимает, о чем он спорит.

Так всё таки, спрашиваю в четвёртый раз — об отсутствии каких статических проверок в решении на основе boost::variant идёт речь?
Если не знаете, так и скажите, к чему переход на личности?
Re[10]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 29.11.13 15:19
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Так всё таки, спрашиваю в четвёртый раз — об отсутствии каких статических проверок в решении на основе boost::variant идёт речь?


Позволю себе предположить, что не контролируется, как минимум, полнота всех вариантов в каждой точке использования. Т.е. в каждом месте, где мы хотим распаковать алгебраический тип, мы должны явно указать все возможные варианты (конструкторы), иначе ошибка компиляции. Если, соответственно, добавляем в АТД новый конструктор, компилятор сообщает об ошибке во всех местах использования. Если не ошибаюсь, про это все в статье написано.
Re[11]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 15:26
Оценка:
Здравствуйте, AlexRK, Вы писали:

EP>>Так всё таки, спрашиваю в четвёртый раз — об отсутствии каких статических проверок в решении на основе boost::variant идёт речь?

ARK>Позволю себе предположить, что не контролируется, как минимум, полнота всех вариантов в каждой точке использования. Т.е. в каждом месте, где мы хотим распаковать алгебраический тип, мы должны явно указать все возможные варианты (конструкторы), иначе ошибка компиляции. Если, соответственно, добавляем в АТД новый конструктор, компилятор сообщает об ошибке во всех местах использования. Если не ошибаюсь, про это все в статье написано.

Дело в том, что boost::variant обеспечивают такую статическую проверку (выше я уже это упоминал).
Например, если добавить новый продукт, но не изменив visitor, то будет ошибка компиляции:
// ...
typedef variant<Cellphone, Laptop, Desktop> Product;

struct Print: static_visitor<>
{
    void operator()(const Cellphone &x) const
    {
        cout << "Cellphone, touch_screen:" << x.touch_screen << endl;
    }
    void operator()(const Laptop &x) const
    {
        cout << "Laptop, screen_size:" << x.screen_size << endl;
    }
};
// ...

int main()
{
    Cellphone phone = {true};
    Product x = phone;
    apply_visitor(Print(), x); // COMPILE ERROR
}
Re[12]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 29.11.13 15:34
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Дело в том, что boost::variant обеспечивают такую статическую проверку (выше я уже это упоминал).

EP>Например, если добавить новый продукт, но не изменив visitor, то будет ошибка компиляции:

А кроме визитора распаковать вариант никак нельзя? Что-нибудь вроде "if (x is Cellphone)"...
Re[13]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 15:57
Оценка: +1
Здравствуйте, AlexRK, Вы писали:

ARK>А кроме визитора распаковать вариант никак нельзя? Что-нибудь вроде "if (x is Cellphone)"...


Справедливости ради, в нетотальных языках вроде хаскеля есть и функции вроде fromJust и tail, которые не заставляют обрабатывать все варианты, а предполагают один, а если там был другой, то происходит рантайм ошибка. Так что тут в некотором смысле паритет. Вот в языках с проверкой тотальности, типа того же идриса, уже построже проверки.
Re[13]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 15:58
Оценка:
Здравствуйте, AlexRK, Вы писали:

ARK>А кроме визитора распаковать вариант никак нельзя? Что-нибудь вроде "if (x is Cellphone)"...


Там есть x.which() который возвращает номер текущего типа, и есть x.type(), который возвращает std::type_info.
Плюс есть get<T>(x) — если в X находится объект типа T, то он возвращается, иначе кидается исключение, то есть сделать "внешний" switch/if можно.
Но тут два момента:
1. При необходимости, get можно запретить, сделав wrapper на boost::variant, или полностью свой.
2. Ручной if/switch по части возможных типов, означает что мы сознательно делаем для остальных "match all default", а-ля "_".
Re[14]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 16:01
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Вот в языках с проверкой тотальности, типа того же идриса, уже построже проверки.


А есть ли там возможность сматчить только один тип, а для остальных выполнить default?
Re[14]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 29.11.13 16:14
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Там есть x.which() который возвращает номер текущего типа, и есть x.type(), который возвращает std::type_info.

EP>Плюс есть get<T>(x) — если в X находится объект типа T, то он возвращается, иначе кидается исключение, то есть сделать "внешний" switch/if можно.
EP>Но тут два момента:
EP>1. При необходимости, get можно запретить, сделав wrapper на boost::variant, или полностью свой.
EP>2. Ручной if/switch по части возможных типов, означает что мы сознательно делаем для остальных "match all default", а-ля "_".

Понятно. Но как-то вот не покидает ощущение, что это все кривоватая эмуляция. Необходимость создания кучи визиторов (и прокидывать в каждый из них необходимый контекст!), и враппер для защиты. Можно ведь, аналогичным образом рассуждая, эмулировать константы в языке, их не имеющем, путем "соглашения не менять определенные переменные". Однако константы от этого в языке не появляются. В общем, на мой взгляд, не тянет это на "прекрасно реализуется".
Re[14]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 29.11.13 16:16
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Справедливости ради, в нетотальных языках вроде хаскеля есть и функции вроде fromJust и tail, которые не заставляют обрабатывать все варианты, а предполагают один, а если там был другой, то происходит рантайм ошибка. Так что тут в некотором смысле паритет. Вот в языках с проверкой тотальности, типа того же идриса, уже построже проверки.


В таком случае наверное да, все аналогично. У С++ все хуже по части бойлерплейта.
Re[15]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 29.11.13 16:28
Оценка: 7 (1)
Здравствуйте, Evgeny.Panasyuk, Вы писали:

DM>>Вот в языках с проверкой тотальности, типа того же идриса, уже построже проверки.

EP>А есть ли там возможность сматчить только один тип, а для остальных выполнить default?

Для конечных сумм (вроде Maybe, Either и т.п., где число вариантов фиксировано) можно: _. Даже если потом тип изменится, и в сумме появится новый вариант, функция с _ отработает без рантайм ошибок, что и требовалось.
С более хитрыми типами уже не уверен.
Re[15]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 16:40
Оценка: 34 (1)
Здравствуйте, AlexRK, Вы писали:

ARK>Понятно. Но как-то вот не покидает ощущение, что это все кривоватая эмуляция. Необходимость создания кучи визиторов (и прокидывать в каждый из них необходимый контекст!)


Я показал C++1998 код.
В C++11/14 boilerplate при желании убирается:
v.visit
(
    [](Laptop &laptop) { cout << laptop.x; },
    [](Cellphone &phone) { cout << phone.y; },
    [](auto &any) { cout << any.something; }
);


ARK>и враппер для защиты.


Wrapper для защиты и не нужен (а если нужен — пишется один раз) — даже в тех языках где нет match-all-default, всегда можно его сделать вручную:
match_only_laptop(Variant x, Action f, Action default)
{
    match(Laptop) as laptop: f(laptop)
    match(Cellphone) as d : default(d)
    match(Desktop) as d : default(d)
}


ARK>Можно ведь, аналогичным образом рассуждая, эмулировать константы в языке, их не имеющем, путем "соглашения не менять определенные переменные". Однако константы от этого в языке не появляются. В общем, на мой взгляд, не тянет это на "прекрасно реализуется".


Константы дают возможность проверить компилятору некоторые инварианты статически.
boost::variant-like также позволяет проверить делать статические проверки — это не какое-то внешнее соглашение, а разговор на вполне понятном компилятору языке.
Re[16]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 29.11.13 16:57
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Я показал C++1998 код.

EP>В C++11/14 boilerplate при желании убирается:

Да, так лучше. Но визиторов все равно придется писать много, в общем случае по одному на каждый вызов — контекст-то везде разный.

К примеру вот на псевдокоде:

  var foo: Integer := ...
  var bar: String := ...

  case variant

    when CellPhone then
      print("Phone count: ", foo + 3);

    when Laptop then
      print(bar, variant.x);

  end;


Мы же можем использовать при паттерн-матчинге и локальные переменные, и параметры метода, и поля класса. Все это добро придется передавать в визиторы.
Re[17]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 17:04
Оценка: +1
Здравствуйте, AlexRK, Вы писали:

EP>>Я показал C++1998 код.

EP>>В C++11/14 boilerplate при желании убирается:

ARK>Да, так лучше. Но визиторов все равно придется писать много, в общем случае по одному на каждый вызов — контекст-то везде разный.


Так и matcher'ы будут на каждый вызов

ARK>К примеру вот на псевдокоде:

ARK>
ARK>  var foo: Integer := ...
ARK>  var bar: String := ...

ARK>  case variant

ARK>    when CellPhone then
ARK>      print("Phone count: ", foo + 3);

ARK>    when Laptop then
ARK>      print(bar, variant.x);

ARK>  end;
ARK>

ARK>Мы же можем использовать при паттерн-матчинге и локальные переменные, и параметры метода, и поля класса. Все это добро придется передавать в визиторы.

Тут нет проблемы, лямбды умеют захватывать контекст:
int foo;
string bar;
v.visit
(
    [&](Cellphone &phone) { cout << "Phone count: " << (foo + 3); },
    [&](Laptop &laptop) { cout << bar << laptop.x; }
);
Re[18]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 29.11.13 17:12
Оценка:
Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Тут нет проблемы, лямбды умеют захватывать контекст:


А! Понял. Не увидел сразу, что там вызов, а не объявление класса. Да, последний вариант, похоже, является полной аналогией с АТД.
Re[19]: Неправильное введение в функциональное программирование
От: Evgeny.Panasyuk Россия  
Дата: 29.11.13 17:17
Оценка:
Здравствуйте, AlexRK, Вы писали:

EP>>Тут нет проблемы, лямбды умеют захватывать контекст:

ARK>А! Понял. Не увидел сразу, что там вызов, а не объявление класса. Да, последний вариант, похоже, является полной аналогией с АТД.

Да. (не считая, как заметил D. Mon, pattern-matching'а — но он и не обсуждался в статье)
Re[20]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 18:18
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Просто у тебя один вид значений отличался от другого тэгом Some, а здесь для них заведены тэги Nbr и Fn, смысл тот же абсолютно.


Ну, правильно, ты поменял код и устранил зависимость от рантайм значений. И что ты хотел этим доказать? Понятно, что аналогичную программу можно написать на любом языке. Она приводилась в качестве примера реализации.
Re[20]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 18:27
Оценка: -1
Здравствуйте, D. Mon, Вы писали:

DM>Звучит как немерлизм, ни в одном нормальном языке такого нет (чтобы именно первого). Формально это ересь, тип функции тут указан уже при определении, а потом лишь используется. Но если речь просто про полиморфизм, то да, тут одна из его форм, параметризованный тип.


Никакой это не немерлизм. Это, может, в OCaml не так, где не потрудились ХМ допилить. А в языках с полиморфными операторами ты даже функцию "sum x y =x+y" иначе не типизируешь. Ибо какой у нее тип?

ВВ>>Здесь нет зависимости от рантайм значений, ведь эта программа доказывается статически. "Доказывается статически" означает, что возможный диапазон значений нам известен в компайл тайм, и мы можем доказать, что ни при каких случаях не выйдем из этого диапазона. Откуда здесь взяться зависимости от рантайма? Тут ее нет


DM>Ну что значит нет? Значение v тут один раз создается и передается. Какого оно типа? Зависит от того, как мы программу запустили, что ей передали. Это и есть зависимость от рантайма в чистом виде, а не твои странные определения.


Ну да.

x = 2


Это тоже рантайм значение. Вот только известно оно в компайл-тайме.
Повторяю — зависимость от рантайм-значений означает зависимость от значений, которые *известны* только в рантайме.

ВВ>>"Зависимость от рантайм-значений" означает "Зависимость от значений, который становятся *известны* только в рантайме".

DM>Ровно так и есть же в этом примере. Есть зависимость типа от булевого значения, истина там или ложь — будет известно только в рантайме.

Диапазон значений известен в компайл, соответственно, всё просчитывается статически.

BB>>А для того, чтобы программа была доказуема статически, ее нужно свести к набору значений, который известен уже в период компиляции. Никаких "нежданчиков" там быть не может. Так что это, мягко говоря, не одно и то же


DM>Да, "набор" значений должен быть известен статически, но он может быть бесконечным. В примере выше, где список читался извне, тип функции зависел от длины списка, который мог быть сколь угодно длинным (если закрыть глаза на технические ограничения ОС). Т.е. в зависимости от переданных данных могло получиться значение типа


Там была зависимость от длины списка. Для доказательства корректности достаточно было того, чтобы длина была длиной именно списка, что компилятор прекрасно видел в коде "length xs" и "fun xs".

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


Статическая типизация устраняет не баги, а все, что не может просчитать статически. Любую ситуацию с "нежданчиком" можно обработать — на основе данных, которые становятся доступны только в рантайме. Не говоря уж о том, что на практике любая система типов имеет свои ограничения и может не пропускать корректный код просто потому что не способна его доказать.
Re[21]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 29.11.13 18:55
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Никакой это не немерлизм. Это, может, в OCaml не так, где не потрудились ХМ допилить. А в языках с полиморфными операторами ты даже функцию "sum x y =x+y" иначе не типизируешь. Ибо какой у нее тип?


над a определен (+) => a -> a -> a


ВВ>Любую ситуацию с "нежданчиком" можно обработать — на основе данных, которые становятся доступны только в рантайме.


Ну так, упрощенно говоря, код, обрабатывающий "нежданчик" — и есть доказательство для теоремы, заданной в сигнатуре типа. Вот компилятор и проверяет обрабатываются ли все "нежданчики". А если такого кода нет — это баг.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[22]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 19:14
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>Никакой это не немерлизм. Это, может, в OCaml не так, где не потрудились ХМ допилить. А в языках с полиморфными операторами ты даже функцию "sum x y =x+y" иначе не типизируешь. Ибо какой у нее тип?

K>
K>над a определен (+) => a -> a -> a
K>


А что такое "а"? С чего ты решил, что функция полиморфная?

> let sum x y = x+y
sum "Hello," "there!";;

val sum : x:string -> y:string -> string
val it : string = "Hello,there!"

> let sum x y = x+y
sum 1 2;;

val sum : x:int -> y:int -> int
val it : int = 3


Да и, собственно, если даже она полиморфная, ее все равно компилировать как-то надо — хотя это уже другой вопрос.

Но на всякий случай повторюсь, чтобы не раздувать лишний флейм — речь шла о том, что "типизация по месту" это прямь какая-то кривь и немерлизм. Однако нет. Нормальная практика.

ВВ>>Любую ситуацию с "нежданчиком" можно обработать — на основе данных, которые становятся доступны только в рантайме.

K>Ну так, упрощенно говоря, код, обрабатывающий "нежданчик" — и есть доказательство для теоремы, заданной в сигнатуре типа. Вот компилятор и проверяет обрабатываются ли все "нежданчики". А если такого кода нет — это баг.

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

Или я не прав и круче зависимых типов только яйца?
Re[21]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 29.11.13 20:32
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>
ВВ>x = 2
ВВ>


ВВ>Это тоже рантайм значение. Вот только известно оно в компайл-тайме.

ВВ>Повторяю — зависимость от рантайм-значений означает зависимость от значений, которые *известны* только в рантайме.

  args <- getArgs          -- читаем аргументы командной строки, рантайм значение
  let p = length args > 1


Вы не видите разницы? p — рантайм значение.
Ну и, просто повторите этот код на любом другом языке программирования.
Re[22]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 29.11.13 21:04
Оценка: :)
Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>
ВВ>>x = 2
ВВ>>


ВВ>>Это тоже рантайм значение. Вот только известно оно в компайл-тайме.

ВВ>>Повторяю — зависимость от рантайм-значений означает зависимость от значений, которые *известны* только в рантайме.

VE>
VE>  args <- getArgs          -- читаем аргументы командной строки, рантайм значение
VE>  let p = length args > 1
VE>


VE>Вы не видите разницы? p — рантайм значение.

VE>Ну и, просто повторите этот код на любом другом языке программирования.

У p всего два возможных значения, оба известны в компайл и зависимости от рантайма тут нет.
Re: Неправильное введение в функциональное программирование
От: Ikemefula Беларусь http://blogs.rsdn.org/ikemefula
Дата: 29.11.13 21:33
Оценка:
Здравствуйте, Воронков Василий Владимирович, Вы писали:

ВВВ>Аннотация:

ВВВ>В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..


Func<int,int> sum(int x)
{
    return z => y => x + y + z;
}


Вот это не палит. Сигнатура должна быть Func<int, Func<int, int>>
Re: Неправильное введение в функциональное программирование
От: Ikemefula Беларусь http://blogs.rsdn.org/ikemefula
Дата: 29.11.13 21:48
Оценка: +1 :)
Здравствуйте, Воронков Василий Владимирович, Вы писали:

ВВВ>Аннотация:

ВВВ>В данном введении я не буду рассказывать об истории функциональных языков программирования. Я не буду писать о лямбда исчислении и комбинаторике. Я даже не буду убеждать читателя в том, что функциональное программирование – это полезно и важно. Наверняка вы уже неоднократно обо всем этом читали. У меня в данном случае несколько иная задача. Я постараюсь действительно ответить на некоторые вопросы, которые могли остаться у вас после прочтения других «введений». Это, конечно, не слишком соответствует традициям – отсюда и подобное название у этой статьи..

Не совсем ясно, почему статья называется "неправильное введение", если у ней отличие от других материалов около нуля. Вопросы которые остаются после книг по ФП обычно навроде "для чего", "где подвох" и "как контролировать память и перформанс"
А у тебя как то скучно — "что это такое" только галопом по европам.
Re[23]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 29.11.13 22:10
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>У p всего два возможных значения, оба известны в компайл и зависимости от рантайма тут нет.


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

myType : Nat -> Type
myType Z = Int
myType (S x) = List (myType x)

create : (n:Nat) -> myType n
create Z = 0
create (S x) = [create x]

useValue : (n:Nat) -> myType n -> String
useValue Z v = show v
useValue (S x) v = concat $ map (useValue x) v

main : IO ()
main = do
  ns <- getLine
  let n = cast ns
  putStrLn $ useValue n (create n)
Re[24]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 06:12
Оценка:
Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>У p всего два возможных значения, оба известны в компайл и зависимости от рантайма тут нет.


VE>Неплохо бы посмотреть исходный код на другом языке.


На каком?

VE>Ну и можно попросить D.Mon (так как у меня идрис не стоит, а под Windows я не собрал, и не уверен, что получится) проверить код для такого случая:


VE>
VE>myType : Nat -> Type
VE>myType Z = Int
VE>myType (S x) = List (myType x)

VE>create : (n:Nat) -> myType n
VE>create Z = 0
VE>create (S x) = [create x]

VE>useValue : (n:Nat) -> myType n -> String
VE>useValue Z v = show v
VE>useValue (S x) v = concat $ map (useValue x) v

VE>main : IO ()
VE>main = do
VE>  ns <- getLine
VE>  let n = cast ns
VE>  putStrLn $ useValue n (create n)
VE>


А вы сами можете доказать корректность этой программы "статически"?
Re[21]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 07:18
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

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


Какую еще зависимость? Примера реализации чего?
Я перевел твою программу дословно. В ней ровно столько зависимости от рантайм значений, сколько в оригинале. Если в статически типизированной версии такой зависимости не усматривается, это лишь потому, что ее не было в исходном варианте.
Re[21]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 07:38
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>>>Функция типизируется в момент первого применения.

DM>>Звучит как немерлизм, ни в одном нормальном языке такого нет (чтобы именно первого).

ВВ>Никакой это не немерлизм. Это, может, в OCaml не так, где не потрудились ХМ допилить. А в языках с полиморфными операторами ты даже функцию "sum x y =x+y" иначе не типизируешь. Ибо какой у нее тип?


Ну, дядь, ты сейчас говоришь как человек, который хаскеля и других ФЯ в глаза не видел.
Prelude> let sum x y = x + y
Prelude> :t sum
sum :: Num a => a -> a -> a

Вот такой у нее тип.
А теперь покажи языки, где "Функция типизируется в момент первого применения". Я подобное встречал лишь в контексте немерле, и то не уверен.

DM>>Ну что значит нет? Значение v тут один раз создается и передается. Какого оно типа? Зависит от того, как мы программу запустили, что ей передали. Это и есть зависимость от рантайма в чистом виде, а не твои странные определения.


ВВ>Ну да.

ВВ>x = 2
ВВ>Это тоже рантайм значение. Вот только известно оно в компайл-тайме.
ВВ>Повторяю — зависимость от рантайм-значений означает зависимость от значений, которые *известны* только в рантайме.

Я тоже повторяю, в моем примере значения именно такие. Они *известны* только в рантайме. Вовсе не как в "x=2".
Давай еще 10 раз повторим, для закрепления.

ВВ>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.


Да. Но сами конкретные значения не известны, в этом вся суть.

ВВ>Там была зависимость от длины списка. Для доказательства корректности достаточно было того, чтобы длина была длиной именно списка, что компилятор прекрасно видел в коде "length xs" и "fun xs".


Все правильно.
Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!

ВВ>Статическая типизация устраняет не баги, а все, что не может просчитать статически. Любую ситуацию с "нежданчиком" можно обработать — на основе данных, которые становятся доступны только в рантайме.


Если этой обработки в коде нет, то будет рантайм ошибка, т.е. это именно баг.
А если такая обработка есть, то значит ты заранее приготовился к тому, что данные могут быть какие-то не такие. Это уже отлично описывается статическими типами и проверяется при компиляции.

ВВ>Не говоря уж о том, что на практике любая система типов имеет свои ограничения и может не пропускать корректный код просто потому что не способна его доказать.


На практике с хорошей системой типов придумать такой код очень сложно. Тебе вот не удалось пока.
Знаешь, что сейчас происходит в математике последние несколько лет? Ее основания и весь фундамент переписывают на Coq и Agda, языках с зависимыми типами, потому что оказалось, что эти системы типов и есть фундамент математики, намного адекватнее теории множеств (которая там как частный случай выводится). Если о программе можно как-то рационально рассуждать, то эти рассуждения можно выразить в тех типах.
http://homotopytypetheory.org/
Единственный минус — пока это довольно сложно делать.
Re[23]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 07:46
Оценка: -1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Но на всякий случай повторюсь, чтобы не раздувать лишний флейм — речь шла о том, что "типизация по месту" это прямь какая-то кривь и немерлизм. Однако нет. Нормальная практика.


Не, одно дело уточнение типа вызова функции, и совсем другое — сама "функция типизируется в момент первого применения". Вторая фраза предполагает, что до первого применения у функции нет типа, а во время второго применения ее тип уже определен первым. Это полная ересь в ЯП с полиморфизмом.

ВВ>Или я не прав и круче зависимых типов только яйца?


Да, вывод именно такой, конечно.
Хотя исходный посыл был скромнее: то, что выглядит "невозможным" для одних статически типизированных языков, еще не обязятально невозможно для статической типизации как таковой, и со всеми предложенными в статье и обсуждении задачами языки вроде Идриса могут справиться статически.
Re[24]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 08:03
Оценка:
Здравствуйте, VoidEx, Вы писали:

VE>Ну и можно попросить D.Mon (так как у меня идрис не стоит, а под Windows я не собрал, и не уверен, что получится) проверить код для такого случая:


В твоем варианте на выходе всегда одно и то же, т.к. все вложенные списки просто разворачиваются, не меняя строки. Я добавил вывод скобок, чтобы была видна вложенность. И еще один cast добавил, т.к. прямого из String в Nat не было.

... -- myType и create как в оригинале
useValue : (n:Nat) -> myType n -> String
useValue Z v = show v
useValue (S x) v = "[" ++ (concat $  map (useValue x) v) ++ "]"

main : IO ()
main = do
  ns <- getLine
  let n = cast . cast $ ns
  putStrLn $ useValue n (create n)


Компиляем, запускаем:
C:\prog\idris>idris nlist.idr -o nlist.exe

C:\prog\idris>nlist
1
[0]

C:\prog\idris>nlist
0
0

C:\prog\idris>nlist
4
[[[[0]]]]

C:\prog\idris>nlist
42
[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[0]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

Имеем значение типа List List List .... Int, где число вложенностей зависит от введенного рантайм значения.

В винде если есть MinGW и Haskell Platform, сборка Идриса последней версии (0.9.10) должна быть не шибко сложнее
cabal install idris
Раньше зависимостей было больше, сейчас некоторые из них сделали опциональными.
Разве что пара сишных либ вроде gmp и pthreads может еще требоваться, он они в MinGW легко добавляются.
Re[25]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 09:09
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

VE>>Ну и можно попросить D.Mon (так как у меня идрис не стоит, а под Windows я не собрал, и не уверен, что получится) проверить код для такого случая:


VE>>
VE>>myType : Nat -> Type
VE>>myType Z = Int
VE>>myType (S x) = List (myType x)

VE>>create : (n:Nat) -> myType n
VE>>create Z = 0
VE>>create (S x) = [create x]

VE>>useValue : (n:Nat) -> myType n -> String
VE>>useValue Z v = show v
VE>>useValue (S x) v = concat $ map (useValue x) v

VE>>main : IO ()
VE>>main = do
VE>>  ns <- getLine
VE>>  let n = cast ns
VE>>  putStrLn $ useValue n (create n)
VE>>


ВВ>А вы сами можете доказать корректность этой программы "статически"?


Конечно. Вы и сами можете пройтись по всем вариантам. Не понимаю, чем вам не нравится bool, но устраивает Nat, у которого тоже два варианта: 0 или (1 + n), правда порождают они бесконечное кол-во вариантов, ну и что.
Re[22]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 09:45
Оценка:
Здравствуйте, D. Mon, Вы писали:

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

DM>Какую еще зависимость? Примера реализации чего?
DM>Я перевел твою программу дословно. В ней ровно столько зависимости от рантайм значений, сколько в оригинале. Если в статически типизированной версии такой зависимости не усматривается, это лишь потому, что ее не было в исходном варианте.

Ну зачем же обманывать? Моя программа работает корректно благодаря рантайм проверке типа, ты, конечно же, ее устранил, но теперь оказывается, что программа была переведена "дословно". Это нормальный подход к дискуссии для тебя?
Re[25]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 09:49
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>В винде если есть MinGW и Haskell Platform, сборка Идриса последней версии (0.9.10) должна быть не шибко сложнее


Haskell Platform не канонично. Haskell у меня, конечно есть.

DM>cabal install idris

DM>Раньше зависимостей было больше, сейчас некоторые из них сделали опциональными.
DM>Разве что пара сишных либ вроде gmp и pthreads может еще требоваться, он они в MinGW легко добавляются.

Не хватало make, после установки через Cygwin cabal install idris собрало idris.exe и кучу .idr файлов, но затем рухнуло на:

cc -fPIC -O2 -Wall -I/usr/local/include -c -o idris_rts.o idris_rts.c
process_begin: CreateProcess(NULL, cc -dumpmachine, ...) failed.
process_begin: CreateProcess(NULL, cc -fPIC -O2 -Wall -I/usr/local/include -c -o idris_rts.o idris_rts.c, ...) failed.
make (e=2): ▒▒ ▒▒▒▒▒▒▒ ▒▒▒▒▒ ▒▒▒▒▒▒▒▒▒ ▒▒▒▒.
make: *** [idris_rts.o] ▒▒▒▒▒▒ 2

Положил idris.exe в libs/prelude, интерпретатор запускается. Но что-то там явно не доделало, скомпилировать простой пример не удается.

C:\Users\Alexandr\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\idris-0.9.10\rts\idris_main.c: openFile: does not exist (No such file or directory)
Re[22]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 09:59
Оценка: -1
Здравствуйте, D. Mon, Вы писали:

DM>Ну, дядь, ты сейчас говоришь как человек, который хаскеля и других ФЯ в глаза не видел.

DM>
DM>Prelude> let sum x y = x + y
DM>Prelude> :t sum
DM>sum :: Num a => a -> a -> a
DM>

DM>Вот такой у нее тип.
DM>А теперь покажи языки, где "Функция типизируется в момент первого применения". Я подобное встречал лишь в контексте немерле, и то не уверен.

Да нет, сынок, это ты сейчас говоришь как человек, который "других ФЯ" в глаза не видел. Причем довольно известных. Например, F#.

DM>>>Ну что значит нет? Значение v тут один раз создается и передается. Какого оно типа? Зависит от того, как мы программу запустили, что ей передали. Это и есть зависимость от рантайма в чистом виде, а не твои странные определения.


ВВ>>Ну да.

ВВ>>x = 2
ВВ>>Это тоже рантайм значение. Вот только известно оно в компайл-тайме.
ВВ>>Повторяю — зависимость от рантайм-значений означает зависимость от значений, которые *известны* только в рантайме.

DM>Я тоже повторяю, в моем примере значения именно такие. Они *известны* только в рантайме. Вовсе не как в "x=2".

DM>Давай еще 10 раз повторим, для закрепления.

Да повторяй хоть сотни раз. В твоей трактовке сам термин "зависимость от рантайм-значений" теряет всякий смысл. Я уже множество раз, разными словами, пытался объяснить, какой смысл я вкладываю в это утверждение. Мы зависим от рантайма только в том случае, когда не можем рассуждать о возможных значениях статически. Если диапазон нам известен, то все зависимости от рантайма снимаются; нам ведь известно все множество инвариантов, и рантайм тут не привнесет ничего нового.

ВВ>>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.

DM>Да. Но сами конкретные значения не известны, в этом вся суть.

Вообще-то если конкретные значения известны, то обычно и само вычисление не требуется.

ВВ>>Там была зависимость от длины списка. Для доказательства корректности достаточно было того, чтобы длина была длиной именно списка, что компилятор прекрасно видел в коде "length xs" и "fun xs".

DM>Все правильно.
DM>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!

Можно подумать, это и правда было для тебя сюрпризом, судя по тому, с каким жаром ты сейчас об этом рассуждаешь.

ВВ>>Статическая типизация устраняет не баги, а все, что не может просчитать статически. Любую ситуацию с "нежданчиком" можно обработать — на основе данных, которые становятся доступны только в рантайме.


DM>Если этой обработки в коде нет, то будет рантайм ошибка, т.е. это именно баг.

DM>А если такая обработка есть, то значит ты заранее приготовился к тому, что данные могут быть какие-то не такие. Это уже отлично описывается статическими типами и проверяется при компиляции.

Обработка означает, что код *может* работать неправильно, мы допускаем это и пишем другой код, который обрабатывает данную ситуацию. Т.е. мы не задаемся вопросом "при каких значениях этот код будет работать?"; у нас другой вопрос — "что делать, когда код не работает?"

ВВ>>Не говоря уж о том, что на практике любая система типов имеет свои ограничения и может не пропускать корректный код просто потому что не способна его доказать.

DM>На практике с хорошей системой типов придумать такой код очень сложно. Тебе вот не удалось пока.

Ой, ладно. Как раз *на практике* "хорошие системы типов" падают там и сям. Кстати, мне кажется, что человеку, который знает Идрис понять паттерны, при которых его система типов будет обламываться, должно быть не очень сложно
А я Идрис не знаю; все, что я могу в данном случае — тыкаться вслепую, пытаясь понять, где его интеллектуальность закончится.
Нет, я могу конечно, приводить более практичные примеры, чем fun. Но ты сам готов переписывать несколько килобайт кода с динамики?

DM>Знаешь, что сейчас происходит в математике последние несколько лет? Ее основания и весь фундамент переписывают на Coq и Agda, языках с зависимыми типами, потому что оказалось, что эти системы типов и есть фундамент математики, намного адекватнее теории множеств (которая там как частный случай выводится). Если о программе можно как-то рационально рассуждать, то эти рассуждения можно выразить в тех типах.

DM>http://homotopytypetheory.org/
DM>Единственный минус — пока это довольно сложно делать.

Это, конечно, хорошо; вопрос, как это все относится к обсуждаемому вопросу.
Re[24]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 10:09
Оценка: -1
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Но на всякий случай повторюсь, чтобы не раздувать лишний флейм — речь шла о том, что "типизация по месту" это прямь какая-то кривь и немерлизм. Однако нет. Нормальная практика.

DM>Не, одно дело уточнение типа вызова функции, и совсем другое — сама "функция типизируется в момент первого применения".

У тебя есть какая проблема с самим термином, который я использовал — "отложенная типизация"? Даже если его и ввел Москаль — то, что? Применим он далеко не только к Немерле. И хорошо подходит далеко не только для Немерле.

DM>Вторая фраза предполагает, что до первого применения у функции нет типа, а во время второго применения ее тип уже определен первым. Это полная ересь в ЯП с полиморфизмом.


Вторая фраза предполагает, что до первого применения типизация функции не завершена. На самом деле совершенно неважно, произведена ли типизация до этого частично или же вообще не произведена. Пока у тебя тип функции выглядит как "хз_что->хз_что->хз_что", скомпилирована она не будет.
А полная ересь — рассуждать обо всех языках на основе каких-то конкретных.
Вот F# (заметь, не Немерле) "во время второго применения тип функции уже определен первым":

> let sum x y = x+y
let x = sum 2 3
let y = sum "one," "two";;

  let y = sum "one," "two";;
  ------------^^^^^^

stdin(3,13): error FS0001: В данном выражении требовалось наличие типа
    int    
, но получен тип
    string


и соответственно:

> let sum x y = x+y
sum "One," "Two"
sum 1 2;;

  sum 1 2;;
  ----^

stdin(3,5): error FS0001: В данном выражении требовалось наличие типа
    string    
, но получен тип
    int


Наверное, все потому что F# "не относится" к "ЯП с полиморфизмом"

Теперь вернемся к нашим баранам. То, что происходит в Идрисе — это по сути доказательство функции по месту ее первого применения. Вот только доказательство по сути и является частью типизации.

ВВ>>Или я не прав и круче зависимых типов только яйца?


DM>Да, вывод именно такой, конечно.

DM>Хотя исходный посыл был скромнее: то, что выглядит "невозможным" для одних статически типизированных языков, еще не обязятально невозможно для статической типизации как таковой, и со всеми предложенными в статье и обсуждении задачами языки вроде Идриса могут справиться статически.
Re[22]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 11:31
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>На практике с хорошей системой типов придумать такой код очень сложно. Тебе вот не удалось пока.


Давай даже так. Я, как говорится, не настаиваю, но вдруг тебе делать будет нечего — или самому захочется проверить. Есть задача, воспроизвести некую библиотеку на Ela, которая позволяет писать следующее:

open espec

test1 =
  test "With list"
  given [1]
    when (++) [2]
    should be [1,2]
    when tail
    shouldn't be [1,2]
    should be [2]

test2 = 
  test "With int"
  given 4
    when (+) 5
    should be 9
    when negate
    should be -9
    when (+) 13
    should be 4

[] 
  |> addTest test1
  |> addTest test2
  |> run
  |> formatResult


Вывод:

Test session started.

Test "With list" (failed 0, errors 0):
  given [1]
    when (++) [2] -> [1,2]
    should be [1,2] -> success
    when tail -> [2]
    shouldn't be [1,2] -> success
    should be [2] -> success

Test "With int" (failed 0, errors 0):
  given 4
    when (+) 5 -> 9
    should be 9 -> success
    when negate -> -9
    should be -9 -> success
    when (+) 13 -> 4
    should be 4 -> success

Total tests:2 Failed: 0


Кстати, этот код можно даже исполнить в онлайн-репле.

Я готов пойти на некоторые уступки — в частности, если будут проблемы с красивым выводом. Но общий смысл подхода (и желательно — синтаксис) должен сохраниться.
У нас есть функция test, которая принимает все подряд — т.е. внутри спецификации теста на самом деле одна апликация. Данная функция ничего не исполняет, а формирует некое дерево, как бы AST нашего DSL-я. Работать она может при этом с любыми значениями. У DSL-я есть определенная грамматика — для простоты пусть она будет ограничена тем что и как приводится в примерах. Сначала идет given, после него значение, а после этого либо трансформация значения (when), либо ассерты (should be, shouldn't be). Заметь при этом, что "трансформатор" when может принимать любое кол-во аргументов — корректно и "when negate" и "when (+) 2" — требуемое кол-во аргументов определяется динамически. Ну и соответственно длина конкретного теста может быть любой.

После того как наш AST сформирован, он может быть интерпретирован через функцию run. Функция возвращает структуру данных, описывающую результат. Ну, далее понимаешь.
Могу привести реализацию модуля espec на Ela, если это нужно.
Re[22]: Неправильное введение в функциональное программирование
От: AlexRK  
Дата: 30.11.13 11:48
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>>>Ну что значит нет? Значение v тут один раз создается и передается. Какого оно типа? Зависит от того, как мы программу запустили, что ей передали. Это и есть зависимость от рантайма в чистом виде, а не твои странные определения.

ВВ>>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.
DM>Да. Но сами конкретные значения не известны, в этом вся суть.
DM>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!

На мой взгляд, спор по сути терминологический. Вот взять, к примеру, диапазоны в Ада:

  type Range_Type is range -5 .. 10;


Вроде как не зависимый тип, но по сути то же самое. Достаточно мощный решатель может статически проверить соответствие рангу, в том числе с помощью предусловий-постусловий.

В зависимых типах мы точно также везде имеем дело с некоторым "набором допустимых значений", а в том месте, где этот набор схлопывается в конкретное значение — надо ставить if или аналог.
Re[25]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 12:09
Оценка: -1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Здравствуйте, D. Mon, Вы писали:


ВВ>У тебя есть какая проблема с самим термином, который я использовал — "отложенная типизация"? Даже если его и ввел Москаль — то, что? Применим он далеко не только к Немерле. И хорошо подходит далеко не только для Немерле.


Да, потому что типизируется всё сразу. "Отложенная типизация", это def x = Foo(), а потом по ходу кода уже видно, какой именно Foo, Foo[Int] или какой-то ещё.
Здесь типизация выводится сразу после объявления.
Re[25]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 12:11
Оценка: -1 :)
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Вторая фраза предполагает, что до первого применения типизация функции не завершена. На самом деле совершенно неважно, произведена ли типизация до этого частично или же вообще не произведена. Пока у тебя тип функции выглядит как "хз_что->хз_что->хз_что", скомпилирована она не будет.


Не несите такой откровенной ерунды.

module Test (foo) where
foo x = x


Компилируется. Функция там одна, работает отлично. Разберитесь уже наконец в вопросе.
Re[25]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 12:12
Оценка: -1 :)
Здравствуйте, Воронков Василий, Вы писали:
ВВ>
>> let sum x y = x+y
ВВ>let x = sum 2 3
ВВ>let y = sum "one," "two";;

ВВ>  let y = sum "one," "two";;
ВВ>  ------------^^^^^^

ВВ>stdin(3,13): error FS0001: В данном выражении требовалось наличие типа
ВВ>    int    
ВВ>, но получен тип
ВВ>    string  
ВВ>


ВВ>и соответственно:


ВВ>
>> let sum x y = x+y
ВВ>sum "One," "Two"
ВВ>sum 1 2;;

ВВ>  sum 1 2;;
ВВ>  ----^

ВВ>stdin(3,5): error FS0001: В данном выражении требовалось наличие типа
ВВ>    string    
ВВ>, но получен тип
ВВ>    int    
ВВ>


ВВ>Наверное, все потому что F# "не относится" к "ЯП с полиморфизмом"


А теперь то же самое в Haskell попробуйте. Попробуйте-попробуйте.
Re[26]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 12:17
Оценка:
Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Вторая фраза предполагает, что до первого применения типизация функции не завершена. На самом деле совершенно неважно, произведена ли типизация до этого частично или же вообще не произведена. Пока у тебя тип функции выглядит как "хз_что->хз_что->хз_что", скомпилирована она не будет.


VE>Не несите такой откровенной ерунды.


VE>
VE>module Test (foo) where
VE>foo x = x
VE>


VE>Компилируется. Функция там одна, работает отлично. Разберитесь уже наконец в вопросе.


Разобраться в вопросе нужно вам. F#, когда тип функции невозможно вывести из применения, либо делает ее полиморфной, либо вообще использует политику "default int":


> let sum x y =x+y;;

val sum : x:int -> y:int -> int


Что как бы не исключает вышесказанного. Хаскелл, о котором в процитированном вами сообщении, речи вообще не шло, по умолчанию делает все функции полиморфными.
Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?
Re[26]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 12:19
Оценка:
Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>
>>> let sum x y = x+y
ВВ>>let x = sum 2 3
ВВ>>let y = sum "one," "two";;

ВВ>>  let y = sum "one," "two";;
ВВ>>  ------------^^^^^^

ВВ>>stdin(3,13): error FS0001: В данном выражении требовалось наличие типа
ВВ>>    int    
ВВ>>, но получен тип
ВВ>>    string  
ВВ>>


ВВ>>и соответственно:


ВВ>>
>>> let sum x y = x+y
ВВ>>sum "One," "Two"
ВВ>>sum 1 2;;

ВВ>>  sum 1 2;;
ВВ>>  ----^

ВВ>>stdin(3,5): error FS0001: В данном выражении требовалось наличие типа
ВВ>>    string    
ВВ>>, но получен тип
ВВ>>    int    
ВВ>>


ВВ>>Наверное, все потому что F# "не относится" к "ЯП с полиморфизмом"


VE>А теперь то же самое в Haskell попробуйте. Попробуйте-попробуйте.


Товарищ, вы вообще не въезжаете, о чем речь или просто покривляться любите? Я довольно хорошо знаю Хаскелл, но при этом совершенно не понимаю, причем тут Хаскелл, когда речь идет о том, что в *некоторых* языках (а не только в Немерле) используется отложенная типизация функций.
Re[27]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 12:23
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Что как бы не исключает вышесказанного. Хаскелл, о котором в процитированном вами сообщении, речи вообще не шло, по умолчанию делает все функции полиморфными.

ВВ>Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?

Я вам немножко напомню, что речь была об Idris и ваших словах, что это благодаря "отложенной типизации". Вам уже 2 человека говорят, что это не так.

Ну да, легко. Отложенная типизация в действии =)

Re[26]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 30.11.13 12:28
Оценка: +1
Здравствуйте, VoidEx, Вы писали:

VE>А теперь то же самое в Haskell попробуйте. Попробуйте-попробуйте.


Тут под "типизацией по первому применению" подразумевается defaulting/disambiguation которые работают в случае monomorphism/value restriction
Соответственно:

Prelude> sum = \a b -> a + b
sum :: Integer -> Integer -> Integer
Prelude> sum a b = a + b
sum :: Num a => a -> a -> a
Prelude> let sum = \a b -> a + b in sum 2.0 40
42.0
it :: Double


Эффект в F# получается потому, что это, по факту, два языка с разными системами типов. И при переходе из одного в другой работает ограничение на полиморфизм. Соответственно, если оставаться в языке inline-функций типизация пройдет иначе:

> let inline sum x y = x+y;;

val inline sum :
  x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( + ) :  ^a *  ^b ->  ^c)

> let x = sum 2 3;;

val x : int = 5

> let y = sum "one," "two";;

val y : string = "one,two"

> let sum x y = x+y;;

val sum : x:int -> y:int -> int

Легко видеть, что функция типизируется вовсе не по первому применению. И может и обязательно будет типизирована при определении и вовсе без всякого применения.
Ну и в немерле никакой "типизации по месту применения" нет там просто всегда выводится конкретный тип, т.е. ограничение на полиморфизм сильнее чем в хаскеле и даже сильнее велью-рестрикшн в эмэлях.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[28]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 12:31
Оценка:
Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Что как бы не исключает вышесказанного. Хаскелл, о котором в процитированном вами сообщении, речи вообще не шло, по умолчанию делает все функции полиморфными.

ВВ>>Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?

VE>Я вам немножко напомню, что речь была об Idris и ваших словах, что это благодаря "отложенной типизации". Вам уже 2 человека говорят, что это не так.

VE>

VE>Ну да, легко. Отложенная типизация в действии =)


По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации. Компилятору-таки нужно понять, что в принципе может вернуть функция и способен ли клиентский код это отработать. Так что, условно говоря, если в динамике мы имеем "List->хз_что", причем вместо "хз_что" может быть Foo или Bar, то в Идрисе будет "List->Foo|Bar", и нам требуется сначала доказать, что ничего другого быть не может.

Причем не столь и важно, как это называть. Называйте "доказательством из применения". Просто, видимо, некоторые термины, получившие популяризацию благодаря Москалю, действуют тут как красная тряпка на быка.

А вот спор уже начался на тему "отложенная типизация в языках, поддерживающих полиморфные функции есть а) немерлизм, б) полная ересь". Что как бы не совсем корректно. Кстати, интересно одно теперь приравнивается ко второму?
Re[27]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 12:39
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Легко видеть, что функция типизируется вовсе не по первому применению. И может и обязательно будет типизирована при определении и вовсе без всякого применения.

K>Ну и в немерле никакой "типизации по месту применения" нет там просто всегда выводится конкретный тип, т.е. ограничение на полиморфизм сильнее чем в хаскеле и даже сильнее велью-рестрикшн в эмэлях.

Ну как же нет-то. В обоих языках — это некая стратегия, которая применяется в ряде случаев. Объясняется ли это исключительно дотнетовой системой типов — хз. Но смысл в этом есть и так — зачем нам полиморфная функция, если она используется неполиморфно?
И что-то мне кажется, в других ML-ях также можно найти подобное; проверять сейчас, правда, лень.
Re[29]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 12:44
Оценка: -1 :)
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Здравствуйте, VoidEx, Вы писали:


VE>>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>>Что как бы не исключает вышесказанного. Хаскелл, о котором в процитированном вами сообщении, речи вообще не шло, по умолчанию делает все функции полиморфными.

ВВ>>>Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?

VE>>Я вам немножко напомню, что речь была об Idris и ваших словах, что это благодаря "отложенной типизации". Вам уже 2 человека говорят, что это не так.

VE>>

VE>>Ну да, легко. Отложенная типизация в действии =)


ВВ>По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации.

Что вы имеете в виду под "доказательство корректности по месту применения"?
Вот в таком коде доказательство корректности делается по месту применения?

foo :: Int -> Int
foo = id

main = print (foo 23) -- тут доказывается, что 23 - это Int


И имеет ли к приведённому выше коду термин, популяризованный Москалем?
Re[30]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 12:45
Оценка:
Здравствуйте, VoidEx, Вы писали:

ВВ>>По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации.

VE>Что вы имеете в виду под "доказательство корректности по месту применения"?
VE>Вот в таком коде доказательство корректности делается по месту применения?

VE>
VE>foo :: Int -> Int
VE>foo = id

VE>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>


А этот код требуется доказывать? Здесь есть зависимые типы?

VE>И имеет ли к приведённому выше коду термин, популяризованный Москалем?


Т.е. вы все-таки кривляетесь?
Re[28]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 30.11.13 12:47
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

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


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

ВВ>И что-то мне кажется, в других ML-ях также можно найти подобное; проверять сейчас, правда, лень.


Ограничение полиморфизма с разными вариациями и названиями, разумеется, во всех есть. А типизации по применению (если понимать под этим то, что я написал выше) наоборот — нет. Такое (упрощенно говоря) есть разве что в C++.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[31]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 30.11.13 12:56
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

VE>>
VE>>foo :: Int -> Int
VE>>foo = id

VE>>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>>


ВВ>А этот код требуется доказывать? Здесь есть зависимые типы?


Ну так (Int -> Int) — это теорема, а id — ее (конструктивное) доказательство. А зависимые типы или нет — в данном случае значения не имеет.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[29]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 13:39
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, Воронков Василий, Вы писали:


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

K>По моему, "типизация по первому применению" означает, что могут быть нетипизированные декларации функций, которые будут типизированы только в том случае, если будут применены и не раньше этого. Ничего такого в хаскеле, эмэлях, немерле нет. Все функции типизируются даже без всяких применений и эти типы могут быть записаны синтаксически.

Что значит нетипизорованные декларации функций? Такие функции попросту не будут скомпилированы. Поэтому F# в данном случае использует тот же default int, а вот немерле, если я правильно помню, потребует аннотировать тип явно. Отложенная типизация только то, что функция типизируется по первому применению при наличии оного. И наверное это нормальная практика в случае, если полиморфный тип или слишком дорог (при рантайм полиморфизме).

В чем собственно проблема с этой терминологией, я не понимаю?

ВВ>>И что-то мне кажется, в других ML-ях также можно найти подобное; проверять сейчас, правда, лень.


K>Ограничение полиморфизма с разными вариациями и названиями, разумеется, во всех есть. А типизации по применению (если понимать под этим то, что я написал выше) наоборот — нет. Такое (упрощенно говоря) есть разве что в C++.


Нигде не утверждалось, что функции вообще не могут быть типизированы без применения; утверждалось, что они могут быть типизированы по применению.
Re[32]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 13:41
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, Воронков Василий, Вы писали:


VE>>>
VE>>>foo :: Int -> Int
VE>>>foo = id

VE>>>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>>>


ВВ>>А этот код требуется доказывать? Здесь есть зависимые типы?


K>Ну так (Int -> Int) — это теорема, а id — ее (конструктивное) доказательство. А зависимые типы или нет — в данном случае значения не имеет.


Хорошо, и какое это имеет отношение к обсуждаемому? Это как-то противоречит тому, что Идрис строит доказательство функции из ее применения?
Re[30]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 30.11.13 15:18
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Что значит нетипизорованные декларации функций?


То и значит, что они не типизированы.

ВВ>Такие функции попросту не будут скомпилированы.


Ну и что? Компилирование-то тут причем?

ВВ> Поэтому F# в данном случае использует тот же default int, а вот немерле, если я правильно помню, потребует аннотировать тип явно.


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

ВВ> Отложенная типизация только то, что функция типизируется по первому применению при наличии оного. И наверное это нормальная практика в случае, если полиморфный тип или слишком дорог (при рантайм полиморфизме).

ВВ>В чем собственно проблема с этой терминологией, я не понимаю?

Проблема в том, что то, о чем вы говорите, называется "ограничением полиморфизма" и есть практически везде. работа этого ограничения отличается разными особенностями, например, эвристиками разрешения неоднозначностей. Но работает это похожим образом.
Вот хаскель:
Prelude> let sum = \a b -> a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)

<interactive>:12:67:
    No instance for (Fractional Int)
      arising from the literal `2.0'
    Possible fix: add an instance declaration for (Fractional Int)
    In the first argument of `sum', namely `2.0'
    In the expression: sum 2.0 42
    In the expression: (foo, sum 2.0 42)

Prelude> let sum a b = a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)
(42,44.0)
it :: (Int, Double)

демонстрирует ту же проблему при ограничении полиморфизма и нормально работает без ограничения. Означает ли это что там типизация откладывается? Что функции типизируются по первому применению? Да нет конечно. Так никто не говорит и если кто-то будет — его не поймут. Это первая проблема. Вторая проблема в том, что эти "термины" описывают механизм типизации в таких языках неправильно.
Третья проблема в том, что вся эта ветка не имеет отношения к обсуждаемой теме. Она про разрешение противоречий при выводе типов. А функция на идрисе проаннотирована типом и типизирована тут же, на месте:

useValue : (p:Bool) -> myType p -> String


Ничего никуда не отложено, по применению ничего не типизируется.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[31]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 15:20
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Здравствуйте, VoidEx, Вы писали:


ВВ>>>По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации.

VE>>Что вы имеете в виду под "доказательство корректности по месту применения"?
VE>>Вот в таком коде доказательство корректности делается по месту применения?

VE>>
VE>>foo :: Int -> Int
VE>>foo = id

VE>>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>>


ВВ>А этот код требуется доказывать? Здесь есть зависимые типы?


Хорошо, а здесь где что доказывается по месту?

foo : (n : nat) → (n > 5) → string
foo n _ = show n
foo n ()

p : nat
p = 10

proof : 10 > 5
proof = refl

main = putStrLn (foo p proof)


VE>>И имеет ли к приведённому выше коду термин, популяризованный Москалем?


ВВ>Т.е. вы все-таки кривляетесь?


Пытаюсь выяснить значение терминов, которые вы вводите.
Re[31]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 15:52
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Что значит нетипизорованные декларации функций?


K>То и значит, что они не типизированы.


ВВ>>Такие функции попросту не будут скомпилированы.


K>Ну и что? Компилирование-то тут причем?


ВВ>> Поэтому F# в данном случае использует тот же default int, а вот немерле, если я правильно помню, потребует аннотировать тип явно.

K>Насколько я помню, для локальных функций там типы выведутся с ограничением полиморфизма, если только полиморфность не проаннотировать явно.

"Там" — это где?

ВВ>> Отложенная типизация только то, что функция типизируется по первому применению при наличии оного. И наверное это нормальная практика в случае, если полиморфный тип или слишком дорог (при рантайм полиморфизме).

ВВ>>В чем собственно проблема с этой терминологией, я не понимаю?
K>Проблема в том, что то, о чем вы говорите, называется "ограничением полиморфизма" и есть практически везде. работа этого ограничения отличается разными особенностями, например, эвристиками разрешения неоднозначностей. Но работает это похожим образом.

То, о чем я говорю, называется отложенной типизацией. А в Хаскелле это ограничение полиморфизма, да.

K>Вот хаскель:

K>
K>Prelude> let sum = \a b -> a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)

K><interactive>:12:67:
K>    No instance for (Fractional Int)
K>      arising from the literal `2.0'
K>    Possible fix: add an instance declaration for (Fractional Int)
K>    In the first argument of `sum', namely `2.0'
K>    In the expression: sum 2.0 42
K>    In the expression: (foo, sum 2.0 42)

K>Prelude> let sum a b = a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)
K>(42,44.0)
K>it :: (Int, Double)
K>

K>демонстрирует ту же проблему при ограничении полиморфизма и нормально работает без ограничения. Означает ли это что там типизация откладывается? Что функции типизируются по первому применению? Да нет конечно. Так никто не говорит и если кто-то будет — его не поймут. Это первая проблема.

Да, вот только этот код действительно демонстрирует другое. И действительно никто не говорит об отложенной типизации в Хаскелле.
В том же F# нет никакого ограничения полиморфизма, что прекрасно видно по коду. "let sum x y = x+y" без применения не будет иметь обобщенный тип, а будет иметь тип int->int->int. При наличии первого применения будет типизирована по первому применению и может стать, скажем, string->string->string. Ограничением чего в данном случае является string->string->string?
По Немерле так и вовсе есть документ:
http://research.microsoft.com/en-us/um/people/moskal/pdf/msc.pdf

K>Вторая проблема в том, что эти "термины" описывают механизм типизации в таких языках неправильно.


Пруф, пожалуйста, что этот "термин" описывает механизм типизации в F# неправильно.

K>Третья проблема в том, что вся эта ветка не имеет отношения к обсуждаемой теме. Она про разрешение противоречий при выводе типов. А функция на идрисе проаннотирована типом и типизирована тут же, на месте:

K>
K>useValue : (p:Bool) -> myType p -> String
K>

K>Ничего никуда не отложено, по применению ничего не типизируется.

Да, тип аннотирован явно. Только вот этого типа недостаточно, чтобы программа прошла проверку. Корректность функции должна быть доказана на основе применения.
Re[32]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 16:09
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

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


Эта функция — корректна, компилируется и работает, этого типа достаточно и он меняться не будет.
Что значит "этого типа недостаточно, чтобы программа прошла проверку"?
Типа функции id : a -> a тоже недостаточно?
Re[33]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 16:17
Оценка:
Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, Воронков Василий, Вы писали:


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


VE>Эта функция — корректна, компилируется и работает, этого типа достаточно и он меняться не будет.

VE>Что значит "этого типа недостаточно, чтобы программа прошла проверку"?
VE>Типа функции id : a -> a тоже недостаточно?

У меня не работает, типы используются правильно:

fun : (xs : List Int) -> sumType (length xs)
fun xs = adder (length xs) (sum xs)

saturate : (n:Nat) -> Int -> sumType n -> Int
saturate Z x f = f
saturate (S k) x f = saturate k x (f x)

convertArgs : List String -> List Int
convertArgs [] = []
convertArgs (x::xs) = map cast xs

main : IO ()
main = do 
  as <- getArgs
  let xs = convertArgs as
  print $ saturate 2 100 (fun xs)
Re[23]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 16:55
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

DM>>Я перевел твою программу дословно. В ней ровно столько зависимости от рантайм значений, сколько в оригинале. Если в статически типизированной версии такой зависимости не усматривается, это лишь потому, что ее не было в исходном варианте.


ВВ>Ну зачем же обманывать? Моя программа работает корректно благодаря рантайм проверке типа, ты, конечно же, ее устранил, но теперь оказывается, что программа была переведена "дословно". Это нормальный подход к дискуссии для тебя?


Не было у тебя рантайм проверки типа, тип там везде один — dynamic (или как он там называтся в Эле). А была проверка тэга, который сидит в каждом значении. Именно такую проверку я и сделал, выразив этот тэг явно. Число возможных вариантов оказалось меньше, тэгов всего два возможных получилось, лишние были выкинуты. Поэтому это вполне себе дословный перевод: что делалось в оригинале, то и делается в переводе.
Re[23]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 17:17
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ> говоришь как человек, который "других ФЯ" в глаза не видел. Причем довольно известных. Например, F#.


Спасибо, просветил меня насчет F#. Я и раньше знал, что это недоделка по мотивам приличного языка, но как-то запямятовал, что настолько убогая. Но ведь "нормальные" полиморфные функции там тоже есть? Это просто проблема слабого вывода типов, как я понял.

ВВ>Да повторяй хоть сотни раз. В твоей трактовке сам термин "зависимость от рантайм-значений" теряет всякий смысл. Я уже множество раз, разными словами, пытался объяснить, какой смысл я вкладываю в это утверждение. Мы зависим от рантайма только в том случае, когда не можем рассуждать о возможных значениях статически.


Раньше ты формулировал его по-другому. Теперь понятно. Что ж, просто у тебя абсолютно неправильное определение. Предлагаю его выкинуть на помоечку и почерпнуть правильное.

ВВ>>>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.

DM>>Да. Но сами конкретные значения не известны, в этом вся суть.
ВВ>Вообще-то если конкретные значения известны, то обычно и само вычисление не требуется.

Какое именно вычисление? Речь же идет о типах, не забывай.

DM>>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!

ВВ>Можно подумать, это и правда было для тебя сюрпризом, судя по тому, с каким жаром ты сейчас об этом рассуждаешь.

Для меня-то нет, ведь это я тебе на ошибки в статье указываю, а не наоборот.

ВВ>Обработка означает, что код *может* работать неправильно, мы допускаем это и пишем другой код, который обрабатывает данную ситуацию. Т.е. мы не задаемся вопросом "при каких значениях этот код будет работать?"; у нас другой вопрос — "что делать, когда код не работает?"


А, навроде catch(...). Ну, тут понятно что делать — констатировать, что в программе баг и идти его исправлять. Обсуждать технику написания абсурдных программ с багами не очень интересно, по выразительности некорректных программ динамические языки конечно сложно превзойти. Я все же вел речь о способах выражения корректных программ.
Re[34]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 17:30
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

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


Я понял, речь идет не о "корректности функции", а о проверке типа выражения, в котором она применяется.

ВВ>У меня не работает, типы используются правильно:

ВВ>saturate : (n:Nat) -> Int -> sumType n -> Int
ВВ> let xs = convertArgs as
ВВ> print $ saturate 2 100 (fun xs)

Тут функция и ее тип корректные, но вызывается она не с подходящими типами аргументов, поэтому выражение saturate 2 100 (fun xs) не проходит проверку типов. Это как в List.map передавать не список, а число. Функция-то правильная, но используется неправильно.
Re[24]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 17:40
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


DM>>>Я перевел твою программу дословно. В ней ровно столько зависимости от рантайм значений, сколько в оригинале. Если в статически типизированной версии такой зависимости не усматривается, это лишь потому, что ее не было в исходном варианте.


ВВ>>Ну зачем же обманывать? Моя программа работает корректно благодаря рантайм проверке типа, ты, конечно же, ее устранил, но теперь оказывается, что программа была переведена "дословно". Это нормальный подход к дискуссии для тебя?

DM>Не было у тебя рантайм проверки типа, тип там везде один — dynamic (или как он там называтся в Эле). А была проверка тэга, который сидит в каждом значении.

Давай только не уводить все в сторону "в динамике вообще один тип".
Вот это вот:

x is Fun


это проверка того, что x является функцией. Fun в данном случае не конструктор, а x не является алгебраическим типом.

DM>Именно такую проверку я и сделал, выразив этот тэг явно. Число возможных вариантов оказалось меньше, тэгов всего два возможных получилось, лишние были выкинуты. Поэтому это вполне себе дословный перевод: что делалось в оригинале, то и делается в переводе.
Re[35]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 17:45
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


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


DM>Я понял, речь идет не о "корректности функции", а о проверке типа выражения, в котором она применяется.


ВВ>>У меня не работает, типы используются правильно:

ВВ>>saturate : (n:Nat) -> Int -> sumType n -> Int
ВВ>> let xs = convertArgs as
ВВ>> print $ saturate 2 100 (fun xs)

DM>Тут функция и ее тип корректные, но вызывается она не с подходящими типами аргументов, поэтому выражение saturate 2 100 (fun xs) не проходит проверку типов. Это как в List.map передавать не список, а число. Функция-то правильная, но используется неправильно.


Разве эта аналогия уместна? Такое применение saturate как у меня вполне соответствует сигнатуре функции, насколько я могу судить.
Re[24]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 17:49
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:

ВВ>> говоришь как человек, который "других ФЯ" в глаза не видел. Причем довольно известных. Например, F#.
DM>Спасибо, просветил меня насчет F#. Я и раньше знал, что это недоделка по мотивам приличного языка, но как-то запямятовал, что настолько убогая. Но ведь "нормальные" полиморфные функции там тоже есть? Это просто проблема слабого вывода типов, как я понял.

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

ВВ>>>>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.

DM>>>Да. Но сами конкретные значения не известны, в этом вся суть.
ВВ>>Вообще-то если конкретные значения известны, то обычно и само вычисление не требуется.

DM>Какое именно вычисление? Речь же идет о типах, не забывай.


DM>>>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!

ВВ>>Можно подумать, это и правда было для тебя сюрпризом, судя по тому, с каким жаром ты сейчас об этом рассуждаешь.
DM>Для меня-то нет, ведь это я тебе на ошибки в статье указываю, а не наоборот.

В статье не идет речи о зависимых типах. Спор идет о том, возможна и в каком виде возможна вполне конкретная функция в статическом языке.

ВВ>>Обработка означает, что код *может* работать неправильно, мы допускаем это и пишем другой код, который обрабатывает данную ситуацию. Т.е. мы не задаемся вопросом "при каких значениях этот код будет работать?"; у нас другой вопрос — "что делать, когда код не работает?"

DM>А, навроде catch(...). Ну, тут понятно что делать — констатировать, что в программе баг и идти его исправлять. Обсуждать технику написания абсурдных программ с багами не очень интересно, по выразительности некорректных программ динамические языки конечно сложно превзойти. Я все же вел речь о способах выражения корректных программ.

Необязательно catch, хотя это тоже вариант. Вообще-то речь не идет о красивом или некрасивом коде. Речь идет о том, возможно ли fun на Ela реализовать в статике. Ты приводишь аналоги, которые работают — но иначе.
Re[25]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 18:26
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Давай только не уводить все в сторону "в динамике вообще один тип".

ВВ>x is Fun
ВВ>это проверка того, что x является функцией. Fun в данном случае не конструктор, а x не является алгебраическим типом.

Эдак ты все сведешь к утверждениям вроде: вот это нельзя сделать на другом языке потому что это будет другой язык и будет выражено другими средствами.
С т.з. как теории типов, так и реализации многих ДЯП, в динамике как раз всего один тип, и он даже алгебраический. Если от этого не отнекиваться, то очевидно, как любую программу на динамически типизированном языке можно при желании один в один переписать на статическом. Но я согласен, это уже не интересная тема.
Re[36]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 18:33
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>>>saturate : (n:Nat) -> Int -> sumType n -> Int

ВВ>>> print $ saturate 2 100 (fun xs)

DM>>Тут функция и ее тип корректные, но вызывается она не с подходящими типами аргументов, поэтому выражение saturate 2 100 (fun xs) не проходит проверку типов. Это как в List.map передавать не список, а число. Функция-то правильная, но используется неправильно.


ВВ>Разве эта аналогия уместна? Такое применение saturate как у меня вполне соответствует сигнатуре функции, насколько я могу судить.


По-моему, не соответствует. Чтобы применение было корректным, тут (fun xs) должно иметь тип sumType 2, но этого типа оно не имеет, а имеет sumType (length xs). О чем компилятор и сообщает.
Can't unify
        sumType (Prelude.List.length xs)
with
        sumType (Prelude.Classes.fromInteger 2)
Re[25]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 18:41
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Я так понял "ересь", "ненормальный" и "немерле" теперь являются синонимами.

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

Я бы отталкивался от теории типов, штук вроде System F, лямбда-куба и т.п.

ВВ>В статье не идет речи о зависимых типах. Спор идет о том, возможна и в каком виде возможна вполне конкретная функция в статическом языке.


Так языки с завтипами как раз статически типизированы, ровно поэтому и возникло возражение.

DM>>А, навроде catch(...). Ну, тут понятно что делать — констатировать, что в программе баг и идти его исправлять. Обсуждать технику написания абсурдных программ с багами не очень интересно, по выразительности некорректных программ динамические языки конечно сложно превзойти. Я все же вел речь о способах выражения корректных программ.


ВВ>Необязательно catch, хотя это тоже вариант. Вообще-то речь не идет о красивом или некрасивом коде. Речь идет о том, возможно ли fun на Ela реализовать в статике. Ты приводишь аналоги, которые работают — но иначе.


Я тоже говорю не о красивом коде, а о корректном.
Реализованы мои аналоги, конечно, иначе, но соответствуют постановке задачи (например, соответствие числа аргументов длине списка), т.е. реализовать подобные функции в статике таки можно. Просто несколько не в той статике, которая подразумевалась в статье.
Re[32]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 30.11.13 18:48
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

K>>Насколько я помню, для локальных функций там типы выведутся с ограничением полиморфизма, если только полиморфность не проаннотировать явно.

ВВ>"Там" — это где?

В немерле.

ВВ>То, о чем я говорю, называется отложенной типизацией.


Нет, в ваших примерах именно ограничение полиморфизма.

ВВ>Да, вот только этот код действительно демонстрирует другое. И действительно никто не говорит об отложенной типизации в Хаскелле.

ВВ>В том же F# нет никакого ограничения полиморфизма, что прекрасно видно по коду. "let sum x y = x+y" без применения не будет иметь обобщенный тип, а будет иметь тип int->int->int. При наличии первого применения будет типизирована по первому применению и может стать, скажем, string->string->string. Ограничением чего в данном случае является string->string->string?

Именно по коду и видно, что есть. Вот смотрите: для того, чтоб функцию выполнить нам нужно функцию конкретизировать, заполнить все параметры со штрихами в ее типе, точно так же, как и во все параметры функции что-то передать. F#, как я уже сказал, — это два языка с различающимися системами типов. Типы "языка inline-функций" могут быть в том числе и такими, какие в основном языке невозможны:

> let inline sum x y = x+y;;

val inline sum :
  x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( + ) :  ^a *  ^b ->  ^c)


Пока мы остаемся в рамках "inline-F#" все хорошо:

> let inline x2 x = sum x x;;

val inline x2 :
  x: ^a ->  ^b when  ^a : (static member ( + ) :  ^a *  ^a ->  ^b)


Но если мы используем inline-функцию в обычной, нам придется заполнить все параметры с крышечкой, точно так же, как нам нужно заполнить все параметры со штрихами чтоб что-то выполнить. Вот тут и наступает ограничение полиморфизма. В данном случае — "крышечного".
Конкретные типы нужно откуда-то брать, это можно сделать с той или иной степенью хитрости, но тут можно только из типов по умолчанию:
> let x2 x = sum x x;;

val x2 : x:int -> int

А где-то из применения и т.д. Если же это невозможно — вывод типов сдается и просит проаннотировать тип вручную. Это не только определение типа по применению (может по возвращению, например), а F# не всегда и по применению может:

> let foo x = x.Length in foo [|1|];;

  let foo x = x.Length in foo [|1|];;
  ------------^^^^^^^^

stdin(46,13): error FS0072: Lookup on object of indeterminate type 
based on information prior to this program point. A type annotation 
may be needed prior to this program point to constrain the type of 
the object. This may allow the lookup to be resolved.


Некоторые применения в F# равнее прочих:

> [|1|] |> fun x -> x.Length;;
val it : int = 1
> fun x -> x.Length <| [|1|] ;;

  fun x -> x.Length <| [|1|] ;;
  ---------^^^^^^^^

stdin(52,10): error FS0072: и т.д.


Этот недоделанный алгоритм мономорфизации в F# и является прямым родственником локального вывода типов из Немерле (в котором он действительно выводит тип по применению и отложенно и работает в более сложных случаях). Аналогов основного, "обобщающего" вывода типа (в F# это как обычно какая-то вариация алгоритма-W) в немерле нет.

ВВ>Пруф, пожалуйста, что этот "термин" описывает механизм типизации в F# неправильно.


С.м. выше, вы говорили что функции "типизируются по применению" а F# даже тип по применению вывести не может. С другой стороны — в других случаях может без всякого применения.

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


Это не верно.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[33]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 18:58
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, Воронков Василий, Вы писали:


K>>>Насколько я помню, для локальных функций там типы выведутся с ограничением полиморфизма, если только полиморфность не проаннотировать явно.

ВВ>>"Там" — это где?
K>В немерле.

Москаль же вполне подробно описывает, что и как там выводится. Посмотри "Type inference with deferal".
Выше же ты утверждаешь, что типизации по применению нет и в Немерле.

ВВ>>То, о чем я говорю, называется отложенной типизацией.

K>Нет, в ваших примерах именно ограничение полиморфизма.
ВВ>>Да, вот только этот код действительно демонстрирует другое. И действительно никто не говорит об отложенной типизации в Хаскелле.
ВВ>>В том же F# нет никакого ограничения полиморфизма, что прекрасно видно по коду. "let sum x y = x+y" без применения не будет иметь обобщенный тип, а будет иметь тип int->int->int. При наличии первого применения будет типизирована по первому применению и может стать, скажем, string->string->string. Ограничением чего в данном случае является string->string->string?

K>Именно по коду и видно, что есть. Вот смотрите: для того, чтоб функцию выполнить нам нужно функцию конкретизировать, заполнить все параметры со штрихами в ее типе, точно так же, как и во все параметры функции что-то передать. F#, как я уже сказал, — это два языка с различающимися системами типов. Типы "языка inline-функций" могут быть в том числе и такими, какие в основном языке невозможны:

K>
>> let inline sum x y = x+y;;
K>val inline sum :
K>  x: ^a -> y: ^b ->  ^c
K>    when ( ^a or  ^b) : (static member ( + ) :  ^a *  ^b ->  ^c)
K>


Инлайн — это инлайн. Было бы очень странно, если бы инлайн типизировался по первому применению.

K>Пока мы остаемся в рамках "inline-F#" все хорошо:


K>
>> let inline x2 x = sum x x;;
K>val inline x2 :
K>  x: ^a ->  ^b when  ^a : (static member ( + ) :  ^a *  ^a ->  ^b)
K>

K>Но если мы используем inline-функцию в обычной, нам придется заполнить все параметры с крышечкой, точно так же, как нам нужно заполнить все параметры со штрихами чтоб что-то выполнить. Вот тут и наступает ограничение полиморфизма. В данном случае — "крышечного".
K>Конкретные типы нужно откуда-то брать, это можно сделать с той или иной степенью хитрости, но тут можно только из типов по умолчанию:
K>
>> let x2 x = sum x x;;
K>val x2 : x:int -> int
K>

K>А где-то из применения и т.д. Если же это невозможно — вывод типов сдается и просит проаннотировать тип вручную.

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

Я не понимаю, в чем проблема. Не устраивет термин "отложенная"? Мое утверждение понимается так, как будто в языке *всегда* используется отложенная типизация? Нет, не всегда. Иногда — используется. А иногда (в F#, кстати, нередко) все вообще аннотировано явно.

K>Это не только определение типа по применению (может по возвращению, например), а F# не всегда и по применению может:

K>
>> let foo x = x.Length in foo [|1|];;
K>  let foo x = x.Length in foo [|1|];;
K>  ------------^^^^^^^^
K>stdin(46,13): error FS0072: Lookup on object of indeterminate type 
K>based on information prior to this program point. A type annotation 
K>may be needed prior to this program point to constrain the type of 
K>the object. This may allow the lookup to be resolved.
K>


K>Некоторые применения в F# равнее прочих:


K>
>> [|1|] |> fun x -> x.Length;;
K>val it : int = 1
>> fun x -> x.Length <| [|1|] ;;

K>  fun x -> x.Length <| [|1|] ;;
K>  ---------^^^^^^^^

K>stdin(52,10): error FS0072: и т.д.
K>


K>Этот недоделанный алгоритм мономорфизации в F# и является прямым родственником локального вывода типов из Немерле (в котором он действительно выводит тип по применению и отложенно и работает в более сложных случаях). Аналогов основного, "обобщающего" вывода типа (в F# это как обычно какая-то вариация алгоритма-W) в немерле нет.


ВВ>>Пруф, пожалуйста, что этот "термин" описывает механизм типизации в F# неправильно.

K>С.м. выше, вы говорили что функции "типизируются по применению" а F# даже тип по применению вывести не может. С другой стороны — в других случаях может без всякого применения.

В F# этот алгоритм сильно отличается от немерлового, в котором собственно ХМ вообще не используется, насколько я понимаю. Но тем не менее — иногда F# таки выводит тип по применению и отложенно.

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

K>Это не верно.
Re[34]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 20:37
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>У меня не работает, типы используются правильно:


ВВ>
ВВ>fun : (xs : List Int) -> sumType (length xs)
ВВ>fun xs = adder (length xs) (sum xs)

ВВ>saturate : (n:Nat) -> Int -> sumType n -> Int
ВВ>saturate Z x f = f
ВВ>saturate (S k) x f = saturate k x (f x)

ВВ>convertArgs : List String -> List Int
ВВ>convertArgs [] = []
ВВ>convertArgs (x::xs) = map cast xs

ВВ>main : IO ()
ВВ>main = do 
ВВ>  as <- getArgs
ВВ>  let xs = convertArgs as
ВВ>  print $ saturate 2 100 (fun xs)
ВВ>


Конечно неправильно, и вы сами это видите. 2 никак не равняется length xs.
Re[23]: философия статики
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 01.12.13 08:48
Оценка: 2 (1) :)
Здравствуйте, Воронков Василий, Вы писали:

ВВ> Мы зависим от рантайма только в том случае, когда не можем рассуждать о возможных значениях статически.


Пофилософствую немножко.
Если открыть учебники по теории типов и дизайну ЯП, там говорится, что в статической типизации тип — это некая синтаксическая конструкция, которая приписывается (порой компилятором, когда есть вывод типов) каждому терму (выражению) в исходном коде программы. Нужна она как раз для статических рассуждений о возможных значениях.

Мысль 1. Если получилось все термы в программе непротиворечиво снабдить типами, то все ок, у нас есть корректная программа, свободная от рантайм ошибок типизации. И если получилось, значит мы смогли рассудить о значениях статически. Если же по какой-то причине мы не может о них статически рассуждать, то и типизировать статически программу не выйдет, она не будет считаться корректной. Фактически, твои вопрошания свелись к "можем ли мы в статике сделать то, чего нельзя делать в статике?". Видимо, не можем.

Мысль 2. По какой причине может возникнуть такое затруднение со статической расстановкой типов? В языках попроще (вплоть до хаскеля) обычно есть явное разграничение между термами и типами. Это два отдельных языка, термы строятся так-то, типы строятся так-то, связываются они через а::Т ("терм а имеет тип Т"). Поскольку это разные языки, они могут где-то расходиться в выразительной силе, и какому-то выражению на языке термов может не соответствовать ни одно выражение на языке типов. Такое выражение не получится типизировать в этой системе типов.

Но системы с зависимыми типами тут разительно отличаются. Они убирают эту грань между двумя подъязыками термов и типов, теперь это все один язык термов. 42 это терм, и Int это терм, и термы могут выступать в роли типов (связка "терм а имеет тип Т" синтаксически выглядит как "терм : терм", а не "терм : тип"). В результате поскольку слева и справа от : ("имеет тип") один и тот же язык, выразительность одинаковая, и по крайней мере этот источник нетипизируемости каких-то выражений устраняется.

Мысль 3. Системы типов в приличных местах строятся не от балды, а основываются на стройных идеях из логики и теории категорий (произведение-конъюнкция, копроизведение-сумма-дизъюнкция, экспонента-следствие и т.п.) в результате чего имеем соответствие Карри-Говарда, согласно которому типы это логические утверждения в интуиционистской логике, а имеющие их термы — это их доказательства. Написал тело функции нужного типа — значит написал конструктивное доказательство теоремы. В этом свете любой код, у которого нет статического типа — это доказательство без утверждения. И всякое бестиповое программирование — это тоже попытка строить доказательства без утверждений. Есть в этом что-то шизофреническое, рациональной деятельностью это сложно назвать.
Re[34]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 01.12.13 14:55
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Выше же ты утверждаешь, что типизации по применению нет и в Немерле.


Там, где я это утверждаю, я также и описываю, что я под этим понимаю. "Отложенная типизация по первому применению" в моем понимании это, когда функция не типизируется вообще, существует в виде текстового шаблона например. И при применении в этот шаблон подставляются типы и только после этого полученный код типизируется.

Отложенный вывод типов в Немерле есть, но его нет в F#. Москальский алгоритм называется отложенным, как я понимаю, чтоб подчеркнуть его отличие от "жадного" алгоритма Карделли. И отличие это заключается в механизме работы с сабтайпингом. Именно оно позволяет выводить типы в тех случаях, для которых я показал, что F# типы вывести наоборот не может. Т.е. никакого отложенного вывода типов там нет.

ВВ>Инлайн — это инлайн. Было бы очень странно, если бы инлайн типизировался по первому применению.


Ну правильно. Было бы также странно если бы обычные функции типизировались по первому применению. Поэтому тип и для тех и для других выводится по Х-М, а конкретизируется при ограничении полиморфизма при переходе от первых ко вторыи и при доведении функций до "выполняемого состояния". Аналогичные эффекты проявляются и в хаскеле и я это показал.

ВВ>Ну, правильно — если функция обычная, то для нее в качестве одной из стратегий используется вывод типов по применению, что хорошо видно на множестве примеров. Используется при этом не так агрессивно, как в Немерле, да, но он как бы используется. Откуда бы иначе "штришки" в типах функций заполнялись строками да числами?


Если вы то, что вы показали для F# называете "типизацией по первому применению", то почему вы тогда соглашаетесь с тем, что с хаскелем тут ничего общего нет, ведь вывод типов в F# работает в основном как в хаскеле и совсем не так как в немерле.

ВВ>Я не понимаю, в чем проблема. Не устраивет термин "отложенная"? Мое утверждение понимается так, как будто в языке *всегда* используется отложенная типизация? Нет, не всегда. Иногда — используется. А иногда (в F#, кстати, нередко) все вообще аннотировано явно.


Три проблемы я перечислил. Оказалось, что есть и четвертая. Создается ложное впечатление, что в F# используется тот же способ мономорфизации в присутствии сабтайпинга, что и в немерле. Но название немерлевского алгоритма как раз и подчеркивает его отличие от родственных тому, что используется в F#.

ВВ>В F# этот алгоритм сильно отличается от немерлового, в котором собственно ХМ вообще не используется, насколько я понимаю.


В прошлом посте я так и написал. В F# есть алгоритм общего вывода типов (вариация Х-М), а есть простая реконструкция типов при ограничении полиморфизма. В немерле же общего вывода нет вообще, а реконструкция как раз навороченная.

ВВ>Но тем не менее — иногда F# таки выводит тип по применению и отложенно.


Иногда F# выводит типы как хаскель, а как немерле никогда, что я продемонстрировал на примерах.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[24]: философия статики
От: Воронков Василий Россия  
Дата: 01.12.13 18:19
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


ВВ>> Мы зависим от рантайма только в том случае, когда не можем рассуждать о возможных значениях статически.


DM>Пофилософствую немножко.

DM>Если открыть учебники по теории типов и дизайну ЯП, там говорится, что в статической типизации тип — это некая синтаксическая конструкция, которая приписывается (порой компилятором, когда есть вывод типов) каждому терму (выражению) в исходном коде программы. Нужна она как раз для статических рассуждений о возможных значениях.
DM>Мысль 1. Если получилось все термы в программе непротиворечиво снабдить типами, то все ок, у нас есть корректная программа, свободная от рантайм ошибок типизации. И если получилось, значит мы смогли рассудить о значениях статически. Если же по какой-то причине мы не может о них статически рассуждать, то и типизировать статически программу не выйдет, она не будет считаться корректной. Фактически, твои вопрошания свелись к "можем ли мы в статике сделать то, чего нельзя делать в статике?". Видимо, не можем.

Ага, надо было, наверное, ставить вопрос — а можем ли мы на одном Тьюринг-полном языке решить задачу, решенную на другом. Видимо, можем. На то он и Тьюринг-полный.

DM>Мысль 2. По какой причине может возникнуть такое затруднение со статической расстановкой типов? В языках попроще (вплоть до хаскеля) обычно есть явное разграничение между термами и типами. Это два отдельных языка, термы строятся так-то, типы строятся так-то, связываются они через а::Т ("терм а имеет тип Т"). Поскольку это разные языки, они могут где-то расходиться в выразительной силе, и какому-то выражению на языке термов может не соответствовать ни одно выражение на языке типов. Такое выражение не получится типизировать в этой системе типов.


DM>Но системы с зависимыми типами тут разительно отличаются. Они убирают эту грань между двумя подъязыками термов и типов, теперь это все один язык термов. 42 это терм, и Int это терм, и термы могут выступать в роли типов (связка "терм а имеет тип Т" синтаксически выглядит как "терм : терм", а не "терм : тип"). В результате поскольку слева и справа от : ("имеет тип") один и тот же язык, выразительность одинаковая, и по крайней мере этот источник нетипизируемости каких-то выражений устраняется.


DM>Мысль 3. Системы типов в приличных местах строятся не от балды, а основываются на стройных идеях из логики и теории категорий (произведение-конъюнкция, копроизведение-сумма-дизъюнкция, экспонента-следствие и т.п.) в результате чего имеем соответствие Карри-Говарда, согласно которому типы это логические утверждения в интуиционистской логике, а имеющие их термы — это их доказательства. Написал тело функции нужного типа — значит написал конструктивное доказательство теоремы. В этом свете любой код, у которого нет статического типа — это доказательство без утверждения. И всякое бестиповое программирование — это тоже попытка строить доказательства без утверждений. Есть в этом что-то шизофреническое, рациональной деятельностью это сложно назвать.


Это что, в Кащенко так программируют? Безтипового программирования не бывает. Программист так или иначе подразумевает типы и делает утверждения, а вот конкретный компилятор может уже его утверждения проверить (типизировать) или довериться рантайму. ФП как раз безтиповое изначально и без типов прекрасно обходится.
Re[25]: философия статики
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 01.12.13 18:36
Оценка: +1 :)
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Ага, надо было, наверное, ставить вопрос — а можем ли мы на одном Тьюринг-полном языке решить задачу, решенную на другом. Видимо, можем. На то он и Тьюринг-полный.


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

ВВ>Это что, в Кащенко так программируют? Безтипового программирования не бывает. Программист так или иначе подразумевает типы и делает утверждения, а вот конкретный компилятор может уже его утверждения проверить (типизировать) или довериться рантайму. ФП как раз безтиповое изначально и без типов прекрасно обходится.


Если эти утверждения остаются несформулированными, у них большой шанс быть или неверными или просто абсурдными.
Что до Кащенко, то это лучше спросить у того, кто в одном абзаце говорит "ФП как раз безтиповое изначально и без типов прекрасно обходится" и "Безтипового программирования не бывает".
Re[35]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 01.12.13 22:34
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, Воронков Василий, Вы писали:

ВВ>>Выше же ты утверждаешь, что типизации по применению нет и в Немерле.
K>Там, где я это утверждаю, я также и описываю, что я под этим понимаю. "Отложенная типизация по первому применению" в моем понимании это, когда функция не типизируется вообще, существует в виде текстового шаблона например. И при применении в этот шаблон подставляются типы и только после этого полученный код типизируется.

Интересно, конечно. Ты еще текстовые макросы вспомни. Отложенная типизация означает, что тип функции уточняется по первому применению.

K>Отложенный вывод типов в Немерле есть, но его нет в F#. Москальский алгоритм называется отложенным, как я понимаю, чтоб подчеркнуть его отличие от "жадного" алгоритма Карделли. И отличие это заключается в механизме работы с сабтайпингом. Именно оно позволяет выводить типы в тех случаях, для которых я показал, что F# типы вывести наоборот не может. Т.е. никакого отложенного вывода типов там нет.


В F# с выводом типов все дрвольно запутанно и сложно. Х-М там все равно используется сильно модифицированный; AFAIR там вообще разные стратегии вывода типов для разных случаев, ибо поддерживается глобальный вывод типов, а снаружи у нас дотнет. Поэтому таки да, такая стратегия как отложенный вывод типа функции там таки используется. И даже *по твоим примерам* хорошо видно, что это не усечение полиморфизма, ибо без применения глобальная функция вида let sum x y = x+y все равно не будет иметь полиморфный тип.

ВВ>>Инлайн — это инлайн. Было бы очень странно, если бы инлайн типизировался по первому применению.

K>Ну правильно. Было бы также странно если бы обычные функции типизировались по первому применению. Поэтому тип и для тех и для других выводится по Х-М, а конкретизируется при ограничении полиморфизма при переходе от первых ко вторыи и при доведении функций до "выполняемого состояния". Аналогичные эффекты проявляются и в хаскеле и я это показал.

Все-все выводится по ХМ? В дотнетовой системе типов? Ну-ну. Это про какой-то другой язык рассказываешь, не про F#.

ВВ>>Ну, правильно — если функция обычная, то для нее в качестве одной из стратегий используется вывод типов по применению, что хорошо видно на множестве примеров. Используется при этом не так агрессивно, как в Немерле, да, но он как бы используется. Откуда бы иначе "штришки" в типах функций заполнялись строками да числами?

K>Если вы то, что вы показали для F# называете "типизацией по первому применению", то почему вы тогда соглашаетесь с тем, что с хаскелем тут ничего общего нет, ведь вывод типов в F# работает в основном как в хаскеле и совсем не так как в немерле.

Потому что в Хаскелле этого нет, в Хаскелле усечение полиморфизма.

ВВ>>Я не понимаю, в чем проблема. Не устраивет термин "отложенная"? Мое утверждение понимается так, как будто в языке *всегда* используется отложенная типизация? Нет, не всегда. Иногда — используется. А иногда (в F#, кстати, нередко) все вообще аннотировано явно.

K>Три проблемы я перечислил. Оказалось, что есть и четвертая. Создается ложное впечатление, что в F# используется тот же способ мономорфизации в присутствии сабтайпинга, что и в немерле. Но название немерлевского алгоритма как раз и подчеркивает его отличие от родственных тому, что используется в F#.

Проблема одна. Нет, вернее, две. Первоначально ты пытался утверждать, что этого нет даже в немерле. Данный вопрос, я так понимаю, мы замяли? Осталось теперь замять вопрос с F# и можно начинать спорить о чем-то другом, как здесь принято.

ВВ>>В F# этот алгоритм сильно отличается от немерлового, в котором собственно ХМ вообще не используется, насколько я понимаю.

K>В прошлом посте я так и написал. В F# есть алгоритм общего вывода типов (вариация Х-М), а есть простая реконструкция типов при ограничении полиморфизма. В немерле же общего вывода нет вообще, а реконструкция как раз навороченная.
ВВ>>Но тем не менее — иногда F# таки выводит тип по применению и отложенно.
K>Иногда F# выводит типы как хаскель, а как немерле никогда, что я продемонстрировал на примерах.

На примерах с инлайн? Смешно.
Re[26]: философия статики
От: Воронков Василий Россия  
Дата: 01.12.13 22:37
Оценка:
Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, Воронков Василий, Вы писали:


ВВ>>Ага, надо было, наверное, ставить вопрос — а можем ли мы на одном Тьюринг-полном языке решить задачу, решенную на другом. Видимо, можем. На то он и Тьюринг-полный.


DM>Самое смешное, что завтипы часто требуют тотальность, а она влечет Тьюринг-худобу. Мы привыкли иметь Тьюринг-полноту как нечто само собой разумеющееся, но это скорее баг, чем фича. Возможность бесконечных циклов все портит по части reasoning, но при наличии коиндукции не особенно нужна на практике.


ВВ>>Это что, в Кащенко так программируют? Безтипового программирования не бывает. Программист так или иначе подразумевает типы и делает утверждения, а вот конкретный компилятор может уже его утверждения проверить (типизировать) или довериться рантайму. ФП как раз безтиповое изначально и без типов прекрасно обходится.

DM>Если эти утверждения остаются несформулированными, у них большой шанс быть или неверными или просто абсурдными.

Статика вс. динамика — это действительно настолько интересная тема или просто больная мозоль?

DM>Что до Кащенко, то это лучше спросить у того, кто в одном абзаце говорит "ФП как раз безтиповое изначально и без типов прекрасно обходится" и "Безтипового программирования не бывает".


Ага, потому что в процесс программирования еще вовлечен человек. И вот он-то как раз не может без типов, а языки программирования без них прекрасно обходятся. Так что да. Безтипового программирования не бывает, а языки — вполне. Все же это человек делает утверждения, а не компилятор.
Re[36]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 02.12.13 10:19
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Интересно, конечно. Ты еще текстовые макросы вспомни. Отложенная типизация означает, что тип функции уточняется по первому применению.


ОК. Тоесть Х-М это и есть "отложенная типизация"? Уточнение (раньше у вас была типизация) типа по первому применению я продемонстрировал.

ВВ>В F# с выводом типов все дрвольно запутанно и сложно. Х-М там все равно используется сильно модифицированный; AFAIR там вообще разные стратегии вывода типов для разных случаев, ибо поддерживается глобальный вывод типов, а снаружи у нас дотнет.


Лично я даже не видел статьи с описанием. Т.е. известно, что в хаскеле вывод типов InsideOut(X), в скале Colored Local Type Inference, для немерле обсуждаемое описание есть. А Сайм то ли нетеоретик и писать ленится, то ли общая нетеоретическая атмосфера в комьюнити не способствует распространению ссылки на статью и делает ее негуглибельной. На вопрос "как работает вывод типов" отвечают обычно "ну эта, работает он, обычно, сверху вниз и слева направо, значить"

ВВ>Поэтому таки да, такая стратегия как отложенный вывод типа функции там таки используется.


Зависит от того, что вы под этим подразумеваете. Пока может Х-М может и F# а как только появляется сабтайпинг так F# сразу перестает мочь в подавляющем большинстве случаев.
Если вы под этим понимаете "как в немерле", то нет, не используется.

ВВ>И даже *по твоим примерам* хорошо видно, что это не усечение полиморфизма, ибо без применения глобальная функция вида let sum x y = x+y все равно не будет иметь полиморфный тип.


Эта функция не имеет полиморфного типа потому, что + не полиморфный. Неполиморфным он становится в результате ограничения крышечного полиморфизма. Если в хаскеле определить + как не полиморфный, то и функция его использующая станет неполиморфной, что тут удивительного?

ВВ>Все-все выводится по ХМ? В дотнетовой системе типов? Ну-ну. Это про какой-то другой язык рассказываешь, не про F#.


Я же пишу черным по белому, языком пушкина и достоевского на разные лады, что и чем выводится, а что реконструируется и мономорфизуется. В дотнетной системе типов Х-М всего не выведешь, ну так F# и не выводит!

ВВ>Потому что в Хаскелле этого нет, в Хаскелле усечение полиморфизма.


Ну и в F# тоже ограничение полиморфизма. Вы в нем ошибки "велью рестрикшн" никогда не видели что ли?

ВВ>Проблема одна. Нет, вернее, две. Первоначально ты пытался утверждать, что этого нет даже в немерле. Данный вопрос, я так понимаю, мы замяли? Осталось теперь замять вопрос с F# и можно начинать спорить о чем-то другом, как здесь принято.


Я же не могу ваши мысли читать. Когда вы выдумываете термин, я выдвигаю гипотезы-расшифровки. Если это первая гипотеза — то нет ни там, ни там. Если это означает "отложенный вывод типов как в немерле", то очевидно, что в немерле это есть. Ну а в F# этого нет. Если это означает Х-М и ограничение полиморфизма — то это во всех эмелях есть и в хаскеле, а в немерле наоборот нет. В Idris, что характерно, нет ничего из вышеперечисленного.

K>>Иногда F# выводит типы как хаскель, а как немерле никогда, что я продемонстрировал на примерах.

ВВ>На примерах с инлайн? Смешно.

И на примерах без инлайн. Я бы сказал, особенно на примерах без инлайн. Смешно или нет — это к делу не относится. По существу возражения есть?
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.