?

Log in

Alexander Kuklev's Journal

> recent entries
> calendar
> friends

> profile
> previous 20 entries

Saturday, January 17th, 2015
2:17 pm
Delayed Настоящим объявляю, что все мои персональные данные, тексты, фотографии, рисунки, переписка и т.п. являются объектами моего авторского права (согласно Бернской Конвенции), и оповещаю «ЖЖ» (LiveJournal, Inc / SUP Media) о том, что разглашение, копирование, распространение моей личной информации в коммерческих целях равно как и любые другие противоправные действия по отношению к моему профилю в социальной сети строго запрещены.

Для коммерческого использования всех вышеупомянутых объектов авторского права в каждом конкретном случае необходимо мое письменное разрешение.

Гёттинген
17 января 2015 г.
Александр Куклев

(5 comments | comment on this)

Saturday, November 26th, 2016
9:49 am - TouchBar
Вообще идея рисовать/писать на функциональных клавишах, какое у них будет действие в данном конкретном случае — очень хорошая идея, она напрашивается с конца восьмидесятых, когда хотелось вот эту нижнюю полоску в Нортоне расположить прямо на клавишах. И TouchId в углу для подтверждения умеренно серьёзных и неотменябельных действий — тоже вещь, о которой даже лично я говорил уже году в 2004'ом, а так люди наверное об этом и намного раньше думали.

Так что появление в новых МакБуках Про TouchBar'а — явление логичное. Только почему без тактильного фидбека и тактильного разделения зон? Мне кажется, это жуткая недоработка. А ещё, нельзя ли по такому случаю наконец убрать строчку меню сверху экрана? Для части приложений оно нафиг не нужно (например, браузеры и мессенжеры), а для тех где нужны гораздо лучше подходит майкрософтовский Ribbon (в варианте Office 2016 for Mac он мне особенно нравится). В строке меню кроме самого ненужного меню из полезного только часы, индикатор текущей раскладки клавиатуры и индикатор заряда батареи, всё остальное либо должно быть в TouchBar'е, либо вообще лишнее.

<чисто-поныть>
А ещё нельзя ли всё-таки взять и сделать где-нибудь нормальный блок классических клавиш навигации (Ins/Del, Home/End, PgUp/PgDn)?...
</чисто-поныть>

(20 comments | comment on this)

Monday, November 21st, 2016
5:54 am - Škoda Kodiaq
А что вы думаете про свежепоявившийся семиместный Škoda Kodiaq? Выглядит как очень занятная машина, которая в варианте со сложенными сиденьями является близка по вместимости к Škoda Yeti, только ездит получше, и при необходимости можно разложить ещё два сиденья с Isofix'ами.

Денег у меня, конечно, как всегда нет, но на сайте Шкоды описываются симпатичные варианты лизинга, о которых можно было бы думать в долгосрочной перспективе, когда мне удастся наконец долги раздать.

(28 comments | comment on this)

5:47 am - Роботопылесосное
Вот у обычных ручных пылесосов кусок с мотором и ёмкостью для мусора расположен отдельно от щётки, чтобы щётку можно было сделать максимально компактной и плоской и она везде пролезла. Почему создатели робопылесосов не пошли таким путём и пытаются запихать всё в моноблок?

Понятно же, что нельзя запихнуть систему уровня прекрасных Miele Blizzard CX1 Cat & Dog PowerLine или Siemens Q8.0, которые реально не подметают, а всасывают грязь с пола и глубоко высасывают её из ковров, в моноблок размером с iRobot Румбу, и при этом даже маломощная Румба нифига не пролезает в углы и под диваны так, как это делают щётки тех самых ручных пылесосов.

Неужели настолько сложно и дорого сделать двублочную систему из робощётки и катающейся хвостиком за ней базы?..

* * *

