Previous Entry Share Next Entry
2016-01

про ООП, модули и типизацию

Наконец-то я могу сказать словами то, что меня мучило все эти годы, бгггг :)

Собственно, правильно ли я понимаю, что поскольку для structurally-typed OO языков inheritance is not subtyping (Cook et al, 1990), то semantics-preserving gradual typing в structurally-typed ОО языках невозможен?

Точнее, добавление и убавление деклараций типов будет влиять на семантику программы, при наличии там проверок типов (pattern matching, method overloading, RTTI).

Ииии, в принципе, мне кажется что это справедливо не только для ОО-языков, а и любых языков с поддержкой functions as first-class values (какие-то функции высшего порядка при этом всё равно можно закодировать, но не произвольные), т.к. тайпчекинг становится data-dependent и вынужден ошибаться либо в одну, либо в другую сторону.

Собственно именно из-за этого я не люблю ООП в Java-смысле, а предпочитаю ООП в Smalltalk-смысле, только раньше формализовать не мог.

То есть, с номинальной системой типов мы не можем выразить (статически типизировать) open-world систему, т.к. номинальная система типов кодирует перечислимое множество типов данных, равномощное ω-порядку без higher-kinded types, и ωω (или ε0?) с ними, чего, очевидно, недостаточно.

Closed-world система при этом очевидным образом ограничивает модульность (типы создают частичный порядок на модулях, который, вообще говоря, не обязателен)

Возможно, это противоречие как-то решается, если делать не gradual typing, а gradual contracts (B. Pierce этого вскользь касается, 2008), т.к. контракты более, гммм, симметричны; но я пока не нашел каких-то адекватных пейперов по теме.

Success typing для Эрланга проблему, конечно, решает, но местами это упрощение до потери смысла :) т.к. оно unsound, хотя позволяет статически детектировать *некоторые* ошибки.

В SaferTypeScript (2014) соорудили франкенштейна, который с одной стороны type-safe, но с другой стороны таки не является semantics-preserving - т.к. сдвигания границы между tagged и untagged world меняют семантику программы. Хотя, может, это и выход. Но сцуко некрасиво.

Скальные path-dependent types выглядят способом обойти проблему с другой стороны; но я их что-то как-то не до конца понимаю и не уверен, поможет ли это вообще (в их случае проблема представляется как "построение type inference для ОО-языка с path-dependent типами какая-то сцуко сложная")

This entry was originally posted at http://wizzard.dreamwidth.org/408429.html. It has comment count unavailable comments. Please comment there using OpenID.

  • 1
nponeccop December 9th, 2014
Я почти ничего не понял, но скажу, что все проблемы - от оверлоадинга имён. Как только вместе с выводом типа надо заниматься name resolution - считай пропало. А в нетривиальном разрешении имён членов - вся суть ОО.

akuklev December 9th, 2014
> Собственно, правильно ли я понимаю, что поскольку для structurally-typed OO языков inheritance is not subtyping (Cook et al, 1990), то semantics-preserving gradual typing в structurally-typed ОО языках невозможен?

Не совсем правильно. Если быть точным, то SPGT возможен для подмножества языка, не использующего Ad hoc полиморфизма aka RTTI.

> Точнее, добавление и убавление деклараций типов будет влиять на семантику программы, при наличии там проверок типов (pattern matching, method overloading, RTTI).

Ну так. Это и есть разница между параметрическим и ad hoc полиморфизмом. Первый тип полиморфизма, это когда семантика инвариантна относительно RTTI, второй когда неинвариантна. В первом случае полиморфная по типу дого или иного аргумента функция требует от типа аргумента поддерживать определённый интерфейс и соблюдать его контракты, в остальном же быть любой. Во втором случае функция просто принимает вместе с аргументом имплицитно Type Descrition его типа (т.е. RTTI) и может от него зависить. В частности это означает, что такая функция ограничивает себя типами данных (не может работать с коданными, реализующими концепцию open world).

Отказ от ад-хок полиморфизма в ОО-языках влечёт за собой отказ от типоориентированного паттернматчинга аргументов имеющих полиморфный тип (включая случай сабтайпинг-полиморфизма), паттерн матчинг разрешается только если тип закрытый. Оверлоадинг же сам по себе проблем не создаёт, если всё остальное параметрически-инвариантно. С другой стороны, чтобы писать параметрически-инвариантные нетривиальные хрени в sound системе типов, нам нужны контракты (либо как first class штуки, либо в составе зависимой системы типов), и нужно думать как сделать их gradual.

