Я хоть и не спец, но ФП оперирует pure functions, в отличие от....

Я хоть и не спец, но ФП оперирует pure functions, в отличие от....

pure functions я упомянул как `функции как объекты первого класса'.

А в отличии от чего?

> pure functions я упомянул как `функции как объекты первого класса'.

И ошибся ;) pure function это функции в математическом смысле, для вычисления которых используется подстановочная модель.

Ну это я тоже упомянул :) Лямбда исчисление `как одна из моделей ФП'. В то время как с точки зрения алгебраического подхода - лямбда исчисление это что-то вроде бакэнда для системы типов. Что касается «типов» - то тут у меня совсем недавно было глобальное непонимание - я думал тип это что-то вроде typedef в C или deftype в CL, в то время как АТД как абстрактный ТД это частный случай АТД как алгебраического ТД, а тот частный случай начальной алгебры (initial algebra) - т.е. чисто математическое определение из которого следует всё остальное. Ну а лямбда исчисление, pure functions, mutable algorithm, или state machine это уже вычислители, на которых может быть выполнена процедура eval соответствующая исходному математическому определению.

Можно сказать что тут такая система отношений:

1) АТД целиком определяет (посредством категории) катаморфизм, анаморфизма, хиломорфизма и параморфизма.

2) Последний определяет класс всевозможных функций над АТД

3) Функции эти могут быть выражены (транслированы, например можно погуглить по warm fusion методам) в представлениях того или иного вычислителя - это не обязательно лямбда исчисление, это может быть вычислитель структурного программирования (ветвление/следование/цикл/мутабельность/память).

      ATD

       |

    Cata, etc.

     /  \

   LC   State Machine

вот мне интересно место LC на этой схеме, оно как бы сбоку :) т.е. в принципе не является абсолютно необходимым.

Слишком сложно для меня. Я не понял, к чему ты это всё сказал. Я знаю про подстановочную модель вычислений (которая используется в ФП) и про модель вычислений с окружением. Критерий ФП/«не ФП» получается простой. И почему называется ФП тоже очевидно.

> я думал тип это что-то вроде typedef в C или deftype в CL, в то время

как АТД как абстрактный ТД это частный случай АТД как алгебраического

ТД, а тот частный случай начальной алгебры (initial algebra)

Мне вообще плохо понятно зачем математику за уши к программированию притягивать. typedef -> initial algebra это мощно.

Функции эти могут быть выражены (транслированы, например можно

погуглить по warm fusion методам) в представлениях того или иного

вычислителя - это не обязательно лямбда исчисление

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

P.S. Типа потроллил

Слишком сложно для меня. Я не понял, к чему ты это всё сказал.

В том числе к тому чтобы прояснить мысль первого поста (в том числе для самого себя)

Я знаю про подстановочную модель вычислений (которая используется в ФП) и про модель вычислений с окружением. Критерий ФП/«не ФП» получается простой. И почему называется ФП тоже очевидно.

В той схеме подстановочная модель (я в курсе только про лямбда исчиление и комбинаторную логику) это LC. Модель с окружением я назвал State Machine. Тут действительно можно чётко отделить первое от второго.

Так вот я утверждаю что эти две вещи (самый нижний уровень - вычислители с категорией времени (с)) сейчас становятся «бакэндами» для понятий следующего уровня (то что на схеме выше) - их часто обсуждают под тэгом fp, но это ведь не ФП (?) Это алгебраические понятия.

Ответ на "потролил" :)

Мне вообще плохо понятно зачем математику за уши к программированию притягивать.

Нет, нет не притягивают - используют математику для изучения программирования. Почему бы нет? Математику ведь используют для изучения чего угодно. Так что «практическое программирование» (с) не имеет отношения к математике - я согласен (правда, если знать математику при практическом программировании возникают посторонние мысле, но это ладно).

typedef -> initial algebra это мощно.

Такого не было, я протестую!)

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

Ну не сразу ведь. Есть промежуточная ступень - в Haskell (и в ML семействе) это LC (и lazy graph reduction), в CL это state machine (и energy graph reduction).

Я не понимаю (учитывая что современные машины это регистрово-стековые машины) зачем в Haskell эта промежуточная ступень в виде лямбда исчисления.

>pure functions я упомянул как `функции как объекты первого класса'.

