LINUX.ORG.RU

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

 


3

1

Вот все праздники разбирался с Template Haskell, квазицитированием, SYB и ghc7, не забывая такие важные вещи как распитие спиртных напитков и игру в FreeCiv :)

И вот какая идея мне пришла в голову... Катаморфизм ведь — штука всеобъемлющая, и если лисперы могут называть свои S-выражения алгебраическими типами данных, то почему же мы не можем называть алгебраические типы данных S-выражениями?

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

Единственное, «но» в подходе лисп-систем к компиляции, там компилятор «внутри», а не «с боку» как в более традиционных подходах. А так, работы ведутся, та же Java, та же Scala позволяет вмешиваться в работу компилятора. А в GHC есть Template Haskell, который идеологически близок к лисповским макросам, с той только разницей, что они стоят по разные стороны относительно катаморфизма: лисп как списки, хаскель как алгебраические типы с соответствующей типизацией.

В ООП языках все еще интереснее, там для реализации лисповского подхода нужно две вещи: а) классы должны быть объектами первого класса; б) должен быть способ узнавать конкретный тип объекта в рантайме. В Яве есть и первое (на худой конец в рамках JVM), и второе. В С++ есть RTTI, а вот с первым дела обстоят вроде бы не очень, хотя Александреску в своей книге показывал, вроде бы, как можно генерить иерархию классов с помощью шаблонов. Про Scala, вообще молчу, там алгебраические типы «из коробки» имеются.

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

★★★★★
Ответ на: комментарий от Macil

> Это общий закон: как только ты перестаешь развиваться, искать

что-то новое — все.


Ладно, и при чём здесь математика? Haskell и т.п.?

archimag ★★★
()
Ответ на: комментарий от Macil

> Дык, видели... Но увы... Пробелы, чудовищные пробелы в образовании.

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

anonymous
()
Ответ на: комментарий от Macil

Дык, видели... Но увы... Пробелы, чудовищные пробелы в образовании.

языки с зависимыми типами Тьюринг-неполны, а rank-n полиморфизм (начиная с n = 2) делает невозможным вывод типов. иногда стоит жертвовать формальной чистотой ради практичости

к слову о Haskell, находка дня: Manatee. сваяно одним китайцем за четыре месяца, с использованием attoparsec, attojson, dbus, template haskell и GHC 6.12

jtootf ★★★★★
()
Ответ на: комментарий от archimag

>Ладно, и при чём здесь математика? Haskell и т.п.?

Да не причем.

Я вот хочу спросить, так могут ли в лиспе S-выражения являться алгебраическими типами данных, как ты с позиции _практики_ на это дело смотришь? Опять же, катаморфизм который устанавливает соответствие между списками и АТД никто не отменял, но только в теории.

И что ты думаешь по поводу Template Haskell. Сможет он заменить лисповскую макросистему?

Macil ★★★★★
() автор топика
Ответ на: комментарий от anonymous

Это тупо композиция двух функций. Ничего интересного.

Мне непонятно, как выделенное (.) :: (b -> c) -> (a -> b) -> a -> c делается из исходных двух функций.

one_more_hokum ★★★
()
Ответ на: комментарий от jtootf

>а rank-n полиморфизм (начиная с n = 2) делает невозможным вывод типов

В общем случае, в общем. Если мы будем в нужных местах подсовывать аннотации типов, то вывод вполне возможен.

языки с зависимыми типами Тьюринг-неполны


А Brainf*k Тьюринг-полный, и?

ЗЫ: Для меня находка месяца - Yesod.

Macil ★★★★★
() автор топика
Ответ на: комментарий от anonymous

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

Может потому, что решают? Пусть пока не все-все-все, но математика на месте не стоит.

one_more_hokum ★★★
()
Ответ на: комментарий от one_more_hokum

Мне непонятно, как выделенное (.) :: (b -> c) -> (a -> b) -> a -> c делается из исходных двух функций.

а что не так? если есть функция a -> b, и есть функция b -> c, в чём сложность сделать функцию a -> c?

jtootf ★★★★★
()
Ответ на: комментарий от one_more_hokum

Мне непонятно, как выделенное (.) :: (b -> c) -> (a -> b) -> a -> c делается из исходных двух функций.

-- Make sure it has TWO args only on the left, so that it inlines
-- when applied to two functions, even if there is no final argument
(.)    :: (b -> c) -> (a -> b) -> a -> c
(.) f g = \x -> f (g x)
anonymous
()
Ответ на: комментарий от one_more_hokum