Не говоря уже о том, что робот для качественной влажной уборки вообще может быть сделан только таким образом. Все имеющиеся на данный момент на рынке роботы для влажной уборки просто водят по полу мокрой тряпочкой: во-первых не осуществляется должного нажима на тряпочку, во-вторых, тряпка становится грязной много раз за уборку, и хозяевам предлагается менять её вручную. Нормальные аппараты для влажной уборки работают совсем по-другому: там вместо тряпки работает поворачивающийся валик, который смачивается свежей водой с моющей в данный момент стороны, а с тыльной стороны очищается по принципу моющего пылесоса: туда под давлением загоняется горячая вода с моющим средством, и тут же с чудовищной силой всасывается, забирая с собой всю грязь. В то же время, засасывающая сила пылесоса используется для высушивания свежепомытого пола. В некоторых вариантах можно снять валик и использовать прибор просто как моющий пылесос для ковров, матрацев и мягкой мебели, что тоже полезная в хозяйстве вещь. Самый компактный прибор этого класса (компактность, увы, не бесплатная: минусом является то, что валик медленно и не очень хорошо очищается, да и режима моющего пылесоса нет) — Kärcher FC 5:



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

(18 comments | comment on this)

Thursday, November 17th, 2016
4:34 pm - Полба
В прошлое воскресенье я узнал две вещи, и мой мир никогда не будет прежним. Во-первых я теперь знаю что такое полба (и с удивлением узнал, что я её ел), а во-вторых как переводить немецкое слово «Dinkel».

* Строго говоря, «Dinkel» — это один конкретный вид полбы: спельта.

(3 comments | comment on this)

Sunday, November 13th, 2016
5:08 am - JoinadFix
Внезапно понял, что операции из вчерашнего поста следует называть join и reduce, причём join имеет прямое отношение к join calculus, прекрасному подходу к многопоточности без нелокальной синхронизации, близкому к Actor Model и линейной логике. Просто по всему выходит, что высший аналог MonadFix это в точности джойнада, допускающая интерпретацию join calculus. Соответственно, вчерашний пост проапдейтил. Коль скоро у меня любая монада с нулём тривиальным образом является джойнадой, выходит что в терминах последних можно интерпретировать наконец императивный код не только с мутабельным состоянием, вводом-выводом, исключениями и прочими delimited continuation passing, но и с использованием любой разумной многопоточности, не прибегающей (к нереализуемой физически) нелокальной синхронизации.

Вот я, кажется, и понял каким образом соотносятся эффекты и многопоточность.Read more...Collapse )

(12 comments | comment on this)

Saturday, November 12th, 2016
5:49 am - Высшие монады и “поле с одним элементом”
Как выясняется, есть глубокая аналогия между монадическими эффектами и индуктивными типами. А что соответствует с эффектной стороны высшим индуктивным типам? Мне кажется, у меня есть ответ на этот вопрос для важного частного случая.Read more...Collapse )

(3 comments | comment on this)

Friday, November 11th, 2016
1:04 am - Политическое
То, что правые популисты приходят во власть, — ничтожная проблема по сравнению с тем, что они приходят во власть демократическим путём именно благодаря право-популистской риторике.

* * *

Множество людей вокруг пишет, как было бы хорошо подкрутить демократические процедуры в США и Великобритании, чтобы в США выиграла Клинтон, а в Великобритании проголосовали против Брекзита, ну то есть в идеале просто вместо демократии просто учитывали только мнение пишущего (конечно не его одного, а ещё скольких-то десятков миллионов его единомышленников, это звучит солиднее и вполне безопасно, они же имеют такое же мнение). Вот нет, не так.
Надо что-то такое подкрутить (я уж не знаю где), чтобы уровень дискусси был вообще другой!