Чистые функции - это функции без сайд-эффектов, неуч.

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

Математику ведь используют для изучения чего угодно.

Угу, в качестве вспомогательного инструмента когда в этом действительно есть необходимость.

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

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

Чистые функции - это функции без сайд-эффектов, неуч.

Спасибо, грамотей, это было очень важно для меня :)

А как быть с over 100500 статей посвящённых сабжу (математические модели в программирование) и с несколькими десятками ЯП (тот же Haskell) которые используют то или иное математическое основание. Просто я постоянно наблюдаю проникновение математических понятий (и судя по истории в последние годы все больше и больше) в программирование. Да, кстати, и на этом форуме ест люди которые позволяют себе использовать эти математические понятия.

С литературой понятно - я тоже люблю литературу :) Но если речь идёт о формальных дисциплинах (неужели программирование больше «литературно» чем формально?) таких как физика или вычислительная теория - по моему ничего странного в математике рядом тут нет.

> А как быть с over 100500 статей посвящённых сабжу (математические

модели в программирование)

Они кому то мешают? Пусть будут, это же наука.

Просто проведи границу между наукой и программированием.

> неужели программирование больше «литературно» чем формально?

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

Кстати, тут говорят, что на днях программист из HP (возможно) доказал P /= NP :)

Просто проведи границу между наукой и программированием.

Не могу :) Как?

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

Если программирование == кодирование...

> Если программирование == кодирование...

Ты не в теме.

>Почему

Устоявшаяся традиция. Аналогично, проф.моряки все невоенные суда называют «пароходами».

границу между наукой и программированием.

Граница - это искусство: Д.Кнут «Искусство программирования» :)

Элементарно. Программирование - это инженерия. Решение конкретной задачи конкретными средствами в конкретные сроки.

Наука - поиск нового, ранее не известного. Как правило, не известно чего именно, и совершенно точно не известно, когда.

> проф.моряки все невоенные суда называют «пароходами».

«Судами», дятел, «судами». В отличие от военных - «кораблей».

Ты не в теме.

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

Плавали, знаем! (с)

>«Судами», дятел, «судами». В отличие от военных - «кораблей».

Военный - «корабь», невоенный - «пароход». Sic!
Даже официально: «Балтийское Морское Пароходство». :)

> Однако, таким образом можно отнести к литературе

Зри в корень. Самым важным, помимо смыслового содержания, свойством хорошей литературы является ясное, чёткое, последовательное изложение мысли на протяжении многих и многих страниц текста (здесь отсылаю к произведениям Чехова и Хэмингуэя, как к вершинам подобного творчества). Тоже относится и к хорошим программам и, между прочим, лежит в основе Unix-традиции. Поскольку сохранения ясности и последовательности для больших программ является, как и для литературных произведений, чрезвычайно сложным, то в основном по этому и можно оценить уровень программиста/архитектора. А сложность разработки алгоритмов очень локальна и её преодоление является чисто технической проблемой, справиться с которой зачастую могут даже математики.

корабль — это такое судно, которое имеет на борту вооружение.

судно — это такой корабль, который не имеет на борту вооружения.

разница ясна?

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

Я должен поправиться - всё таки LC играет в Haskell важную роль ещё потому что это модель чистого программирования. Т.е :

1) Есть программирование функциональное имеющее моделью LC.

2) Есть императивное программирование основанное на таких принципах: окружение/память, мутабельность, следование, ветвление, цикл (или go). Т.е. host это state machine.

3) Есть программирование в терминах чистых данных (не мутабельных). Есть соответствующая теория параллелизации программ.

4) И есть алгебраическое программирование (восходящее к категориям). Оно известно в Haskell в том числе - считается правильным использовать операторы/комбинаторы при написании функций, а не реализовывать их через рекурсию.

