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

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

S>>файла в программе нет. как объекта, во всяком случае.

K>Как нет? А во что вы пишете/ что читаете?
В вызовы API, полагаю

S>>а "мир"-а нет снаружи.

K>Вот это да! Как же его, нет, когда есть. По крайней мере мне он в ощущениях задан.
Тот что задан в ощущениях, никакой связи с внутрипрограммным World не имеет.

S>>Потому что есть четкое представление о том что этот "модельный мир" это не модель и не мир.

K>Почему не модель? От мира нам требуется только модель времени. Время (точнее, только упорядоченность событий) и моделируется.
не моделируется, а достигается посредством передачи значения.

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

K>Чем лучше? Названием?
да

S>>Но я не понимаю, зачем нужно строить какие-то иллюзии вокруг модели мира внутри программы, если отсутствие чистоты действий не компрометирует хаскель как чистый язык?

K>Затем, чтобы можно было отличать процедуры, нарушающие ссылочную прозрачность от функций, не нарушающих. Это практически важное свойство.
Я отличаю, никаких проблем не вижу, кроме регулярных споров на эту тему.
K>Если руководствоваться вашим определением чистоты — получится, что такую классификацию мы осуществить не сможем.
Это не мое определение.
K>Ведь у вас получается так, что широкий класс функций, которые чистыми не являются — ссылочную прозрачность тем не менее не нарушают. Это неудобно.
Не понимаю о чем речь. Да, ссылочная прозрачность слабее чистоты. Что в этом неудобного?

S>>>>этак можно сказать что fprintf принимает неявно внешний мир и возвращает длину строки и новый мир с файлом.

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

K>Не обеспечивается. Она неявная, никакими ; в коде не определяется.
Верно, неявная.

S>>Прозрачность по ссылкам — это возможность заменить выражение значением. Я уже отвечал VoidEx-у, что не готов рассматривать файл на диске или байты, ушедшие в сеть, в качестве части значения, которым мы заменили выражение.

K>Ну, мы вроде бы обсуждаем ссылочную прозрачность, а не чью-то неготовность что-то рассматривать. Попробуйте ее нарушить записью в файл или хождением байтов по сети без всяких unsafe* — тогда и будет материал для разговора.
Начинаю сердиться. Я только и твержу о том, что комбинирование нечистых действий чисто, следовательно ссылочно прозрачно. А выполнение действий — нечисто и непрозрачно. Но выполнение можно сделать лишь через unsafe*.

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

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

S>>Прозрачность по ссылкам — это возможность заменить выражение значением. Я уже отвечал VoidEx-у, что не готов рассматривать файл на диске или байты, ушедшие в сеть, в качестве части значения, которым мы заменили выражение.

VE>Вообще говоря, мы можем запустить вычисление функции f от 10 в потоке, и в другом потоке мониторить выделенную память, тем самым определяя, вычисляется ли что-то реально, или подставляется готовое значение. При этом f чистая, а реализация вольна мемоизировать по своему усмотрению.
VE>Если f использует всякие newSTRef, то она всё равно останется чистой, и вряд ли можно сказать, что компилятор не имеет права в (f 10, f 10) вычислить её лишь один раз. При этом мы таки можем при желании организовать возможность определить это, но на чистоту f это никак не влияет.
не понимаю, к чему это?

VE>Поэтому я склонен считать, что даже если f посылает данные в сеть, но остается прозрачной по ссылкам (гарантированно, насколько это возможно), то её можно считать чистой и заменять на вычисленное значение.
Если посылает данные в сеть, то ее нельзя заменить вычисленным значением. Данные ведь в сеть не пошлются!!! При замене вызова значением мы должны обеспечить тот же эффект по определению прозрачности.

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

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

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

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

S>>Определение ПП не требует (потенциально) бесконечного кол-ва типов.

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

S>>Нет. Тут я о возможности получать экземпляры типов, которые не были инстанциированы при компиляции.

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

S>>Не понимаю, какое отношение value-type и ref-type имеют к кайндам.

K>Прямое. Это типы типов.
Я бы это назвал видами/категориями/классами типов. Но не типами типов.

S>>Чем оно бесконечнее, чем в C++?

K>Тем, что обсуждаемый код с (потенциально) бесконечным числом типов на C# работает, а на C++ нет.
на C++ потенциальную бесконечность типов мы можем обеспечить во время компиляции, поместив что надо в заголовок и залив на гитхаб.

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