Не вот это вот соревнование доктрины «Мы исконно круче всех, гноби чужаков!» с доктриной «Мы особые, гноби консерваторов и буржуев!» (консенсус им удаётся найти разве что где-то в области антисемитизма), а содержательная дискуссия.
В отношении Евросоюза полно далеко ведущих и непростых структурных и стратегических вопросов — вот уж по поводу чего можно и нужно содержательно дискутировать. Но эти дискуссии протекали где-то в эмпиреях, а реальный исход выборов определялся спором между «от Брекзита будут чудовищные убытки и лишняя волокита» и «без Брекзита к нам понаедет ещё больше унтерменшей». А кандидаты с такой риторикой как Д. Трамп и такой подноготной Х. Клинтон в здравом обществе должны просто не иметь шансов получить хоть по 5% голосов и отсеиваться ещё до праймериз.

(29 comments | comment on this)

Thursday, November 10th, 2016
2:57 am - ICQ
Решил тут зайти в аську, посмотреть кто онлайн. Последний раз я там был лет пять назад. Из трёх сотен контактов трое онлайн. Мъртвэ.

(26 comments | comment on this)

Monday, November 7th, 2016
11:37 pm - Снилось мне
На днях снилось, что я работаю водителем гибридного троллейбуса. Не спрашивайте.
Однако (!) четыре педали и около 20 передач. %-)

(4 comments | comment on this)

11:35 pm - Необычные имена
У меня с детства идеосинкразия на имена Вахтанг и Ядвига, с одной стороны я знаю живых людей, которых так зовут. Однако когда я слышу или произношу эти имена, у меня в голове ассоциации не с людьми, а с предметами, причём чисто визуальные. Вахтанг, например — причудливое античное устройство, сочетающее черты бумеранга, штангенциркуля и плоской пружины. Ядвига — древнее причудливое змеевидное сучковато-коленчатое деревянное сельскохозяйственное устройство, где-то между мотыгой и сохой.

(2 comments | comment on this)

Friday, November 4th, 2016
1:06 am - 640K ought to be enough for anybody
Кто не знает, сейчас уже продаются SD-карточки на 1 TiB. Говорят к концу года должна выйти такого же размера MicroSD, ага.

У меня вот в компьютере SDD такой, и там 83% свободно, не смотря на то, что место я не экономлю вообще, на компьютере стопками лежат фильмы, десятки гигабайт музыки (всё что я слушаю и слушал вообще), архивы всего и вся. При таких запасах памяти уже можно более или менее позволить себе вообще все изменяемые ручками файлы хранить вместе с историей изменений с момента создания, фактически во write-only режиме. Вот для меня реально достаточно. Я понимаю, что есть любители очень высококачественного видео, RAW-фотографий и RAW-музыки, может им понадобится кроме жеского диска ещё десяток SD-карточек. Но в целом проблема объемов решена для любых персональных нужд. По крайней мере, пока не появилось какого-нибудь 3D-видео.

В конце сентября Spin Transfer Technologies анонсировала чип STT-MRAM памяти по плотности всего в десять раз уступающей тем самым чипам, при помощи которых в microSD влезает терабайт, только скорость у этой памяти в тысячу раз быстрее. Очень ждём!

Read more...Collapse )

(7 comments | comment on this)

Thursday, November 3rd, 2016
12:11 am - Новый MacBook Pro
Не знаю, чего на него ругаются. По мне так тринадцатидюймовая версия — это просто проапгрейженный Air, всё отлично (в рамках традиции Apple).

Что все разъемы унифицировали меня лично радует, давно пора. Флешки и сетевые карты под этот разъем уже поспели, как и провода для переферии (где с одной стороны USB Type-C, а с другой любой старый USB или DisplayPort/HDMI/DVI/VGA/RS-232). Годик-другой походим с переходниками, а потом забудем как страшный сон, что какие-то другие разъёмы вообще были. Дать индустрии толчок к переходу на USB Type-C — благое дело.

(18 comments | comment on this)

Friday, October 28th, 2016
6:11 pm - Коэффекты
(Ниженаписанное — спекулятивный черновик для внутреннего применения, приведённые утверждения пока даже не проверены, не говоря о формальных доказательствах.)