>Мне непонятно, как выделенное

Функциональная композиция принимает на вход две функции. Возвращает функцию, которая сначала подает свой вход на вход первой функции (a -> b), выход первой функции подает на вход второй (b -> c), выход второй функции подает на свой выход: вот и получается a -> c.

ЗЫ: Но намного интереснее композиция двух функций map. Вот это истинный Дзен.

Macil ★★★★★
() автор топика
Ответ на: комментарий от Macil

и?

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

jtootf ★★★★★
()
Ответ на: комментарий от Macil

> могут ли в лиспе S-выражения являться алгебраическими типами данных

Я х.з. как можно понятие алгебраических типов данных проецировать на лисп.

И что ты думаешь по поводу Template Haskell. Сможет он заменить

лисповскую макросистему?



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

archimag ★★★
()
Ответ на: комментарий от jtootf

>так это побольше красивых вещей вроде

Но почему-то эти вещи появляются на стыке практики и исследований... Или вон взять Скалу... Вроде бы все там есть, но какой там комбинаторный парсер. Разве он сравниться с Parsec? Нет, его изучать очень интересно и познавательно, особенно имея под боком статью Фоккера... И даже монады там имеются, но пока только в качестве сторонней библиотеки... И без той элегантности, присущей хаскелю.

Или взять тот же совершенно примитивный, но крайне полезный tagsoup.

Почему-то именно там где проводися исследовательская работа получаются красивые вещи... А там где решаются инженерные задачи получаются монстры типа EJB и Spring.

Macil ★★★★★
() автор топика
Ответ на: комментарий от jtootf

>никакого дзена. обобщается с помощью first и second из Control.Arrow

О! А объясни почему такая композиция ВООБЩЕ РАБОТАЕТ!

Macil ★★★★★
() автор топика
Ответ на: комментарий от archimag

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

А почему? Ведь по сути дела нас окружают алгебраические типы.

Macil ★★★★★
() автор топика
Ответ на: комментарий от Macil

> Почему-то именно там где проводися исследовательская работа

получаются красивые вещи... А там где решаются инженерные задачи

получаются монстры типа EJB и Spring.



Это просто особенности вашего восприятия. Всё не так.

archimag ★★★
()
Ответ на: комментарий от one_more_hokum

> (.) :: (b -> c) -> (a -> b) -> a -> c

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

one_more_hokum ★★★
()
Ответ на: комментарий от Macil

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

С тех же успехом можно заявить, что нас окружают ООП объекты.

anonymous
()
Ответ на: комментарий от Macil

> Почему-то именно там где проводися исследовательская работа получаются красивые вещи... А там где решаются инженерные задачи получаются монстры типа EJB и Spring.

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

anonymous
()
Ответ на: комментарий от Macil

почему такая композиция ВООБЩЕ РАБОТАЕТ

а почему не должна?

Prelude> fmap show ([1, 2, 3] :: [Int])
["1","2","3"]
Prelude> (fmap . fmap) show ([[1], [2], [3]] :: [[Int]])
[["1"],["2"],["3"]]

вопрос лишь в том, как глубоко мы хотим залезьть в функтор

jtootf ★★★★★
()
Ответ на: комментарий от archimag

>> Ведь по сути дела нас окружают алгебраические типы.

Лично меня - нет.


Хорошо, рассмотрим самый простой и избитый пример: XML. Рано или поздно его приходтся читать или писать. Например, в XML'е по просторам нашей родины путешествуют межбанковские платежи (см. УФЭБС).

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

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

Для приложения же, XML — алгебраический тип. В конце-концов наша задача преобразовать XML в структуры, специфичные для нашего приложения, или наоборот сделать их них XML.

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

И нам уже без разницы _откуда_ взялся этот алгебраический тип! Как только мы его получили, мы забыли про XML. Например, мы можем писать абстрактные операции, связанные с обходом нашего типа, причем таким образом что они не будут зависеть от его структуры, и не нарушая типизации представлением XML в виде списка или стирания типов до Node. См. например, Scrap Your Boilerplate.

Мы можем делать морфизмы АТД -> АТД' для целей адаптации к нашей предметной области, максимально независимым от чего-либо способом. Мы без опаски можем раздавать куски нашего алгебраического типа функциям для анализа и система проверки типов нам гарантирует, что никакого «непонимания» не случится: мы чисто физически не сможем передать его в «неправильную» функцию. Мы получаем возможность использовать функциональную композицию в качестве аналога «/» XPath.

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