K>В языке с ПП id имеет тип forall a. a -> a множество типов, к которым мы можем применить такое выражение (потенциально) бесконечно. В случае C++ это не так. Множество конечно. Для того, чтоб наблюдать на практике отличия между этими случаями нужно иметь возможность организовать тайплевел-вычисления, которые тут обсуждаются.

В случае C++ по моему ты все-таки завязываешся на реализацию. Вроде стандарт не запрещает реализовать шаблоны так чтобы они
компилировались для любых типов в один и тот же код. Возможно в каком нибудь интерпретаторе C++ (например http://root.cern.ch/drupal/content/cint)
это уже и реализовано.

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

K>module Main where

K>import System.Environment

K>data Nil = Nil

K>data Cons a = Cons Integer a

K>class ScalarProduct a where scalarProduct :: a -> a -> Integer

K>instance ScalarProduct Nil where 
K>    scalarProduct Nil Nil = 0
K>instance ScalarProduct a => ScalarProduct (Cons a) where 
K>    scalarProduct (Cons n1 a1) (Cons n2 a2) = n1 * n2 + scalarProduct a1 a2

K>test :: Integer -> Integer
K>test n = test' n 0 Nil Nil where
K>  test' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer
K>  test' 0 _ as bs = scalarProduct as bs
K>  test' n i as bs = test' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)
K>--  test' n i as bs = test' (n-1) (i+1) as (Cons (i^2) bs) 

K>main = print . test . read . head =<< getArgs

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

test :: Integer -> Integer
test n = scalarProduct as bs
  where
    make_lst _ 0 _ xs = xs
    make_lst f n i xs = make_lst f (n-1) (i+1) (Cons (f i) xs)
    as = make_lst (\x -> 2 * x + 1) n 0 Nil
    bs = make_lst (^2) n 0 Nil

Грит:

    Occurs check: cannot construct the infinite type: a2 = Cons a2
    In the second argument of `Cons', namely `xs'
    In the fourth argument of `make_lst', namely `(Cons (f i) xs)'
    In the expression: make_lst f (n - 1) (i + 1) (Cons (f i) xs)

Я что-то не так изменил, или haskell-е нет ПП?
Вроде как и в твоём коде всё известно на этапе компиляции.
Компилятор: ghc 7.0.3 из Kubuntu 11.10

Изначаально я хотел посмотреть что будет при такой сигнатуре:

test :: Integer -> Integer -> Integer
test n m = scalarProduct as bs
  where
    make_lst _ 0 _ xs = xs
    make_lst f n i xs = make_lst f (n-1) (i+1) (Cons (f i) xs)
    as = make_lst (\x -> 2 * x + 1) n 0 Nil
    bs = make_lst (^2) m 0 Nil

функция скомпилится или нет? Ведь доказать эквивалентность типов можно или нельзя в зависимости от того, как мы её вызываем.
Если скомпилится в любом случае, то очивидно, проверка должна быть вынесена в rantime.
Можно похожим образом изменить код для C# и Java, и посмотреть используется ли там поддержка в rantime или всё полная статика.
И если таки rantime, то есть ли там вообще проверки эквивалентности и какие.

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

VE>>Вообще говоря, мы можем запустить вычисление функции f от 10 в потоке, и в другом потоке мониторить выделенную память, тем самым определяя, вычисляется ли что-то реально, или подставляется готовое значение. При этом f чистая, а реализация вольна мемоизировать по своему усмотрению.
VE>>Если f использует всякие newSTRef, то она всё равно останется чистой, и вряд ли можно сказать, что компилятор не имеет права в (f 10, f 10) вычислить её лишь один раз. При этом мы таки можем при желании организовать возможность определить это, но на чистоту f это никак не влияет.
S>не понимаю, к чему это?

К тому, что даже не вызывающее сомнений чистое вычисление не более и не менее чисто, чем вычисление через посыл данных по сети.

VE>>Поэтому я склонен считать, что даже если f посылает данные в сеть, но остается прозрачной по ссылкам (гарантированно, насколько это возможно), то её можно считать чистой и заменять на вычисленное значение.
S>Если посылает данные в сеть, то ее нельзя заменить вычисленным значением. Данные ведь в сеть не пошлются!!!

