про ООП, модули и типизацию
Dec. 9th, 2014 07:42 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
wizzardНаконец-то я могу сказать словами то, что меня мучило все эти годы, бгггг :)
Собственно, правильно ли я понимаю, что поскольку для 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 типами какая-то сцуко сложная")
Собственно, правильно ли я понимаю, что поскольку для 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 типами какая-то сцуко сложная")
