Собственно, правильно ли я понимаю, что поскольку для 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
Не совсем правильно. Если быть точным, то 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.
Вот хочется gradual contracts, именно.
Почитал про path-dependent выглядит неплохо, в жабе такой штуки нехватало.
Правда, небось, как обычно: path-dependent class от стринга отнаследовать нельзя. :)
В общем случае если проблема стандартная: как сделать такие контракты, чтоб и 100 программеров могли писать разное, и все не ломалось, и багов было мало. То уже решено вроде: все всегда делать во время компиляции и лобзиком по шаблонам (см. эпохальный труд Баткина).
(тут я упрощаю местами до потери смысла, но такой сценарий это тоже решило бы)
Сделать так, чтобы можно было сделать к приложению А плагины Б, В (отдельные compilation unit-ы, от разных вендоров) и они могли друг с другом поговорить, не ссылаясь на общую либу с интерфейсами, а ссылаясь на две разных, но при этом чтобы можно было проверить, совместимы ли эти "две разных" в install-time или load-time, а не run-time.
а также, если эти либы референсят депенденсю Г разных версий, чтобы можно было определить, пересекается ли множество совместимых версий депенденси чтобы вгрузить ее 1 штуку.
Понятное дело, либы при этом должны экспортировать метаданные о типах, простого списка импортов а-ля DLL тут не хватит.
> все всегда делать во время компиляции
см. "от разных вендоров".
В рантайме с дактайпингом это тривиально, ну в смысле будет работать, но иногда падать;
если есть четвёртая либа и всё видно во время компиляции, то это руками тоже делается, для джавы даже понапридумывали всякие AutoMapper'ы, для дотнета вроде тоже;
а вот так чтобы доказанно правильно автоматически, в тех случаях, когда это можно - такого я не видел.
Да, рантайму для этого потребуется как минимум constraint solver и JIT-компилятор для всех случаев кроме самых тривиальных, где type member layout полностью совпадает.
CLR (только MS Desktop, Mono и Silverlight - нет) + WinSxS к этому пришли достаточно близко (там есть специальные атрибуты, которые позволяют перемапить неймспейс, имя метода или сигнатуру метода, если с каким-то апдейтом оно было рефакторнуто), но констрейнт солвер там работает только по версиям, типы матчатся руками.
Ну и всяческие "генераторы прокси-классов из WSDL" тоже решают похожую проблему.
В каком-то смысле это, конечно, "архитектура эльфов", но при правильной реализации могло бы дать возможность очень и очень глубокой интеграции приложений друг с другом - без нарушений статических гарантий.
См "опен сорс" :)
> В каком-то смысле это, конечно, "архитектура эльфов", но при правильной реализации могло бы дать возможность очень и очень глубокой интеграции приложений друг с другом - без нарушений статических гарантий.
Дык, берем компоненты, делаем протоколы - пилим софт. В чем проблема неясно. Железо давно так работает и не жужжит. :)
Просто думается, что очень хорошо было бы, если бы компоненты и приложения могли бы платформонезависимо детально декларировать свою совместимость друг с другом - сейчас это ложится на мейнтейнеров дистрибов и платформ соотв-но.
P2P, децентрализация, вот это всё.
Интересная тема. Я, правда, не понимаю, почему в скале такой шухер с path-dependent; зафиксировать все - и все определено; а не фиксировать - так это где угодно можно накуролесить с помощью includes.
Это, пожалуй, надо не у меня спрашивать, а у
Всё, что можно сделать для более раннего обнаружения несоответствий - переход в closed-world с верификацией при завершении линковки библиотек и датасетов.
2) Общепринятых вариантов перевода для многих терминов (например, subtyping или gradual typing) ещё нет, как и переводов большинства публикаций.
3) В таком виде термины сразу являются ключевыми словами для поиска, в отличие от переводных вариантов.
4) "хотелось бы" пишется через пробел, а не через дефис.
5) Как видно из вышеприведённого, знание английского языка для обсуждения поднятых вопросов обязательно в любом случае. Поэтому сомнений в знании терминологии среди тех, кто владеет темой — не возникает :)
6) Если вы всё-таки не знаете английского языка, и хотели бы уточнить что-то конкретное — спрашивайте, буду рад пояснить.