Purely functional total computations are excellently understood both syntactically and semantically, they are very easy to work with mathematically. The business of describing effectful computations urges to extend this result from total pure functions to procedures written in powerful general purpose imperative programming languages. Procedures are assumed to be typed and composable (thus, form a category, say Proc; actually, a monoidal category we are to interpret procedures with more than one argument) and to faithfully include total pure functions (thus, there should be a monoidal functor proc : Func -> Proc). This structure is enough to interpret plain (i.e. without loops and other control structures) ALGOL-style procedure definitions, i.e. sequences of instructions and let-definitions. Control structures have to be described separately as additional generators of the Proc category.Read more...Collapse )

(4 comments | comment on this)

Thursday, October 27th, 2016
5:22 am - Как же до меня медленно доходит!
Как до жирафа. Всего-то лет десять прошло. В общем я о том, что translucent modules это “виртуальный” uncurrying тайпклассов.

Давайте работать в терминах предикативного λωΠΣW-исчисления, без каких либо предположений о существовании вселенных. Т.е. у нас как термы, так и типы могут быть зависимы как от термов, так и от типов, однако мы не смешиваем термы и типы, как это принято в традиции MLTT, благодаря тому что там подразумевается, что вселенные у нас есть.

Если у нас есть обыкновенный зависимый тип навроде Fin[n : Nat], то функцию f типа
Π(n : Nat).Π(m : Fin[m]).R никто не мешает оформить как f : Π(x : BoundedNat).R, где BoundedNat := Σ(bound : Nat).Fin[bound].

Вот и когда у нас есть зависимый от типов тип навроде Order[T] и полиморфная функция f : ∀(T).Π(o : Order[T]).R, мы хотим иметь возможность эквивалентно написать f : Π(x : Ordered).R, где Ordered что-то вроде Σ(T).Order[T], при в терминах Σ-типов мы это выразить не можем, T не терм, а тип. В MLTT мы можем аппроксимировать этот тип через U-Ordered := Σ(T : U).Order[T], где U — какая-нибудь вселенная, однако в этом случае мы фиксируем вселенную перед определением функции, и таким образом теряем требование, чтобы функция была параметрически полиморфна по T.

Отметим, что в MLTT сигнатура Π(T : U).Π(o : Order[T]).R гарантирует параметрическую полиморфность благодаря тому, что т.е. вселенные в MLTT не имеют элиминаторов и синтаксически невозможно написать неполиморфную функцию такой сигнатуры; однако двойственная ей через uncurrying сигнатура Π(x : U-Ordered).R уже ничего такого не гарантирует.

Так вот translucent modules, они же “records with abstract type members” это такой синтаксический сахар, который позволяет нам жить и писать так, как будто бы uncurrying для ∀(X).Y[X] существовал, получается такой специальный “рекорд” (X : ∗, y : Y[X]), в котором поле X такое специальное, что честной проекции на него не существует, но мы тщательно делаем вид, что она существует при помощи path dependent types (т.е. записей вида o.X), только ведёт себя не как все нормальные отображения, а как-то особенно хитро, на самом деле в точности так, чтобы "λo : (X : ∗, y : Y[X]). blablabla o.X blablabla" всегда можно было desugar'нуть в “Λ(X : ∗).λ(y : Y[X]). blablabla X blablabla”.

Семантически транслюсцентный модуль (рекорд с одним или несколькими абстрактными полями) следует понимать как типозависимый тип (тайпкласс) R[T1 T2 .. Tn : ∗], просто представленный синтаксически нетривиальным образом. В языках с развитой системой модулей, абстрактные поля могут иметь не только тип Type, но и тип иного транслюсцентного модуля, скажем M := (O : Ordered, x : X[O.Carrier],..), всё спокойно это дешугарится в вышеописанную схему, просто M[T : ∗] := (order : Order[T], x : X[T],..), в процессе, правда, возникнут higher kinded parameters, если тип абстрактного поля сам был параметризован. Функции, возвращающие translucent module после дешугаринга возвращают просто параметризованный одним или несколькими типами рекорд, т.е. f : X -> (∀(T).M[T]), функции, принимающие translucent module дешугарятся в полиморфные: f : (l : List) -> List.Item превращается в f : ∀(T). List[T] -> T. После такого дешугаринга можно заменить все ∀(T) на Π(T : U) без потери строгости, вот и всё. (Насколько я понимаю, higher kinded ∀'s тоже заменяются на Π's без потери строгости, хотя это совсем не элементарный результат.) Вот и ответ на мой вопрос про семантику сложных структур из прошлого поста.

