[ЖЖ] *морфизм, Haskell & Lisp

> И самое главное в рамках XML есть XSD и Schema, которая используется для описания его структуры. В терминах, очень похожих на определение АТД.

значит, абстракция «список» дырявая и не совсем адекватная — не описывает схему и DTD

И кстати, это касается не только XML: например, любой сложный конфигурационный файл является АТД.

и так далее, вплоть до правила Гринспуна — конфиги на лиспе?

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

утверждение нестрогое, так, ощущение, а не доказательство. Синтаксис без семантики. Семантикой могли бы быть аксиомы и базовые понятия + логика, но логик много разных. Тем не менее, если зафиксировать базу и логику, то надстройка (множество выводимых из базы теорем) в некотором приближении ближе к языку, по крайней мере, понятно как такой язык можно было бы сконструировать.

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

а потом выясняется, что кроме множеств по Кантору и Колмогорову есть ещё ZF, без аксиомы упорядочивания. Главное, что мы знаем или можем узнать, что если у марсиан интуитивное понимание другое, то это можно проверить наличием или отсутствием аксиомы. И одну модель выразить через другую. Формальных способов отделить может и нет — достижение понимания может быть неформальный способ, отделив который формально мы теряем весь цимес. Главное, чтобы был формальный способ объяснить понятия на другой язык, другую модель, не завися от способа реализации модели, минимизировав систему аксиом.

Но у марсиан ведь может быть несколько другое интуитивное понимание?

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

Тьюринг-неполнота появляется только в том случае, если мы хотим сохранить алгоритмическую разрешимость тайпчека.

а почему мы не должны этого хотеть?

> Семантикой могли бы быть аксиомы и базовые понятия + логика

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

Главное, что мы знаем или можем узнать, что если у марсиан интуитивное понимание другое, то это можно проверить наличием или отсутствием аксиомы.

Так аксиомы задают теорию, а не модель. Вот есть ZFC - это теория. И ZF - теория. Это разные теории. И у каждой, наверное, есть модели (разные). но каждая из моделей теории подчиняется одинаковому набору аксиом.

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

А вот в том и дело, что нету никакого понимания. Нету никакого определения у стандартной модели (даже не факт, что эта модель существует). То есть эта модель - это именно то, что ты себе представляешь, когда слышишь «стандартная модель». Не более и не менее. Никаких других определений и уточнений нет.

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

Без нее практически всегда можно обойтись.

как работает композиция для функций арности > 1

а таких функций не бывает. ну смотри:

Prelude> :t fmap
fmap :: (Functor f) => (a -> b) -> f a -> f b
Prelude> :t (.)
(.) :: (d -> e) -> (c -> d) -> c -> e

это - то, что у нас есть. рассматриваем тип fmap как (a -> b) -> (f a -> f b), подставляем его в тип (.) на место (c -> d): c ~ (a -> b), d ~ (f a -> f b). поскольку d у нас встречается дважды, подставляем (f a -> f b) и в первое выражение тоже, отсюда получаем e ~ (f (f1 a) -> f (f1 b)). подставляем c и e в результат, получаем (a -> b) -> (f (f1 a) -> f (f1 b)). проверяем:

Prelude> :t (fmap . fmap)
(fmap . fmap)
  :: (Functor f, Functor f1) => (a -> b) -> f (f1 a) -> f (f1 b)

с точностью до необязательной расстановки скобок всё соответствует

> а почему мы не должны этого хотеть?

А почему мы должны не хотеть тьюринг-неполноту языка?

> тьюринг-неполноту

тьюринг-полноту, чорт.

А почему мы должны не хотеть тьюринг-неполноту языка?

в том-то и дело, что мы её хотим - но ни в Epigram, ни в Agda, ни в Coq не получаем. практическая ценность резко ограничивается автоматическим доказательством теорем, да и там большую часть действий приходится выполнять вручную

> да и там большую часть действий приходится выполнять вручную

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

> А вот что эти символы обозначают (то есть когда мы сопоставляем этим символам какие-то объекты и операции над этими объектами) - это модель, то есть семантика.

чем тогда будет являться модель этой модели, метамодель (какой-то объемлющей теории) — если она существует?

А вот в том и дело, что нету никакого понимания.

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

Не было понимания — пообщались — появилось. Странно как-то выходит, слова жо^W нету — а понимание есть.

