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

V>>Ну и тем более не доверяй Вики. ))
S>Конечно, особенно если она совпадает с классификацией, на которую ссылается. Это особо подозрительно.

Вики противоречит самой себе на одной и той же странице.
Это не подозрительно, это банально смешно. ))


V>>Я вот всё жду, когда вот эту опенсорсную книгу докончат:
V>>https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf
V>>а потом переведут на русский.
V>>Этой книге можно верить.
S>За ссылку спасибо, буду верить. Но вот что касается конкретно parametric/ad-hoc — там верить нечему, такие наборы букв не встречаются. Сложно руководствоваться книгой для отделения мух от котлет, если ни те ни другие в книге не помянуты.

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

A polymorphic function is one which takes a type as one of its arguments ...

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


V>>А когда некоторые авторы начинают разбирать на молекулы конкретно разновидности всего-навсего параметрического полиморфизма, чудовищно плавая при этом по всему вокруг и повторяя всевозможные заблуждения и городские легенды, то мне становится тошно. ))
S>Заблуждения при этом это то, с чем твое пролетарское чутье не согласно?

Если авторы не согласны друг с другом, то кто-то из них ошибается, верно?
А моё "чутьё" тут лишь выбирает "верную сторону".
Например, книга по ссылке на сегодня — наиболее полная классификация из теории типов.

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


V>>И да. Некоторые авторы в запале "прозрения" называют параметрический полиморфизм "истинным полиморфизмом".
V>>В общем случае это не так. В общем случае речь идёт о "зависимом функциональном типе" (упомянут выше).
V>>Усё. Остальное зависит от техник, частностей и т.д.
S>То есть, ты в этой книге упоминания ad-hoc тоже не нашел, и потому все остальные упоминания стали мутными.

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

V>>Запомним это определение. Оно верное до тех пор, пока "исполнение" будет означать "исполнение по исходнику", а не по машинным кодам. Где-то я даже встречал "физическое исполнение" и тоже ужасался. )) В книге по ссылке говорится:
V>>

V>>A polymorphic function is one which takes a type as one of its arguments, and then acts on elements of that type.

V>>Заметь, и параметрический и ad hoc-полиморфизмы прекрасно подходят под определение.
S>Ничего нового. Это устоявшееся определение полиморфизма вообще. Например, у Luca Cardelli
S>

S>Polymorphic functions are functions whose operands (actual parameters) can have more than one type.

Что НЕ эквивалентно определению из данной мною книги.
Согласно неё полиморфная ф-ия берет два аргумента на входе:

An example is the polymorphic identity function id: ∏(A:U) A → A, which we define by id :≡ λ(A : U).λ(x : A).x.

На всяк случай, запись через лямбда-абстракции эквивалентна вот этому объявлению:
function id(A : U, x : A).
Где U — семейство типов, А — конкретный тип, x — единственный аргумент-значение некоей функции с идентификатором id.


S>Деление на parametric/ad-hoc обычно следует абзацем ниже. Но у HOTT до этого не дошло.

Зато "дошло" до отсечения из "полиморфизма" части классификации твоего Луки Карделли.
Причем, легким и непринуждённым движением руки. ))

Я правильно понимаю, что ты ссылаешься на вот эту его работу?
http://www.lucacardelli.name/Papers/TypefulProg.pdf
ы-ы-ы, как грится:

In ad hoc polymorphism a function can behave in arbitrarily different ways on objects of different types. We shall ignore this view here, and consider only generic polymorphism where a function behaves in some uniform way over all the relevant types.

Этот Лука вообще отвергает ad hoc как разновидность полиморфизма, в то время как согласно Hott — это несомненно разновидность полиморфизма.

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

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


V>>В первом случае мы напишем единственное тело ф-ии, которое сможет обслуживать, допустим, все типы из данной вселенной.
V>>Во втором случае мы для одной и той же ф-ии напишем несколько версий тел — под разные типы из данной вселенной (или их семейства — подвселенных).
S>Верно

Ну и слава богу.


V>>Тут надо сделать паузу и обратить внимание, что в последнем случае, когда речь идёт об обслуживании некоего ограниченного семейства типов из вселенной, то опять получается параметрический полиморфизм, но уже на вселенной меньшего ранга.(*)
S>Верно. Но ты потерял чистоту квантора ∀.

Я ничего не терял. Я же сразу тебе сказал, что спор сейчас пойдёт о "необходимом" vs "достаточном".
Сразу — как только увидел твою цитату из хаскель-вики.

Это же было как на ладони, там получались ровно два сценария:
— или ты соглашаешься, что не правильно понял про ad hoc-полиморфизм;
— или начинаешь спекулировать насчет "необходимом" vs "достаточном"... и что самое обидное — так и вышло (С).

Моё предупреждение не сработало. Пичалька...

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