А, да, про системы модулей в языках с отношением subtyping'а: указание верхних и нижних границ можно рассматривать на уровне семантики как дополнительные поля рекорда, обеспечивающие конверсию в/из абстрактного параметра T из/в указанной границы. И всё работает.

(7 comments | comment on this)

1:09 am - Прямо сюжет для сатирической передачи xtra3
В магазине C&A в центре Гёттингена нередко случаются магазинные кражи и иногда орудуют карманники (жертвой каковых вчера и стала моя дорогая жена), в связи с этим в магазине установлено восемь дорогих и качественных всенаправленных потолочных камер. Кроме камер в специальной комнате безопасности, она же кабинет заведующей, установлено 16 мониторов, на которые транслируется изображение с камер, полноценная CCTV-система, видимо совсем недешёвая.

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

(7 comments | comment on this)

Tuesday, October 25th, 2016
7:47 am - Okmij
Вчера у меня наконец дошли руки посмотреть на статью Freeer monads Олега Киселёва et al., и реализацию — библиотеку Eff для хаскеля. Вот блин, а. Это же надо так уметь. Шедевр, тончайшая работа.

На чистом хаскеле безо всяких макросов превратили его фактически в язык с модулярными алгебраическим эффектами. Описываешь свой эффект как в языках с алгебраическим эффектами через параметризованный GADT, т.е. просто пишешь какие ты хочешь добавить в ambient language команды с описанием их сигнатуры, пишешь ему модулярный интерпретатор, а дальше можно это свободно перемежать с другими описанными в такой же форме эффектами, умная бубиотика определяет параметрическую монаду Eff '[list of effects], всё настолько круто, что там не только композиция эффектов работает сама и полиморфные по эффектам процыдурки сами получаются, но даже effect inference для do-нотации в какой-то мере работает. И семантически очень красиво выходит: алгебраическое описание эффекта это индуктивный тип * -> *, для него конструируется левое расширение Кана, а на получившемся функторе задаётся свободная монада, вложение индуктивных типов превращается во вложение монад, соответственно “описания эффектов” можно комбинировать через disjoint sums, прощайте монадные трансформеры. В библиотеке описаны стандартные эффекты — IO, State, Non-Determinism, и всё что можно описать через Delimited Continuations (эксепшены, кооперативный мультитрединг/сопроцедуры и т.д.).

Заодно понятно, каким образом будет выглядеть комбинирование эффектов с зависимыми типами. Кажется, там ничего не сломается, кроме того что Eff станет вообще говоря относительной монадой (“монадоподобный объект, не являющийся эндофунктором”). Единственное, что мне пока не понятно — это как в сигнатуре эффекта указывать соотношения (например требовать, чтобы вызовы ReadEnv коммутировали), я вообще пока не встречал удовлетворительного подхода к этому вопросу, если работать в терминах монад/комонад, а не в терминах стрелок. Но по идее оно должно быть, собственно монадами описываются эффекты, у которых контракты накладываются на интерпретатор (если он есть), а процедуры могут полагаться на их выполнение, а комонадами эффекты, налагающие на использующую их процедуру обязательства по выполнению контрактов (например, использовать вызов команды только один раз).

(14 comments | comment on this)

5:48 am - Сабтайпинг для индуктивных типов
Предлагается трактовать обозначения [T :> Nat] и [T <: Nat] как [T : NNO] и [T : CoNNO] соответственно, где
@Structure NNO:
  @on N : Type
  zero : N
  succ : N -> N