> вот что эти символы обозначают (то есть когда мы сопоставляем этим символам какие-то объекты и операции над этими объектами) - это модель, то есть семантика.

то есть: у модели есть логика. Или нет? На чём она базируется, если есть (на какой теории или модели теории)? Если нет, то как это доказать?
Моделей можно придумать много разных, но есть полезные и бесполезные. Как их отделить? Что описывает такое разделение?
И как наконец, работает это понимание?

> чем тогда будет являться модель этой модели, метамодель (какой-то объемлющей теории) — если она существует?

Модель бывает у теории. У модели модели не бывает.

тогда что появляется в голове от объяснения этой модели?

Ничего не появляется. Нету никакого объяснения у этой модели, нету. Есть некоторое понимание (изначальное и неполное) и вот именно его мы и объявляем стандартной моделью.

> то есть: у модели есть логика. Или нет?

Логика - часть теории. Например ZF - это логика первого порядка + собственно аксиомы ZF + аксиома выбора.

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

Они с точки зрения пользы все одинаковые.

> а представьте, что к вам попал марсианин.

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

«Здесь приблизим синус фи как фи, там натянем такую натяжку... тут

члены отбросим, там модель упростим» позвольте, а по какому праву?

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

> Ибо хорошая модель та, которая описывает результаты эксперимента и это единственный критерий.

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

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

> математика (и любое другое направление искусства).

Математика не имеет никакого отношения к искусству, ибо в математике нет творчества, которое подразумевает уникальность результата, что не верно для математики, где результат по определению логически выводим из исходных данных. Собственно, эта самая «не уникальность» результата многократно и наблюдалась на практике.

>Я думаю, что Template Haskell лучше, во всяком случае, для создания eDSL.

Ты хоть один eDSL в своей жизни написал?
TH с макросами CL и рядом не стоял. Максимум - рядом со схемовскими.

> Максимум - рядом со схемовскими

Да, схемовские макросы я тоже ценю больше.

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

Ну так, события одновременные для одного наблюдателя могут не быть таковыми для другого =)

> Математика не имеет никакого отношения к искусству, ибо в математике нет творчества, которое подразумевает уникальность результата, что не верно для математики

гг. Тогда творчества нет в науке вообще (и в инженерии тоже). и остается только... хотя нет, не остается просто ничего - всё можно скопировать.

>Математика не имеет никакого отношения к искусству, ибо в математике нет творчества, которое подразумевает уникальность результата, что не верно для математики, где результат по определению логически выводим из исходных данных. Собственно, эта самая «не уникальность» результата многократно и наблюдалась на практике.

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

>По этой самой причине физика (как и любая наука) более закостенела, чем математика (и любое другое направление искусства).

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

Продолжая аналогию с литературой. Математики пишут фентези, физики - исторический роман или как-то так.

> Тогда творчества нет в науке вообще (и в инженерии тоже)

Наука и инженерия во многом именно этим и отличаются.

>> Тогда творчества нет в науке вообще (и в инженерии тоже)

Наука и инженерия во многом именно этим и отличаются.

Ты сталкивался с какими-то странными наукой и инженерией.

>значит, абстракция «список» дырявая и не совсем адекватная — не описывает схему и DTD

Да нет же! Просто XML _одновременно_ и список и АТД. Вернее существует катаморфизм устанавливающий соответствие между конкретным списком и конкретным АТД. Дело не в дырявости каких-то абстракций (тут к слову сказать и абстракций-то никаких нет), просто такой вот закон природы.

>ибо в математике нет творчества

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

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

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

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

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

>ибо в математике нет творчества

Не, я точно дурак. Подскажи хоть где по этому поводу копать? Ведь же есть наверняка раздел какая-то очередная теория по этому пододу?

> Я не хочу тебя огорчать, но «творчество» это всего лишь цепь Маркова,

с биологическим интерпретатором.

О, этот раздел математики мне знаком, и да, сказанное чушь.

При изучении естественных языков, музыки, живописи не требуются

разум.

Надеюсь этот такой грубый троллинг?

Ведь же есть наверняка раздел какая-то очередная теория по

этому пододу?

Математическая? Я не в курсе. Прочих хоть отбавляй, но я не ценитель.