И оперативная память не выделится, если заменить чистую f от 10 на запомненное где-то значение. Ну и что?

S>При замене вызова значением мы должны обеспечить тот же эффект по определению прозрачности.

Какой такой эффект у факториала?
Ты понимаешь, что твоя отсылка "в википедии написано, что такое IO" означает, что в википедии должно быть не "например, вывод на экран", а чёткий такой список, что именно IO, а что нет. И более того, способ определить для гипотетического случая, IO это будет или нет. А там такого нет, там всё на интуицию завязано.
f вычисляет факториал, если есть гарантия, что для 6! вернёт 120, вычисляй ты хоть 300 раз подряд, то она referential transparent, а как именно она реализована — детали реализации. Что мешает использовать файл как оперативную память?

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

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

Эти определения натыкаются на термин outside world, который не определён.
Работа с памятью определяется рантаймом, и поэтому мы считаем, что это не эффект. Ну ок. Делаем рантайм, который общается с кластером, загружает туда код, получает оттуда результат. Это что? IO? Side effect? С т.з. языка нет, это детали реализации. С т.з. зрения википедии ответа просто банально нет.

An expression is said to be referentially transparent if it can be replaced with its value without changing the behavior of a program (in other words, yielding a program that has the same effects and output on the same input).

Более того, у них там рекурсия какая-то просто.

If all functions involved in the expression are pure functions, then the expression is referentially transparent. Also, some impure functions can be included in the expression if their values are discarded and their side effects are insignificant.

Тут поле для демагогии открывается. В контексте вычисления факториала посылка данных в сеть столь же бессодержательна (insignificant), как и выделение памяти.

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

T>Если чуть измениь код функции test на эквивалентный, то компилятор ругаицця:

Вы хотите прозвести на меня впечатление способностью нерабочий код написать? Могли бы просто закомментировать сигнатуру типа у test' и получить ошибку "cannot construct the infinite type", а не вкладывать столько труда. И, главное, какое это имеет отношение к полиморфизму и как отменяет работоспособность приведенного выше кода?

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

T>Если скомпилится в любом случае, то очивидно, проверка должна быть вынесена в rantime.
T>Можно похожим образом изменить код для C# и Java, и посмотреть используется ли там поддержка в rantime или всё полная статика.
T>И если таки rantime, то есть ли там вообще проверки эквивалентности и какие.

Удивительно просто, как можно так отчаянно цеплятся за рантайм. Как вы вообще представляете себе механизм, откладывающий эту проверку типов в GHC в рантайм? Это святой дух? Может магия вуду? Мне правда интересно.

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

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

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

S>Ну вот в C# мы можем применять типы в рантайме. Хотя это означает лишь "докомпиляцию" джитом.

Все типы в обсуждаемых примерах применяются в компайл-тайм.

S>Я бы это назвал видами/категориями/классами типов.

kind иногда переводят как "вид". Классами типов вообще совершенно другие вещи называют.

S>Но не типами типов.

Но почему?

S>на C++ потенциальную бесконечность типов мы можем обеспечить во время компиляции, поместив что надо в заголовок и залив на гитхаб.

Эта шутка тут уже была:
>Я могу (потенциально) написать id в foo.h и использовать его в бесконечном количестве программ по одному разу.
Или шутка, повторенная дважды, становится в два раза смешнее?
Ответ мне копипастить или сами прочитаете?

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

K>>Как нет? А во что вы пишете/ что читаете?
S>В вызовы API, полагаю

И в каком АПИ есть функции прочтиТоНеЗнаюЧто и сохраниТудаНеЗнаюКуда?

S>Тот что задан в ощущениях, никакой связи с внутрипрограммным World не имеет.

Это ваша позиция по любой модели или конкретно по этой? Если по этой — что именно вас не устраивает.

S>не моделируется

Почему?

S>Не понимаю о чем речь. Да, ссылочная прозрачность слабее чистоты. Что в этом неудобного?

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

S>Это не мое определение.

А чье? Замечание про "семантическую наблюдаемость" из общепринятого вы с негодованием отвергаете.

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

А с этим разве спорит кто-то?

S>А выполнение действий — нечисто и непрозрачно. Но выполнение можно сделать лишь через unsafe*.

Утверждение опровергается одним примером:

main = print 42

Выполнение есть — unsafe* нет. Как же так?

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