Я с самого начала хотел сказать что 4 (алгебраическое программирование) и 1 (классическое ФП) - очень разные вещи. В конце концов понятие типов и отображений самые высокоуровневые и ключ к ним именно в 4 - я могу взять императивный язык (2) с метапрограмными возможностями и реализовать эти понятия, причём никакого LC тут не будет а соответствующая выразительность появится. Плюс LC в том что оно даёт возможность ещё к (3), но я догадываюсь (тут я не уверен), что можно обойтичь и без него - достаточно просто ввести иммутабельность (без всякого LC) - как пример есть Clojure.

> про базовые вещи, лежащие в основе программирования

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

Нифига. В документах только «суда» и «корабли».

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

В основе *ремесла* - да. Когда я говорю «в онове программирования» я не имею ввиду какое-либо искусство или умение писать программы. Где-то 70% серьёзных вещей в программировании возникли не без воздействия математики (за всё время его существования) вот это под базой я и и подразумеваю. Короче не программирование (процесс), а скажем его основания.

>судно — это такой корабль, который не имеет на борту вооружения. Rastafarra.

Судно, в просторечье «утка» - подают в больничках, а пароход подают к причалу.

>корабль

Спроси любого военного моряка: правильно - «корабь» (без «л») NB!

>Нифига. В документах только «суда» и «корабли». LamerOk

Ага, по документам Москва - порт 5 морей!

Бумажные «моряки» дектектед : сходите хотя бы раз в море, там вас научат правильной морской терминологии :)

Ты свои сказки бабушке рассказывай, «железный моряк». ))

>Ты свои сказки бабушке рассказывай, «железный моряк». ))

И у моряков и у программеров есть профессиональный сленг, жаргон, не совпадающий с русским литературным языком и вызывающий недоумение у непосвящённых. На корабельном ВЦ я даже слышал пожелание: «семь футов под сервером» :)

Здесь не корабль и не пароход, поэтому не нужно употреблять корабельный сленг.

на днях программист из HP (возможно) доказал P /= NP

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

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

Т.е. в целом разделение на ветви которое я обозначил (мало связанные) - это верно?

разделение на ветви которое я обозначил (мало связанные) - это верно?

которое именно? в этом треде было много разделений на ветви

и, к слову, любая CCC индуцирует simply typed LC,- так что связь, определённо, есть

То что в самом первом посту и то же самое но другими словами http://www.linux.org.ru/jump-message.jsp?msgid=5221790&cid=5222105

и, к слову, любая CCC индуцирует simply typed LC,- так что связь, определённо, есть

А что такое CCC? Я сейчас могу (с горем по-полам) автоматически строить из списков декларативно задающих АТД соответствующие катаморфизмы, причём как в в функциональном виде (то к чему можно привязать LC) так и в виде набора императивных инструкций - вот этот факт заставил меня задуматься о том, что связь типы (категории) -> LC не является чем-то уникальным (хотя может я упускаю LC как некое промежуточное представление между типом и императивным представлением катаморфзма), так или иначе ещё есть типы (категории) -> вычислитель другого (императивного) толка.

что такое CCC?

декартово замкнутая категория

в виде набора императивных инструкций

любая императивная программа строится из набора базовых инструкций (таких, как add, mul, div, test<, etc) с помощью конструкций, доступных в дистрибутивной категории

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

tnx.

Меня в общем смущает такие моменты: возьмём к примеру haskell, как язык в котором уделяется много внимания АТД:

1) Есть АТД List и есть foldr - почему этот foldr определён рекурсивно - ведь это рекурсивное определение будет транслироваться посредством lazy graph reduction в более примитивное (низкоуровневое) представление с привлечением LC (LC я считаю в данном случае промежуточным представлением между АТД (которое чисто математически определяет свой катаморфизм) и низкоуровневым языком архитектуры). Почему не написать foldr императивно - как цикл, например? В этом случае несколько упростится последующая трансляция. Возможно промежуточное представление LC используется для оптимизаций основанных на иммутабельности?

2) Собственно, почему этот foldr *пишется* - он ведь может быть построен автоматически по АТД, причём как в виде рекурсивного определения, так в виде императивного цикла.

почему этот foldr *пишется* - он ведь может быть построен автоматически

http://www.mail-archive.com/haskell-cafe@haskell.org/msg51106.html

смотри ответы

рекурсивное определение будет транслироваться посредством lazy graph reduction в более примитивное (низкоуровневое) представление с привлечением LC