А уж открывать математические объекты, вот тут уж чистый разум.

Я не совсем уловил смысл словосочетания «чистый разум», но чем бы оно ни было оно не имеет отношения к творчеству.

есть наверняка раздел какая-то очередная теория по этому пододу?

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

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

> а почему не (b -> c) -> (a -> b) -> (a -> c) ?

скорее всего это у них карринг головного мозга, видимо они отождествляют x -> y -> z и x -> (y -> z)

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

> В ООП, к сожалению, понятия «тип» «интерфейс» и «поведение» настолько переплетены, что при поминании одного из них, два других обычно подразумевают. Я пока еще не встречал ни одного ООП языка,

А как это могло вы выглядеть «правильно»? Приведи пример.

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

Только если разработчик делает формочки к БД. Но, уверяю тебя, бывают более алгоритмически содержательные задачи.

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

Это не обязательно делать сразу. Для начала полезно поисследовать упрощенную модель. И в математике тоже.

> Она делаеться в _любом_ языке. Весь вопрос в удобстве использования, и вообще применимости в рамках конкретного языка. Например, в С она не только бесполезна, но еще и вредна.

ммм... как ты сделаешь композицию функций в си без модификации исполняемого кода?

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

У плюсов типизация достаточно условно называется статической.

> Только если разработчик делает формочки к БД.

Я х.з., никогда таким не занимался, не знаю специфики.

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

Ради бога, что ты думаешь, я задач разных не видел, не решал?

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

> У плюсов типизация достаточно условно называется статической.

Как писать. Если не использовать приведения типов и RTTI, то очень даже статическая.

Т.е. DSL(и eDSL - особенно) ты не писал, и даже не пробовал разбираться в существующих.

Я так и думал.

Тогда вопрос - каким образом ты расставляешь оценки системам, назначение которых эти самые DSL создавать?

P.S. Лучше не отвечай на него. «Иногда лучше молчать и выглядеть идиотом, чем открыть рот и развеять все сомнения»

> Т.е. DSL(и eDSL - особенно) ты не писал

Догадка, очевидно, неверная.

и даже не пробовал разбираться в существующих.

Ваша глупость имеет пределы?

P.S. Лучше не отвечай на него.

Увы, идиотом и ещё каким выглядите здесь вы.

> Как писать. Если не использовать приведения типов и RTTI, то очень даже статическая.

То, что к указателю можно обратиться, не проверив его на нулл, и отсутствие типа «не-нулл-указатель-на...» это основное нарушение статической типизации с/с++. Ссылки не всегда можно поставить вместо указателей.

RTTI в общем-то непричем.

> Как писать. Если не использовать приведения типов и RTTI, то очень даже статическая.

и еще возможность использовать неинициализированные значения

> Как писать. Если не использовать приведения типов и RTTI, то очень даже статическая.

еще по мелочам: Parent* a = new Child(); ++a;

Хм, и как это влияет на обсуждаемый вопрос (вызов несуществующего метода)? Или хотите сказать, что это есть основной источник ошибок при программировании на С++?

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

Хорошо, расскажи, сколько и каких тестов надо написать, чтобы 100% быть уверенным, что нигде не вызывается неопределенная функция.

> Parent* a = new Child(); ++a;

Что-то не припомню, что бы я когда-либо писал что-либо подобное. Я вообще подобного кода никогда не видел, а вы?

> Хм, и как это влияет на обсуждаемый вопрос (вызов несуществующего метода)?

не делай вывод о статической типизации по плюсам — там она не лучшая

и да, с помощью этого можно вызвать несуществующий метод

Или хотите сказать, что это есть основной источник ошибок при программировании на С++?

основной — не знаю, но весьма значительный — по моему опыту чаще всего проги сегфолтятся

> Хорошо, расскажи, сколько и каких тестов надо написать

Вы о чём вообще? Речь шла совсем о другом.

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

предлагаю общаться на «ты»

Речь шла совсем о другом.

ну так можно отвлечься немного и все же выяснить, колько и каких тестов надо написать, чтобы 100% быть уверенным, что нигде не вызывается неопределенная функция

например, в g++ например есть gcov, который может гарантировать, что при тестовом прогоне прошли все строки (хотя половинки строк он не проверяет) — я ожидаю, что есть и допустим юзается для лиспа какой-то аналог