FR>В случае C++ по моему ты все-таки завязываешся на реализацию. Вроде стандарт не запрещает реализовать шаблоны так чтобы они
FR>компилировались для любых типов в один и тот же код.

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

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

T>>Если чуть измениь код функции test на эквивалентный, то компилятор ругаицця:
K>Вы хотите прозвести на меня впечатление способностью нерабочий код написать?
Нет. Я хочу понять, что именно ты понимаешь под Полиметрическим Полиморфизмом.
Чем мой вариант настолько отличается от твоего, что твой является ПП и компилится, а мой нет и нет.
Это моё непонимание или глюк в компиляторе?
Как можно преобразовать мой код (1-ый и 2-ой) чтобы они компилились?

K>Мы вроде бы обсудили уже, что для обнаружения (потенциальной) бесконечности типов тут используются тайплевел-вычисления, а это штука довольно хрупкая и костыльная в хаскеле.
Если ПП настолько сложная весчь, что даже к 7-ой версии haskell её неосилил, то кого-же использовать как эталон?
Неужели C#?

T>>Если скомпилится в любом случае, то очивидно, проверка должна быть вынесена в rantime.
T>>Можно похожим образом изменить код для C# и Java, и посмотреть используется ли там поддержка в rantime или всё полная статика.
T>>И если таки rantime, то есть ли там вообще проверки эквивалентности и какие.
K>Удивительно просто, как можно так отчаянно цеплятся за рантайм. Как вы вообще представляете себе механизм, откладывающий эту проверку типов в GHC в рантайм? Это святой дух? Может магия вуду? Мне правда интересно.
Мне показалось, что я придумал отличный тест, который показывает влияние рантайма на реализацию ПП.
С ghc вроде бы всё понятно — он не может скомпилить даже 1-ый мой пример, стало быть полная поддержка ПП даже времени компиляции у него под вопросом. А для рантайма — и вовсе нет или нужен другой тест.

Ну, или ты внятно объяснишь, почему мои пример 1 и 2 не являются ПП, а стало быть и уточнишь его определение.
Так же было бы очень интересно узнать твоё мнение, почему эти примеры нельзя (или таки можно, тогда как) конвертировать в тру-языки поддерживающие ПП, такие как C# и Java.

П. С. Чтобы не было недопонимания, под примером 1 и 2, я понимаю соответственно
Пример 1:

test :: Integer -> Integer
test n = scalarProduct as bs
  where
    make_lst _ 0 _ xs = xs
    make_lst f n i xs = make_lst f (n-1) (i+1) (Cons (f i) xs)
    as = make_lst (\x -> 2 * x + 1) n 0 Nil
    bs = make_lst (^2) n 0 Nil

Пример 2:

test :: Integer -> Integer -> Integer
test n m = scalarProduct as bs
  where
    make_lst _ 0 _ xs = xs
    make_lst f n i xs = make_lst f (n-1) (i+1) (Cons (f i) xs)
    as = make_lst (\x -> 2 * x + 1) n 0 Nil
    bs = make_lst (^2) m 0 Nil

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

Они не компилятся не потому, что ПП или не ПП, а потому что нет compile-time доказательства того, что длины таки равные.
На Agda перепиши.

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

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

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

VE>К тому, что даже не вызывающее сомнений чистое вычисление не более и не менее чисто, чем вычисление через посыл данных по сети.
Это ты на невыполнение какого критерия чистоты намекаешь? На семантически обозримый сайд эффект что ли?

S>>Если посылает данные в сеть, то ее нельзя заменить вычисленным значением. Данные ведь в сеть не пошлются!!!

VE>И оперативная память не выделится, если заменить чистую f от 10 на запомненное где-то значение. Ну и что?
Выделение памяти у нас превартилось в семантически обозримый side effect? С каких пор?

S>>При замене вызова значением мы должны обеспечить тот же эффект по определению прозрачности.

VE>Какой такой эффект у факториала?
VE>Ты понимаешь, что твоя отсылка "в википедии написано, что такое IO" означает, что в википедии должно быть не "например, вывод на экран", а чёткий такой список, что именно IO, а что нет. И более того, способ определить для гипотетического случая, IO это будет или нет. А там такого нет, там всё на интуицию завязано.
по поводу четкого списка, я полагаю что ты понимаешь, что его составить невозможно с точностью до идей о нагревании атмосферы. А по поводу интуиции — все-таки ориентировано на неглупых людей, которые способны провести границы между системой и остальным миром.

