Мало. Ещё разбирающиеся в практической программистской стороне проблемы. А то породится философско-логическое подобие машины Тьюринга, выйдет статья, а программировать будет не на чем.

(а есть еще оптимизация запросов к БД)

Вроде уже говорили, что у разных инженеров разные языки, и засунуть их в один универсальный жутко тяжело

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

Кстати про БД, @ailevenchuk а на Clojure + EDN + Datomic Вы смотрели? Как оно оценивается с обсуждаемых позиций?

Это я к тому, что сведение проблемы перевода между языками (или иного взаимодействия) сводить к универальному языку мне кажется неправильным углом зрения, т. к. это сведение неподъёмного к ещё более неподъёмному. Раз нет универсального языка и, соответственно, типов в нём, то типы здесь и вовсе ни при чём. Точнее, если и при чём, то это другие типы

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

Так что я бы ответил: нет, нельзя так сделать, чтобы оно всё было одно и то же

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

Онтологи же как-то эти факты моделируют? Они же выделяют отношения "часть-целое" и "то же самое, что и"? Недостаточно будет формализовать эти отношения в достаточно богатом языке (программирования)?

Я так понимаю, что FOL их уже формализовала, но нужно что-то другое.

там те же проблемы, что с image в Smalltalk. Фишка в том, что в базы данных читают-пишут много программ, и это с самого начала учитывается — выгода в том числе и в том, что сложные программные структуры данных приходится парсировать до реляционной элементарщины. А все эти имиджи рабочих областей (persistance) одной программы плохо выразима через API для других программ. То есть ничего не добавляет.

И тогда появляются документарные базы данных, которые частично снимают эту проблему. Документы понимаются какой-то библиотекой, которую используют для чтения-записи разные программы, а вот поскольку таких программ и документов много, то организуется отдельная документарная (NoSQL) БД.

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

+

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

Да у нас регулярно теоркатегорщики появляются, только почему-то приемлемых решений нет ))) Вот, например, очередной подход к проблеме, 2014 год — https://vimeo.com/111671795

-- математическое выражение эмерджентности
-- теория категорий для выражения трассировок и correspondence rules
-- теория категорий как язык для technical space плюс
-- теория категорий как возможный формализм для SysMoLan

Эпиграф: http://asylums.insanejournal.com/atlas_farted/1741.html

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

О! Так а что этот подход, не подошел?

(Ковалёв) Ой, это же мой научрук :)

Судя по ответу - пристально не смотрели... 😃