@Structure CoNNO:
  @on N
  rec[T : NNO](n : N) : T
  rec[:T](zero) = T.zero
  rec[:T](succ(:n)) = T.succ(rec[T](n))


Отметим, что если N1 N2 : NNO ∧ CoNNO, то между типами N1 и N2 имеется изоморфизм, причём каноническим представителем этого класса эквивалентности типов является
@Family Nat:
  zero : Nat
  succ : Nat -> Nat


Для любого индуктивного типа IndT можно автоматически генерировать структуры IND-T и CoIND-T, таким образом проясняя что подразумевается под [T :> IndT] и [T <: IndT]. Наличие таких обозначений позволяет в общем виде описать тип рекурсора для любых индуктивных типов:
IndT.rec[X <: IndT <: Y](x : X) : Y

Read more...Collapse )

(comment on this)

Monday, October 24th, 2016
8:08 am - Ыыы
Боже, как я сразу не узнал?
Высшие ℧-модули, которые у меня вырисовываются в мемо про линейные типы из идеи про квантовые трансдьюсеры — это же просто геометрии Зарисского*. Как же я сразу не сообразил-то?.. Теперь я понимаю откуда у Зильбера квантовый гармонический осциллятор из теории моделей всплывает.


____
(* У геометрий вылезающих из теорий на первом уровне “type of generic points, i.e. equivalence classes of model elements modulo observational distinghishability”, на втором “type of generic point couples”, “type of generic point triples” и т.д., у таких геометрий автоматически есть отображение из подвешивания n-ного уровня в (n + 1)-ый, т.е. это спектры. Интенесно, образуют ли геометрии Зарисского AT-категорию? Было бы красиво.)

(comment on this)

Sunday, October 23rd, 2016
5:18 am - Коданные и параметричность, диалгебры
Когда мы говорим Nat-алгебра, подразумеваем объект, снабженный морфизмами zero и succ.

@Structure NatAlgebra(@on N : Type):
  zero : N
  succ : N -> N


Когда говорим Nat (индуктивный тип), подразумеваем инициальный объект в категории таких алгебр. Когда говорим CoNat (коиндуктивный тип), подразумеваем терминальный объект в категории таких алгебр, если он существует. Терминальность CoNat означает, что для всякой Nat-алгебры A существует каноническое отображение extend[A] : A.N -> CoNat.

А теперь внимание: всякая определимая синтаксически (средствами той или иной теории типов) чистая функция вида
f : [A : NatAlgebra] A.N -> X
задаёт в том числе и f* : CoNat -> X, и может благодаря параметрическому полиморфизму обязана восстанавливаться из неё: f[A] = f* ∘ extend[A]. Т.е. задать функцию из коиндуктивного типа данных структуры F с это абсолютно то же самое, что определить полиморфную функцию для всех F-алгебр.

Замечательная особенность параметрического полиморфизма состоит в том, что он продолжает работать и в ситуации, когда терминального объекта не существует. Read more...Collapse )

Мне по сей день неизвестно, как в рамках диалгебраической семантики проинтерпретировать индуктивно-рекурсивные типы. Специалисты, ау! Кто-нибудь знает хоть что-нибудь про это? Оно не гуглится совершенно.

Это невероятно интересный вопрос, т.к. двойственные к ним типы — это те самые Very Dependent Types (= Reedy Limits), при помощи которых можно интерпретировать всякие симплициальные типы и обобщённые алгебраические теории (GATs).

____
* Структура a la Tarski вселенных может быть описана в терминах индукции-рекурсии, соответственно если можно будет определить структуру TarskiAlgebra, то функции полиморфные по типам [T : Type] X -> Y можно будет эквивалентно описывать как структуры полиморфные по [Univ : TarskiAlgebra] (T : Univ) X -> Y.

(8 comments | comment on this)

> previous 20 entries
> top of page
LiveJournal.com