VE>f вычисляет факториал, если есть гарантия, что для 6! вернёт 120, вычисляй ты хоть 300 раз подряд, то она referential transparent, а как именно она реализована — детали реализации.
Ты путаешь referential transparency с детерминированностью. Если есть гарантия что результат будет тот же и не будет зависеть от ввода через I/O или скрытых состояний, то это есть детерминированность, а не ссылочная прозрачность. Детерминированной функции портить мир можно. Ссылочно прозрачному выражению — нельзя.

VE>Что мешает использовать файл как оперативную память?
Ничего. Только детерминированности не будет, т.к. общаешься с файлом через I/O. А нет детерминированности — нет и прозрачности.

S>>Определения с тобой не согласны. Я лишь пытаюсь это обозначить.

VE>Нет, ты со мной не согласен. Я задал кучу вопросов, на которые такое определение ответить не в состоянии.
Мне казалось, что я на все ответил, опираясь на определение.

VE>Эти определения натыкаются на термин outside world, который не определён.

VE>Работа с памятью определяется рантаймом, и поэтому мы считаем, что это не эффект. Ну ок. Делаем рантайм, который общается с кластером, загружает туда код, получает оттуда результат. Это что? IO? Side effect? С т.з. языка нет, это детали реализации. С т.з. зрения википедии ответа просто банально нет.
Ответа не может быть для тех, кто не может провести границу системы. Смотри:
а) твоя программа запрашивает значение факториала у кластера путем отправки голубя. Это ввод/вывод.
б) твоя программа выполняется рантаймом на кластере путем посылки дилижансов, почтовых голубей и т.п. к кластеру и обратно прозрачно для программы. Т.е. сама программа никого не посылает. Тогда ввода/вывода формально нет, и если голуби работают семантически необозримо, то все формально чисто. Даже если у кочегара дилижанса не выдержала селезенка и его семье придется выплачивать пособие.

VE>

VE>An expression is said to be referentially transparent if it can be replaced with its value without changing the behavior of a program (in other words, yielding a program that has the same effects and output on the same input).

Спасибо, но я заглядываю в него практически каждый раз, когда отвечаю.

VE>Более того, у них там рекурсия какая-то просто.

VE>

VE>If all functions involved in the expression are pure functions, then the expression is referentially transparent. Also, some impure functions can be included in the expression if their values are discarded and their side effects are insignificant.

VE>Тут поле для демагогии открывается. В контексте вычисления факториала посылка данных в сеть столь же бессодержательна (insignificant), как и выделение памяти.
Посылка данных в сеть — это output через I/O девайс. А выделение памяти не является семантически обозримым сайд эффектом.

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

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

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

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

K>Код никому не должен "не быть специализирован", он может быть специализирован для оптимизации, и на практике так и происходит.
Если на практике происходит специализация, то это не ПП, а ad-hoc.
K>Важно, чтоб он работал для любого типа (того кайнда, для которого полиморфизм вообще работает). А из "любого типа" и следует (потенциальная) бесконечность. Ну, или — если не согласны — двайте верхнюю оценку на число "любых типов".
(Потенциальная) — это значит что мне не потребуется специализировать для работы с еще одним любым типом. А если мне в программе нужно всего 10 типов и не нужно бесконечность, то это не мои проблемы.

K>Мало того, это не просто теоретизирование — показаны примеры, которые используют именно это свойство полиморфизма и которые предсказуемо работают в языках с ПП и не работают в языке без ПП. И вы как-то умудряетесь это игнорировать утверждая, что ничего ниоткуда не следует.
А вы умудряетесь игнорировать то что определение ПП не требует бесконечности.

S>>Ну вот в C# мы можем применять типы в рантайме. Хотя это означает лишь "докомпиляцию" джитом.

K>Все типы в обсуждаемых примерах применяются в компайл-тайм.
Но не в C#.

S>>Я бы это назвал видами/категориями/классами типов.

K>kind иногда переводят как "вид". Классами типов вообще совершенно другие вещи называют.
Я не про type class-ы.

S>>Но не типами типов.

K>Но почему?
Потому что кайндов в дотнете нет. Не хочу еще и по этому поводу спорить.

S>>на C++ потенциальную бесконечность типов мы можем обеспечить во время компиляции, поместив что надо в заголовок и залив на гитхаб.

