Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Литобзор

Во-первых хочу посоветовать блестящую публикацию Нады Амин и Росса Тейта «Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers» (15–45 минут чтения).

Статья очень хорошо и доступно написана. Разобраться сможет любой, кто прилично знает Java или Scala. Прочитать её будет крайне полезно всем, кто хочет поглубже понять generics в типизированных объектно-ориентированных языках, и не только семейства Java.

Дело в том, что системы типов Java и Scala несостоятельны: авторы приводят код метода `coerce<T>(v)`, который без использования unsafe cast или ещё каких-либо хаков берёт любое значение `v` какого угодно типа и выплёвывает его под видом значения типа `T`. Проблема вскрывается только во время выполнения, при попытке сделать что-нибудь с этим значением.

Идея в том, что алгоритмы проверки типов полагаются на существование объектов определённых типов как на признак заменимости типов (subtyping evidence): такие объекты по идее невозможно было бы сконструировать, если бы соответствующее отношение заменимости типов не выполнялось.
Авторы алгоритмов, по-видимому, упустили из виду, что они работают не с тотальными языками вроде Agda или Idris. В иных языках “пустые по идее” типы можно “населить” незавершающимися вычислениями ⊥ или даже вообще имеется “универсальное значение” null, подходящее в качестве значения любого непримитивномого типа.
Первое не является проблемой для Java, т.к. язык не поддерживает ленивых вычислений, и метод, содержащий расходящееся вычисление, просто никогда не завершится, но для других нетотальных языков надо помнить: в качестве признаков можно использовать только значения, помеченные как неленивые, т.е. подлежащие обязательному вычислению, даже если вычисленное значение дальше никак не используется.
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 27 comments

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…