Скальные PDTs (на самом деле просто грамотный подход к номинальному счислению), насколько я понимаю, в принципе маст в любой достаточно мощной номинальной системе с абстракцией модулей, без них принципиально невозможно совместить инкапсуляцию и open world'ness.

wizzard0 December 9th, 2014
Ога, спасибо, всё сходится.

Вот хочется gradual contracts, именно.

akuklev December 9th, 2014
Ну по gradual contracts пока всё, насколько я понимаю, в малоразвитом состоянии. А gradual dependent typing в своеобразном состоянии, когда теорчасть (см. последние работы Боба Этки, например) отстаёт от практической части лет на 20. Причём под практической частью я имею в виду далеко не готовые имплементации, а хотя бы прототипы языков, в которых что-то такое реализуется.

wizzard0 December 9th, 2014
Ну да. Практические имплементации таких штук отрастают не в языках, а в операционках - http://wizzard0.livejournal.com/479545.html?thread=5042745#t5042745

wizzard0 December 9th, 2014
Тааак, в треде с Максимом родился термин gradual process calculi :)

edit: http://www.cs.cmu.edu/~aldrich/FOOL/FOOL11/FCM.pdf Type Inference for First-Class Messages нагуглилось, надо помедитировать.

edit: мдааа, метапротоколы http://wizzard0.livejournal.com/479545.html?thread=5048633#t5048633

Edited at 2014-12-09 03:26 pm (UTC)

maxim December 9th, 2014
Пока ты сам не напишешь унификацию типов и паттер-мачинг, которые как две ноги одного существа, не видать тебе умиротворения :-)

nponeccop December 9th, 2014
судя по всему, он этот уровень прошёл давно :) унификацией ничего лучше haskell98 не напишещь, т.е. для объектных языков не годится совсем

maxim December 9th, 2014
если бы в его написанной реализации был модули как первоклассные сущности возможно ему бы не понадобилось ООП :-)

wizzard0 December 9th, 2014
см. тред с sorcerer. я не утверждаю, что для этого нужно ООП, но мапить ОО-языки явно придётся.

maxim December 9th, 2014
Кому придется и зачем он должен это делать?

wizzard0 December 9th, 2014
рантайму для web-scale distributed приложений, написанных группой лиц, возможно не знающих друг друга даже; на разных ЯП.

maxim December 9th, 2014
это ты считаешь лучше чем унифицировать два кортежа ? Именно то что делается всю жизнь в бинарных протоколах в том числе и TCP, где кортежами выступают пакеты а полями битовые последовательности ?

Ну-ну :-)

wizzard0 December 9th, 2014
кортеж - унификация данных, а не коданных.

maxim December 9th, 2014
коданные хранятся как данные. или ты работаешь в категорном языке Хагино ?

wizzard0 December 9th, 2014
я понимаю, что в конечном итоге между акторами летают сообщения, которые данные; сообщение описать несложно, мне нужно описать сам актор.

а Хагино я читал давно и не уверен что правильно понял, поэтому не могу подтвердить или опровергнуть это утверждение.

Edited at 2014-12-09 02:47 pm (UTC)

maxim December 9th, 2014
ну я там про актор и типизацию его пайпа написал

sorcerer_ December 9th, 2014
А можно для тупых, в чем проблема, простыми словами?
Почитал про path-dependent выглядит неплохо, в жабе такой штуки нехватало.
Правда, небось, как обычно: path-dependent class от стринга отнаследовать нельзя. :)

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

nponeccop December 9th, 2014
нельзя сделать нормальный вывод типов для языков типа javascript

wizzard0 December 9th, 2014
Скажем так, в TypeScript никогда не будет оператора "is", а typeof так и будет возвращать "function", "object" и т.д.

Есть и другое применение, см. http://wizzard0.livejournal.com/479545.html?thread=5040697#t5040697

wizzard0 December 9th, 2014
> в чем проблема, простыми словами?

(тут я упрощаю местами до потери смысла, но такой сценарий это тоже решило бы)

Сделать так, чтобы можно было сделать к приложению А плагины Б, В (отдельные compilation unit-ы, от разных вендоров) и они могли друг с другом поговорить, не ссылаясь на общую либу с интерфейсами, а ссылаясь на две разных, но при этом чтобы можно было проверить, совместимы ли эти "две разных" в install-time или load-time, а не run-time.

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

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

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

