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, именно.

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

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

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

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

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

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" тоже решают похожую проблему.

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

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

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

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

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

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

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

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

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

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

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

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

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)
  • 1
?

Log in

No account? Create an account