V>>Ну и тем более не доверяй Вики. ))
S>Конечно, особенно если она совпадает с классификацией, на которую ссылается. Это особо подозрительно.

Вики противоречит самой себе на одной и той же странице.
Это не подозрительно, это банально смешно. ))


V>>Я вот всё жду, когда вот эту опенсорсную книгу докончат:
V>>https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf
V>>а потом переведут на русский.
V>>Этой книге можно верить.
S>За ссылку спасибо, буду верить. Но вот что касается конкретно parametric/ad-hoc — там верить нечему, такие наборы букв не встречаются. Сложно руководствоваться книгой для отделения мух от котлет, если ни те ни другие в книге не помянуты.

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

A polymorphic function is one which takes a type as one of its arguments ...

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


V>>А когда некоторые авторы начинают разбирать на молекулы конкретно разновидности всего-навсего параметрического полиморфизма, чудовищно плавая при этом по всему вокруг и повторяя всевозможные заблуждения и городские легенды, то мне становится тошно. ))
S>Заблуждения при этом это то, с чем твое пролетарское чутье не согласно?

Если авторы не согласны друг с другом, то кто-то из них ошибается, верно?
А моё "чутьё" тут лишь выбирает "верную сторону".
Например, книга по ссылке на сегодня — наиболее полная классификация из теории типов.

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


V>>И да. Некоторые авторы в запале "прозрения" называют параметрический полиморфизм "истинным полиморфизмом".
V>>В общем случае это не так. В общем случае речь идёт о "зависимом функциональном типе" (упомянут выше).
V>>Усё. Остальное зависит от техник, частностей и т.д.
S>То есть, ты в этой книге упоминания ad-hoc тоже не нашел, и потому все остальные упоминания стали мутными.

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

V>>Запомним это определение. Оно верное до тех пор, пока "исполнение" будет означать "исполнение по исходнику", а не по машинным кодам. Где-то я даже встречал "физическое исполнение" и тоже ужасался. )) В книге по ссылке говорится:
V>>

V>>A polymorphic function is one which takes a type as one of its arguments, and then acts on elements of that type.

V>>Заметь, и параметрический и ad hoc-полиморфизмы прекрасно подходят под определение.
S>Ничего нового. Это устоявшееся определение полиморфизма вообще. Например, у Luca Cardelli
S>

S>Polymorphic functions are functions whose operands (actual parameters) can have more than one type.

Что НЕ эквивалентно определению из данной мною книги.
Согласно неё полиморфная ф-ия берет два аргумента на входе:

An example is the polymorphic identity function id: ∏(A:U) A → A, which we define by id :≡ λ(A : U).λ(x : A).x.

На всяк случай, запись через лямбда-абстракции эквивалентна вот этому объявлению:
function id(A : U, x : A) : A => x.
Где U — семейство типов, А — конкретный тип, x — единственный аргумент-значение некоей функции с идентификатором id.


S>Деление на parametric/ad-hoc обычно следует абзацем ниже. Но у HOTT до этого не дошло.

Зато "дошло" до отсечения из "полиморфизма" части классификации твоего Луки Карделли.
Причем, легким и непринуждённым движением руки. ))

Я правильно понимаю, что ты ссылаешься на вот эту его работу?
http://www.lucacardelli.name/Papers/TypefulProg.pdf
ы-ы-ы, как грится:

In ad hoc polymorphism a function can behave in arbitrarily different ways on objects of different types. We shall ignore this view here, and consider only generic polymorphism where a function behaves in some uniform way over all the relevant types.

Этот Лука вообще отвергает ad hoc как разновидность полиморфизма, в то время как согласно Hott — это несомненно разновидность полиморфизма.

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

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


V>>В первом случае мы напишем единственное тело ф-ии, которое сможет обслуживать, допустим, все типы из данной вселенной.
V>>Во втором случае мы для одной и той же ф-ии напишем несколько версий тел — под разные типы из данной вселенной (или их семейства — подвселенных).
S>Верно

Ну и слава богу.


V>>Тут надо сделать паузу и обратить внимание, что в последнем случае, когда речь идёт об обслуживании некоего ограниченного семейства типов из вселенной, то опять получается параметрический полиморфизм, но уже на вселенной меньшего ранга.(*)
S>Верно. Но ты потерял чистоту квантора ∀.

Я ничего не терял. Я же сразу тебе сказал, что спор сейчас пойдёт о "необходимом" vs "достаточном".
Сразу — как только увидел твою цитату из хаскель-вики.

Это же было как на ладони, там получались ровно два сценария:
— или ты соглашаешься, что не правильно понял про ad hoc-полиморфизм;
— или начинаешь спекулировать насчет "необходимом" vs "достаточном"... и что самое обидное — так и вышло (С).

Моё предупреждение не сработало. Пичалька...