K>Эта шутка тут уже была:
>>Я могу (потенциально) написать id в foo.h и использовать его в бесконечном количестве программ по одному разу.
K>Или шутка, повторенная дважды, становится в два раза смешнее?
K>Ответ мне копипастить или сами прочитаете?

Нет. Не в (потенциально) бесконечном кол-ве программ. Так разницу не обнаружить. А в одной программе для (потенциально) бесконечного кол-ва типов. Как в примере выше.

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

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

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

K>>>Как нет? А во что вы пишете/ что читаете?
S>>В вызовы API, полагаю

K>И в каком АПИ есть функции прочтиТоНеЗнаюЧто и сохраниТудаНеЗнаюКуда?
В любом. Имя файла или его хэндл — это в точности НеЗнаюЧто/Куда. Конкретика лежит по другую сторону API.

S>>Тот что задан в ощущениях, никакой связи с внутрипрограммным World не имеет.

K>Это ваша позиция по любой модели или конкретно по этой? Если по этой — что именно вас не устраивает.
Конкретно по этой. Не устраивает то что общего с миром у нее не больше, чем у слова "затычка".

S>>не моделируется

K>Почему?
По факту

S>>Не понимаю о чем речь. Да, ссылочная прозрачность слабее чистоты. Что в этом неудобного?

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

S>>Это не мое определение.

K>А чье? Замечание про "семантическую наблюдаемость" из общепринятого вы с негодованием отвергаете.
Я негодую когда вы пытаетесь говорить о семантической прозрачности ввода/вывода.

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

K>А с этим разве спорит кто-то?
Вы с этим не спорите, но пытаетесь этим аргументировать, будто я против чистоты комбинирования.

S>>А выполнение действий — нечисто и непрозрачно. Но выполнение можно сделать лишь через unsafe*.

K>Утверждение опровергается одним примером:
Оно им подтверждается

K>

K>main = print 42
K>

K>Выполнение есть — unsafe* нет. Как же так?
Я не вижу в этом коде выполнения. Если что, main не выполняет построенное им действие. Точнее так: void main() — выполняет, но не строит. main::IO() — строит, но не выполняет. Удивлен и смущен, что мне приходится об этом упоминать.

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

_>Кстати, что касается ленивости в списках, то в том же Питоне есть некая забавная попытка ленивости — две отдельных функции range и xrange.

Отстаёте от жизни. В 3-м осталась только range, которая во 2-м была xrange, то есть со внутренним итератором. Для эффекта, аналогичного range() во 2-м, надо писать list(range()). Вообще в поздних 2-х и 3-х многое сдвинуто в сторону итераторов.
Не всегда это, однако, хорошо — оптимизация по производительности часто показывает противоположные решения: не сильно длинные списки эффективнее итераторов с yield'ом.

Здравствуйте, VoidEx, Вы писали:
VE>Они не компилятся не потому, что ПП или не ПП, а потому что нет compile-time доказательства того, что длины таки равные.
VE>На Agda перепиши.
Можно ли поподробнее?
Почему, в версии

K>test :: Integer -> Integer
test n = test' n 0 Nil Nil where
  test' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer
  test' 0 _ as bs = scalarProduct as bs
  test' n i as bs = test' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)

можно доказать что длины as и bs равны, а в версии

test :: Integer -> Integer
test n = scalarProduct as bs
  where
    make_lst _ 0 _ xs = xs
    make_lst f n i xs = make_lst f (n-1) (i+1) (Cons (f i) xs)
    as = make_lst (\x -> 2 * x + 1) n 0 Nil
    bs = make_lst (^2) n 0 Nil

этого доказать нельзя?

Я межу ними различия не вижу, но для компилятора оно есть.
Можешь объяснить его?
В чём оно? Это принципиальное/теоретическое различие, или это особенности компилятора?

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

S>Выделение памяти у нас превартилось в семантически обозримый side effect? С каких пор?

Ты спрашиваешь, как программе определить, выделяется ли память?

S>>>При замене вызова значением мы должны обеспечить тот же эффект по определению прозрачности.

S>А по поводу интуиции — все-таки ориентировано на неглупых людей, которые способны провести границы между системой и остальным миром.

Математики не потому составляют чёткие определения, что они глупые, а как раз наоборот, потому что понимают, что дьявол в деталях.
Может, в определение напишем "side-effect — то, что неглупый человек считает side-effect'ом"?