Слабо через TH замутить определение АТД путем анализа Schema? И так далее.

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

Macil ★★★★★
() автор топика
Ответ на: комментарий от anonymous

>а linux монструозен, но делает своет дело

А на всех банкоматах крутится винда (или OS/2). А мы почему-то идем против тенденции и входим в число 1%, пользующих линукс на десктопах.

Macil ★★★★★
() автор топика
Ответ на: комментарий от Macil

> А на всех банкоматах крутится винда

4.2, я знаю как минимум один банк( ПриватБанк ) где используется линукс, хоть и не везде

aho
()
Ответ на: комментарий от aho

>4.2, я знаю как минимум один банк( ПриватБанк ) где используется линукс, хоть и не везде

Не везде. На банкоматах стоит винда. ЦБшный спецсофт: ПТК ПСД, АРМ КБР, Клико, Верба, Сигнатура, всякие разные проги для подготовки отчетности (валютные отчеты вообще DOS'овские), например 652-я форма отправляется ежедневно из ДОС'овской проги. Вот так и живут.

Мало кто будет дублировать ПТК ПСД в регионах или Клико в Москве, хотя форматы открыты, и никто не мешает. Но, все-равно останется криптософт.

А опердень - дело банка. Вон вроде кто-то его даже на ерланге пишет. Или например есть БИФИТ'овский интернет-банк, и серверная и клиентская часть (при использовании совместимых смарт-карт) может работать под линуксом. Там даже документация в LaTeX'е сделана.

Macil ★★★★★
() автор топика
Ответ на: комментарий от Macil

Переписали бы Spring на Scala (вариант - Spring.NET на Nemerle) - монструозность если бы и не исчезла, но существенно уменьшилась бы.
Но ах и увы - жаберы смотрят на скалу, как на существо из параллельной вселенной.

yaws
()
Ответ на: комментарий от Macil

> Хорошо, рассмотрим самый простой и избитый пример: XML.

Что-то я какого-либо профита от представления XML в виде АТД не ощутил.

Мы получаем возможность использовать функциональную композицию

в качестве аналога «/» XPath.



Спасибо, я лучше через XPath.

любой сложный конфигурационный файл является АТД


Только для того, кто хочет его таким увидеть. Я не хочу.

archimag ★★★
()
Ответ на: комментарий от anonymous

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

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

anonymous
()
Ответ на: комментарий от jtootf

> языки с зависимыми типами Тьюринг-неполны

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

anonymous
()
Ответ на: комментарий от anonymous

> Тьюринг-полнота появляется

Тьюринг-неполнота, конечно.

anonymous
()
Ответ на: комментарий от jtootf

>вопрос лишь в том, как глубоко мы хотим залезьть в функтор

Я это понимаю. И композиция, допустим, return понятна. А вот как работает композиция для функций арности > 1?

Macil ★★★★★
() автор топика
Ответ на: комментарий от archimag

> По моим представления конец разработки он через год или два после того, как программа уже активно эксплуатируется.

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

anonymous
()
Ответ на: комментарий от archimag

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

не очевидно ни разу. Это процесс разработки в котором отсутствует нормальная рабочая спецификация, а разработка ведётся мимо спецификации (составление спецификации — сайдэффект процесса разработки). Это неорганизованный процесс.

Вот посмотри на разработки по спецификациям: House OS на Хаскеле, seL4 , TRON, EROS и BitC , драйвера DevIL (описание)

Тут сначала описана спецификация (в случае seL4 — спецификация не на сам L4, который уже был, а спецификация проверки на безопасность), затем спецификация формально верифицируема, затем пишется ОС (или драйвер) по формально проверенной спецификации. То есть, спецификации становятся исполняемыми — потому что формально верифицируемы и доказаны на корректность.

Для приложений сурового ынтерпрайза гугли в сторону метамоделей, по «Metamodel framework» . Например, у Eclipse есть EMF /TMF /ECF/EPF метамодели. Из всего этого выводка наиболее интересен с точки зрения функциональности Xtext как средство создания DSL, почти что language workbench на базе Eclipse.

Я как бы прозрачно намекаю, что DSL — это тоже исполняемая спецификация.

Вообще почитай хотя бы того же Джоэля, что он пишет о правильной, полезной спецификации. А то, то что ты называешь спекой — это записки на манжетах, а не спецификация.

anonymous
()
Ответ на: комментарий от archimag

Ну и как, что-нибудь уже доказали?

доказали, сюрприз. Доказали фактическое соответствие программы исполняемой, верифицируемой спецификации. Потому что исполняемая спецификация — это и есть программа. А процесс компиляции — доказательство.

Система типов и её ограничения — доказательство корректности одной части спецификации. Контрактное программирование и инварианты — доказательство другой её части. Тесты и тестовое покрытие — доказательство третьей части спецификации. Статический анализ, lattice ичсо — четвёртая часть спецификации. Агда и т.п. автоматическое доказательство теорем — пятая. Старый добрый Дейкстра с верифицируемыми программами и пред- и пост- условиями на операционную семантику инструкций программы — шестая.

Ну, ты понял.

anonymous
()
Ответ на: комментарий от anonymous

>> Кстати, а вообще можно работать полностью без преобразования типов?

А какие с этим проблемы? Зачем вообще может понадобиться преобразование типов?


я вот намедни повозился с Обероном-2 в BlackBox Component Pascal. Почти что лисп, в некотором роде :) С точки зрения интерактивности разработки. Но какой-то недоделанный, без макросов и monkey patching-а отдельных функций. Исключений даже нет в языке, зато есть ASSЁRT-ы.