В рантайме с дактайпингом это тривиально, ну в смысле будет работать, но иногда падать;

если есть четвёртая либа и всё видно во время компиляции, то это руками тоже делается, для джавы даже понапридумывали всякие AutoMapper'ы, для дотнета вроде тоже;

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

Да, рантайму для этого потребуется как минимум constraint solver и JIT-компилятор для всех случаев кроме самых тривиальных, где type member layout полностью совпадает.

CLR (только MS Desktop, Mono и Silverlight - нет) + WinSxS к этому пришли достаточно близко (там есть специальные атрибуты, которые позволяют перемапить неймспейс, имя метода или сигнатуру метода, если с каким-то апдейтом оно было рефакторнуто), но констрейнт солвер там работает только по версиям, типы матчатся руками.

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

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

maxim December 9th, 2014
> Сделать так, чтобы можно было сделать к приложению А плагины Б, В (отдельные compilation unit-ы, от разных вендоров) и они могли друг с другом поговорить, не ссылаясь на общую либу с интерфейсами, а ссылаясь на две разных, но при этом чтобы можно было проверить, совместимы ли эти "две разных" в install-time или load-time, а не run-time.

Я это нехуй делать могу сделать в Erlang. У меня #validation{} определенный в одном модуле совпадает с #validation{} определенным в другом модуле если у них совпадают все поля. Т.е. аля унифицируются их типы. Прочекать все перед стартом вообще не проблема, возможно даже в compile-time.

Edited at 2014-12-09 02:33 pm (UTC)

wizzard0 December 9th, 2014
> совпадают все поля
это first-order тип. а если я захочу тебе функцию вернуть?

maxim December 9th, 2014
функция от сравнения двух типов объявленых в разных модулях? и куда ты ее хочешь вернуть? Допустим я тебе ее могу обеспечить в Эрланге.

Edited at 2014-12-09 02:38 pm (UTC)

wizzard0 December 9th, 2014
мммм....

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

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

могу вернуть структуру с именем файла, датой и данными, тут ты можешь проматчить

а если я на самом деле торрент-клиент и тебе хочу вернуть обьект/агент/whatever, который представляет собой абстракцию seekable stream'a с методами соответствующими, один из которых жрёт колбек чтобы отдавать туда данные по мере поступления?

это не данные, это коданные уже. как ты структурной типизацией проматчишь коданные?

maxim December 9th, 2014
ну так у тебя объектын протокол сикабл стрим если реализуют этой версии то ок.
Например вот как выглядят протоколы в эрланге:

receive TypeSignature1 -> Code1;
...
TypeSignatureN -> CodeN end,

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

Где тут ООП нахуй нужно нипанятна мне вообще. у меня такое ощущение что Майкрософты тебя наебали.

wizzard0 December 9th, 2014
хм, описывать через process calculi это занятная мысль, надо над ней подумать.

edit: ну ХОРОШО, а gradual process calculi у нас вообще кто-то умеет?

а также генерировать описание актора в этой семантике из его имплементации, на хоть каком языке?

http://www.cs.cmu.edu/~aldrich/FOOL/FOOL11/FCM.pdf Type Inference for First-Class Messages нагуглилось, надо помедитировать.

Edited at 2014-12-09 03:06 pm (UTC)

maxim December 9th, 2014
ну так а хули там экстрактить можно актора в любой язык я думаю если писать на чем то мощном. документ да, отражает то, что я пытаюсь сказать, хотя хуй его знает как бы я это реализовывал. У меня в унификаторе и матчинге тут были просто конструкторы типов, константы и вайлкарды.

Edited at 2014-12-09 03:13 pm (UTC)

wizzard0 December 9th, 2014
> хотя хуй его знает как бы я это реализовывал
дык :)

есть ещё один нюанс, не очень важный но существенный, предлагаю подумать. у нас тут в протоколе участвуют два равноправных (!) пира, которые занимаются, по сути, protocol negotiation'ом.

при этом согласно gradual typing promise, декораций типов на них никаких изначально нету.

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

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

Edited at 2014-12-09 03:37 pm (UTC)

wizzard0 December 9th, 2014
Э, стоп! Я тут вчитался повнимательнее в твой коммент.

> этой верси
это номинальный тайпинг! а я про структурный спрашиваю!

maxim December 9th, 2014
та не это я версию файла имел ввиду не обращай внимания на это слово.

nponeccop December 9th, 2014
> простого списка импортов а-ля DLL тут не хватит.