S>Ты путаешь referential transparency с детерминированностью. Если есть гарантия что результат будет тот же и не будет зависеть от ввода через I/O или скрытых состояний, то это есть детерминированность, а не ссылочная прозрачность. Детерминированной функции портить мир можно. Ссылочно прозрачному выражению — нельзя.

Не путаю. Она и не портит, мир живёт себе как жил. Ничем не хуже, чем с выделенной памятью.

VE>>Что мешает использовать файл как оперативную память?
S>Ничего. Только детерминированности не будет, т.к. общаешься с файлом через I/O. А нет детерминированности — нет и прозрачности.

Почему это не будет? На n! при сотне вызовов возвращает верное значение? Да. Так что ж тогда?

S>>>Определения с тобой не согласны. Я лишь пытаюсь это обозначить.

VE>>Нет, ты со мной не согласен. Я задал кучу вопросов, на которые такое определение ответить не в состоянии.
S>Мне казалось, что я на все ответил, опираясь на определение.

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

VE>>Эти определения натыкаются на термин outside world, который не определён.
S>
VE>>Работа с памятью определяется рантаймом, и поэтому мы считаем, что это не эффект. Ну ок. Делаем рантайм, который общается с кластером, загружает туда код, получает оттуда результат. Это что? IO? Side effect? С т.з. языка нет, это детали реализации. С т.з. зрения википедии ответа просто банально нет.
S>Ответа не может быть для тех, кто не может провести границу системы. Смотри:
S>а) твоя программа запрашивает значение факториала у кластера путем отправки голубя. Это ввод/вывод.
S>б) твоя программа выполняется рантаймом на кластере путем посылки дилижансов, почтовых голубей и т.п. к кластеру и обратно прозрачно для программы. Т.е. сама программа никого не посылает. Тогда ввода/вывода формально нет, и если голуби работают семантически необозримо, то все формально чисто. Даже если у кочегара дилижанса не выдержала селезенка и его семье придется выплачивать пособие.

А что если работает рантайм, но программа имеет возможность косвенно следить за её работой? Ну, как с памятью.
Или обратный эффект. Что, если я могу рантайм расширять? Ну вот например ввёл доставки голубем, и с т.з. языка это считается runtime extension и даёт те же гарантии, что и работа с памятью. А дальше компилятор на основе метаданных выбирает реализацию сам — то ли память, то ли голуби.
Я не думаю, что это такой уж надуманный пример, вон взять Nemerle 2, который будет как бы инструмент для создания языков. Там может понадобиться нечто подобное. В базовом языке (который ещё и грязный) у нас будет всё превращаться в голубиную почту, но в исходном чистом ДСЛ это будет обычное вычисление.

S>Посылка данных в сеть — это output через I/O девайс. А выделение памяти не является семантически обозримым сайд эффектом.

В чём разница? Увидеть можно и то, и другое. Изнутри программы.

S>Что по поводу insignificant сайд эффекта — так это представь вычисление факториала со внешним мутабельным аккумулятором. Такая функция будет формально impure, но включенная в выражение таким образом, что бы изменения не распространялись за пределы выражения, ее побочный эффект будет незначителен для того, кто ожидает результат выражения.

Можно ещё представить себе вычисление огроменного списка. Формально он pure, но запусти их 3 сразу и памяти не хватит. И это оказывается очень так значительно для того, кто ожидает результат вычисления. Но это лирика.
А можно опять вернуться к голубиной почте, а лучше к temporary файл. Можно создать temporary file (имя которому генерирует ОСь, и имя которого неизвестно никому, только handle открывшему процессу), поиспользовать для вычислений и закрыть (после чего он может удалиться, а может и нет, зависит от флагов открытия). Такая функция чиста? Вроде ввод-вывод есть, но побочный эффект необнаруживаем.

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

T>Здравствуйте, VoidEx, Вы писали:
VE>>Они не компилятся не потому, что ПП или не ПП, а потому что нет compile-time доказательства того, что длины таки равные.
VE>>На Agda перепиши.
T>Можно ли поподробнее?

Можно.

T>Почему, в версии
T>

K>>test :: Integer -> Integer
T>test n = test' n 0 Nil Nil where
T>  test' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer
T>  test' 0 _ as bs = scalarProduct as bs
T>  test' n i as bs = test' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)
T>