С одной стороны, здоровый минимализм: язык в EBNF умещается на 1 страницу, конпелятор модулем <16к, далее модулями реализованы загрузчик/выгрузчик модулей и bootstrap к Kernel (через KERNEL32 WinAPI, о-ё), и линкер standalone exe и DLL, сборщик мусора модулем на паскале.

Текст как интерфейс, привет Plan9. Можно сконпелировать, подёргать за функции модуля, перегрузить новую версию модуля. Правда, аналога asdf нет, так что для чего-то вроде hot swapping нужно извращаться: составить топологической сортировкой список клиентов модуля, выгрузить клиентов, перегрузить сервер, опять загрузить клиентов. Правда, есть ГУИ, несколько упрощает. Такие же выкрутасы с standalone exe: готовим список модулей в нужном порядке, генерируем exe.

В лиспах можно было бы отдельную функцию на лету monkey patch-ить, без возни с модулями.

Единица конпеляции модуль, модули с метаинформацией о типах, которая активно используется в GC и утилитах. Например, как там строят ГУИ формочки: пишешь в модуле переменные-записи, экспортированные с экспортированными полями (интеракторы), пишешь экспортированные из модуля процедуры. Затем выбираешь в меню Form/New Form... вводишь <имя модуля> — модуль FormGen, который есть в исходниках, разбирает метаинформацию модуля <имя модуля> и сам лепит форму с полями по образцу интеракторов + экспортированные процедуры становятся кнопками. Никаких OnButton1Click-ов! Наоборот, из исходника — форма, текст как модель.

Так вот, там прикручен COM и венда; а сами системоспецифичные штуки убраны в «псевдомодуль» SYSTEM. В SYSTEM есть преобразование типов, unsafe [untagged] указатели вне сборщика мусора, битхак регистров и памяти напрямую. COM «псевдомодуль» реализован примерно как SYSTEM.

За исключением этих модулей, весь остальной код — переносим, безопасен и написан сам на себе. Зато сразу понятно в модуле — включили SYSTEM, получили преобразование типов и unsafe код, не включили — получили безопасный код со сборщиком мусора, контрактами (ассёртами) и т.п.

COM там тоже интересно сделан. Вообще-то тот же QueryInterface(GUID iid,(void**)&pInterface)) — это тот самый пример, когда нужно преобразование типов (через void**).

Они там сделали типобезопасный COM! То есть, если пишем QueryInterface(COM.ID(iid1),pId1);...;QueryInterface(COM.ID(iid2),pId2); ...; pId2:=pId1, то конпелятор **проверяет** являются ли интерфейсы pId2 и pId1 совместимы (один потомок другого) и если нет, ругается в момент конпеляции!!

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

Вот примерно за этим нужно преобразование типов.

anonymous
()
Ответ на: комментарий от archimag

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

странно, а мне Real World Haskell показался довольно практичным. Почти как PCL, хотя в PCL примеров побольше. Потом, есть же Rossetta Code

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

