Dec. 9th, 2014

wizzard: (Default)
Блин, вот как научить себя более цинично менеджить приоритеты и планировать таймслоты ЧЕСТНО перед самим собой?

Как согласиться с тем фактом, что чтобы засесть поработать, мне НАДО сходить в кино, или сьездить поговорить про Х, или покормить себя вон тем тортиком, или еще чего? Что на самом деле написать пару страниц бреда "в стол" более важно, чем супермегадедлайн, потому что без этого не выйдет очистить мозги, и суперважная задача будет продвигаться с черепашьей скоростью, или вообще не будет.

Или что с вероятностью К в этот день постучится человек М, и потребуется уделить ему Й часов времени, а потом Ф часов времени обдумывать услышанную Ж.

Уже ж сколько раз пробовал - если действительно это всё вписывать в "зависимости" задач, то точность планирования становится филигранной - что-то типа 15% погрешности на 2 недели вперёд.

Нет же, накатывает идеализм, и планы начинают выглядеть "Красиво и Правильно", но нужно к ним делать тройной запас времени, а незапланированные события приводят к трёхсуточным марафонам по разгребанию хвостов...
wizzard: (Default)
Наконец-то я могу сказать словами то, что меня мучило все эти годы, бгггг :)

Собственно, правильно ли я понимаю, что поскольку для 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 типами какая-то сцуко сложная")

Profile

wizzard: (Default)
wizzard

January 2019

S M T W T F S
  12 345
6789101112
1314 1516171819
202122 23242526
2728293031  

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Aug. 25th, 2025 07:59 pm
Powered by Dreamwidth Studios