T>можно доказать что длины as и bs равны,

По определению. Тип функции test' явно говорит, что 3 и 4 аргументы совпадают по типу, а таковые одинаковы только у списков с равной длиной (не встроенных списков, а нами определённых).
Поэтому приходится использовать рекурсию. Nil имеет тип List b Zero или как-то так (я исходник изначальный не нашёл), где b — тип элементов, Zero — длина. Когда мы во второй строке для test' к каждому списку делаем Cons, то для двух List b n (т.е. одинаковой длины списки) для любого n мы получаем два List b (Succ n), которые опять же одной длины (очевидно), и это компилируется.
То, что они одной длины, как-то отдельно доказывать не надо банально потому, что это доказательство тривиально выводится из определения списка (при таком построении).
Однако возможности Haskell в этой области крайне скудные, поэтому для сложных случаев компилятор уже понять ничего не может, но это не относится к ПП, это относится к невозможности дать подсказки компилятору и как-то выразить известный нам факт.

а в версии
T>

T>test :: Integer -> Integer
T>test n = scalarProduct as bs
T>  where
T>    make_lst _ 0 _ xs = xs
T>    make_lst f n i xs = make_lst f (n-1) (i+1) (Cons (f i) xs)
T>    as = make_lst (\x -> 2 * x + 1) n 0 Nil
T>    bs = make_lst (^2) n 0 Nil
T>

T>этого доказать нельзя?

На Агде можно. В Haskell ваш make_lst возвращает список неизвестной длины. Т.е. вам-то очевидно, какой, но компилятору — нет. А уж то, что они ещё и одинаковые у двух списков — тем более. В первом же варианте у вас в типе test' заложен факт равности длин списков, пусть сама длина и неизвестна, да и не нужна.

T>В чём оно? Это принципиальное/теоретическое различие, или это особенности компилятора?

Принципиальное в том, что число и число уровня типа (Zero, Succ Zero...) — это разные вещи. То, что вам ясно, что список получился и там, и там длиной n, компилятор понять не в состоянии.
В первом случае мы берем за базу явно равные Zero Zero (это компилятор понимает), а потом по ним строим через Succ и Succ (и это тоже компилятору понятно).
Если ничего не путаю, то отличие и теоретическое, так как в Haskell нет зависимых типов (типы, зависящие от термов), в данном случае они эмулируются через вычисления над типами (типы, зависимые от типов).

В Агде с зависимыми типами такое вполне возможно. Вот, кстати, пример закольцованного счётчика (внизу ссылки на код) от 0 до 255 с доказательствами закольцованности и того, что прибавление и отнимание взаимно уничтожают друг друга. Доказательство выражено в виде обычной функции (+1 и -1 — это не сложение вычитание, это оператор (цельный, но пользовательский) инкремента и декремента):
+1-1₀ : ∀ {n} → (k : Counter n) → k +1 -1 ≅ k
И компилятор сможет это использовать (ну или мы ему подскажем).

Соответственно, для примера выше мы могли бы написать доказательство, что длины списков make_lst n и make_lst m равны, если n равно m. Получится — скомпилируется.

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

T>Я хочу понять, что именно ты понимаешь под Полиметрическим Полиморфизмом.

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

T>Чем мой вариант настолько отличается от твоего

Самое существенно отличие в том, что "мой" код содержит теорему, утверждающую о том, что списки имеют одинаковую длину, т.е. такой вот тип:

test' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer

И конструктивное доказательство (с оговорками) утверждения. Т.е. терм, населяющий этот тип:

test' 0 _ as bs = scalarProduct as bs
test' n i as bs = test' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)

Ваш, с другой стороны, не содержит ни первого, ни второго.

T>что твой является ПП и компилится, а мой нет и нет.

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

T>Как можно преобразовать мой код (1-ый и 2-ой) чтобы они компилились?

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

T>Если ПП настолько сложная весчь, что даже к 7-ой версии haskell её неосилил, то кого-же использовать как эталон?

ПП (ML-style) совсем не сложная вещь, проще шаблонов. Сложные вещи нужны для демонстрации разницы.

T>Мне показалось, что я придумал отличный тест, который показывает влияние рантайма на реализацию ПП.

ПП — это статическая типизация. Рантайм на нее никак не влияет. Может использоваться для оптимизаций, но на семантику языка не влияет.