Факториал нужен не для изучения языка, а для изучения его компилятора и кодогенератора. Факториал, фибонначи, функция аккермана, tak/takl и т.п. — это stress test для вызова функций, рекурсии, выделения на стеке переменных и пары несложных операций. То есть, время выполнения такой функции показывает, насколько хороший код генерирует конпелятор.

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

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

Отличный язык Haskell, в котором нельзя сделать ошибок просто по той причине, что на нём почти нельзя писать ничего практического. Нет код - нет ошибок. Мечта

да, то, что код написаный кое-как в хаскелле просто не скомпилируется из-за слишком умного конпелятора — новичка озадачивает поначалу (а я как-то обновил ghc, у меня и старый cabal/haddock новым конпелятором перестал собираться, а на новый ещё ебилд не написали. Похожая история с редактором yi: вроде бы и есть редактор, а уже не собирается. Вот засада). Тут с нахрапу не взять — нужно читать, думать, думать что писать. Тогда как в более динамичных языках можно сразу накидать какой-то код и он даже как-то заработает.

anonymous
()
Ответ на: комментарий от anonymous

>> Факториал нужен не для изучения языка, а для изучения его компилятора и кодогенератора. Факториал, фибонначи, функция аккермана, tak/takl и т.п. — это stress test для вызова функций

archimag не про это написал, а про то, что подавляющее число книг и туториалов по Хаскелю вместо hello world используют факториал.

cathode
()
Ответ на: комментарий от anonymous

а какие абстракции над АСТ нужны? не то чтобы минимально достаточные, а реально удобные?

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

намекаешь на DSL? но можно построить например Skeleton Syntax Tree , двигаясь от АСТ к макросам, а можно наоборот, двигаться от макросов к АСТ (схемовские макросы или через списки вместо AST в общелисп).

Какие макросы удобнее? АСТ для АСТ макросов должен строить конпелятор, его не нужно строить руками.

anonymous
()
Ответ на: комментарий от anonymous

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

и так далее, вплоть до драйверов и ОС

Этого сделать на данный момент нельзя,


вообще-то, можно

да и никому не надо.


но не нужно.

у т.е. всякие факториалы еще можно гарантировать, а что-то сложнее трудно.


сразу на ум приходит многопоточное программирование и отсутствие race conditions. И ещё что-то по характеристикам GC и/или JIT — только они владеют динамической полной информацией.

anonymous
()
Ответ на: комментарий от anonymous

> Какие макросы удобнее? АСТ для АСТ макросов должен строить конпелятор, его не нужно строить руками.

Об этом я и говорю. Кстати, доделал loop (дропнул только named-форму для for, потому что не понял семантику, и terminated формы с терминальными accumulate-clause - лениво набивать все это дело, хотя на каждую и надо по две строки) в итоге получилось 150 строк. Сколько там у нас исходники оригинального лупа? 1500?

anonymous
()
Ответ на: комментарий от Macil

Ответ очевиден: закостенеешь мозгом, будешь не спобен принимать, и воспринимать новое.

+1 образ мышления надо улучшать, тогда и профиты посыпятся тыц

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

anonymous
()
Ответ на: комментарий от anonymous

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

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

Развлекательный сайт, короче говоря.

tailgunner ★★★★★
()
Ответ на: комментарий от archimag

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

имею противоположный опыт. Наш математик, объясняя теорию чисел в 8-м классе, доказывая что 2*2=4 (и по геометрии, доказывая теорему Евклида (аксиому в обычной школе) из другой произвольно взятой аксиомы) на вопрос: «Зачем?» отвечал: «а представьте, что к вам попал марсианин. Как вы смогли бы найти с ним общий язык? Каким должен быть алфавит, система понятий, общие точки соприкосновения?» и потом как-то само собой получалось, что математика на роль такого языка подходит. Подошли бы, возможно, и физические законы. Ну а вдруг мы в другой вселенной и инварианты интегралов (законы сохранения) там другие?

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

От людей зависит, на самом деле. Не так важно зачем, важно могёт или не могёт.

anonymous
()
Ответ на: комментарий от tailgunner

ну да, там дальше в Reciprocality совсем веселуха пошла... скандалы, интгриги, расследования...

anonymous
()
Ответ на: комментарий от anonymous

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

... и не все. А только те, где абстракции адекватные. Не надо впихать невпихуемое.

anonymous
()
Ответ на: комментарий от anonymous

> математика на роль такого языка подходит

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

anonymous
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.