Ну так это не совсем система типов тогда, и не система модулей, а "компонентная модель". Этот термин уже здесь кто-то произносил?

И понятно теперь, причём тут контракты.

По "nominal component system" нагуглилось

http://www.jot.fm/issues/issue_2008_01/article4.pdf

The design and formal specification of a new powerful model of nominal subtyping which allows to express many subtyping relationships that could previously only be established with structural subtyping without sacrifying the advantages of nominal subtyping. A sketch of the soundness proof is also given.

Edited at 2014-12-09 11:58 pm (UTC)

AutoMapper это уж слишком упрощенно

Serge Shikov December 14th, 2014
Если судить по вот этому конкретно описанию задачи, то OSGI - то, что на практике в мире Java пытается решать именно такую задачу. Кстати, constraint solver там даже имеется.

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

Гибкости это конечно дает дофига - но и проблем совершенно новых и лишних тоже с собой приносит, причем немало.

Re: AutoMapper это уж слишком упрощенно

wizzard0 December 14th, 2014
От времени даааа!

sorcerer_ December 9th, 2014
> см. "от разных вендоров"

См "опен сорс" :)

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

Дык, берем компоненты, делаем протоколы - пилим софт. В чем проблема неясно. Железо давно так работает и не жужжит. :)

wizzard0 December 9th, 2014
Не, ну понятно что раньше и на ассемблере вот писали, безо всяких вот этих классов методов и те де ))))

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

P2P, децентрализация, вот это всё.

sorcerer_ December 9th, 2014
Дык, протоколы нам на что? :)

wizzard0 December 9th, 2014
Дык я хочу чтобы

0) самое важное! протоколы матчились не по названию а по контенту, почему же Structural Typing. если по названию - то получается ActiveX и COM, это мы уже видели.
1) протокол не текстом а кодом специализировался, и
2) был стандартизованный способ в пакадже и/или DLL декларировать не только "эта прога умеет открывать DOC и TXT" а "эта прога умеет общаться с git репозиториями и монтировать их как FUSE", "в этот документ можно эмбедить такое-то и такое-то" в таком духе.

Примерно в эту сторону копают сейчас все - Android с их Intents, iOS App Extensions, Sandstorm с их Capabilities, MSFT с App Contracts

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

Edited at 2014-12-09 02:27 pm (UTC)

juan_gandhi December 9th, 2014
О, спасибо за линк.

Интересная тема. Я, правда, не понимаю, почему в скале такой шухер с path-dependent; зафиксировать все - и все определено; а не фиксировать - так это где угодно можно накуролесить с помощью includes.

wizzard0 December 9th, 2014
> почему в скале такой шухер с path-dependent

Это, пожалуй, надо не у меня спрашивать, а у xeno_by или еще кого-то...

nponeccop December 10th, 2014
Не, ну почему шухер - понятно: хотят прикрутить вывод типов, ничего не меняя.

justy_tylor December 9th, 2014
А почему только типы? Это общая проблема pattern matching + open-world, когда приходится разруливать в рантайме.

Всё, что можно сделать для более раннего обнаружения несоответствий - переход в closed-world с верификацией при завершении линковки библиотек и датасетов.

ponomarevmv December 10th, 2014
хотелось-бы уточнить, почему не писать все эти термины по-русски? кроме прочего, это даст понять посторонним, что автор не просто пользуется терминологией, но и в курсе, что это все означает.

wizzard0 December 10th, 2014
1) Литературы на русском языке по данным темам я не встречал; невзирая на то, что в статьях немало русскоговорящих авторов — издаются они сугубо на английском.
2) Общепринятых вариантов перевода для многих терминов (например, subtyping или gradual typing) ещё нет, как и переводов большинства публикаций.
3) В таком виде термины сразу являются ключевыми словами для поиска, в отличие от переводных вариантов.
4) "хотелось бы" пишется через пробел, а не через дефис.
5) Как видно из вышеприведённого, знание английского языка для обсуждения поднятых вопросов обязательно в любом случае. Поэтому сомнений в знании терминологии среди тех, кто владеет темой — не возникает :)
6) Если вы всё-таки не знаете английского языка, и хотели бы уточнить что-то конкретное — спрашивайте, буду рад пояснить.

(Screened comment)
wizzard0 December 11th, 2014
Пикча ок. Только великовата.

HERE I FIXED IT

  • 1
?

Log in

No account? Create an account