стандарт этого не требует; посмотри на кодогенерацию JHC, например

>Самым важным, помимо смыслового содержания, свойством хорошей литературы является ясное, чёткое, последовательное изложение мысли

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

название ФП совершенно неудачное, я бы предложил «иммутабельное программирование», оно не настолько плохо

но в оправдание ФП можно отметить, что 4 плохо стыкуется с 2, во всяком случае так говорят

начав раздумывать над конкретным примером неприятностей при этой стыковке, выяснилось, что найти его трудно... можно вспомнить «квадрат это не прямоугольник», но это не на тему АлгТД... вот высосал из пальца :

data MyData = This Char Char Char | That Int

то при попытке сделать MyData мутабельным, выделив для его хранения 4 байта (максимум из 2 вариантов) *и* мутируя его после этого in-place, огребаем проблемы например в паттерн-матчинге (надеюсь, ясно какие); при мутировании а-ля ява (class MyData... class This extends MyData ... class That extends MyData ...) со сборкой мусора проблем придумать пока не удалось

видимо, стоит поднять этот вопрос

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

у меня давно впечатление, что 4 с 2 стыкуется вполне прилично, а всякие «квадрат это не прямоугольник» это следствие слишком «большого шага» в объектной системе; маленький шаг — это что-то типа тайпклассов или концептов в с++

у меня давно впечатление, что 4 с 2 стыкуется вполне прилично

Вот это и есть основная мысль этого треда. Можно взять какой-нибудь императивный язык в котором нет и в помине ни иммутабельности, ни лямбда исчисления, но есть приличное метапрограммирование - тогда можно внести в такой язык очень хорошие АТД. При этом мне сейчас кажется что АТД (и сопутствующие категорные понятие) это вершина, т.е. цель, в то время как остальные пункты - просто средства. Скажем в этом императивном языке с метапрограммированием определение типа Список автоматически может определять и катаморфизм, следовательно (почти) автоматически все функции над списками, причём выражены они будут не функционально а императивно (функциональное выражение это выражение в терминах LC, а императивное - в терминах state machine).

data MyData = This Char Char Char | That Int

то при попытке сделать MyData мутабельным, выделив для его хранения 4 байта (максимум из 2 вариантов) *и* мутируя его после этого in-place, огребаем проблемы например в паттерн-матчинге (надеюсь, ясно какие); при мутировании а-ля ява (class MyData... class This extends MyData ... class That extends MyData ...) со сборкой мусора проблем придумать пока не удалось

Мне кажется, что для типа с набором конструкторов:

data Data = {Cons ... | i = 1 .. k }

Нужно вводить соответствующие k функций мутирования. Например в CL существует defstruct который определяет АТД типа структура, при этом для n полей определяет n функций setf (которые мутируют поля). Ну а в CLOS есть ещё и некоторый контроль над тем - какие мутирующие функции вводить (и вводить ли). Например:

(defstruct square
  x
  y
  a)

;; вводит мутирующие функции square-x, square-y и square-a

Никаких проблем тут, конечно, нет - ни при паттерн-матчинге, ни при сборке мусора.

Вообще, вопрос введения (4) в (2) в лице CL (а то я уже слегка попробовал) это вопрос техники - точнее техники применения warm fusion в императивно-агоритмической сфере (а не в функциональной).

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

Кстати, а грамматика Хомского случаем не является категорией?

Кстати, а грамматика Хомского случаем не является категорией?

аккуратней с терминами, пожалуйста. что значит является категорией?

В смысле:

G ≡ (T, N, S, R)

T -- терминалы,
N -- нетерминалы,
S ∈ N -- начальный символ,
R -- продукции.

Obj(G) = [T ∪ N]* -- объекты это все цепочки (кортежи) над T и N
Arr(G) = R -- собственно стрелки α → β ; α, β ∈ [T ∪ N]*

Очень похоже, а композиция это конкатенация цепочек (?) α β ≠ β α . Но ведь это ещё не всё? Нужно как-то доказывать?

Блин, композиция над стрелками должна же быть, а конкатенация это просто операция в моноиде [T ∪ N]*. Но может есть какая-нибудь другая композиция?