akuklev: (ДР Цертуса 2011)
Ура, ура, у меня теперь есть прекрасная книжка Аркадия Эммануиловича Мильчина! Спасибище Графу!

И ещё плакат со всеми странами и территориями в мире, отсортированными по площади. Одна беда с плакатом, что там спорно решён вопрос со спорными/аннексированными территориями. Тяжело понять, почему если во многих случаях сочтено, что спорную территорию лучше вынести отдельно и пометить как спорную (Фолклендские острова, Косово и мн. др.), и даже Калининградская область вот отделена от России, нельзя сделать то же самое именно в случае Крыма и Нагорного Карабаха.
akuklev: (ДР Цертуса 2011)
Подумалось тут, что сдача теоретического экзамена на вождение в Германии в виде multiple-choice-теста — анахронизм. Да, там и видео есть, и всякий другой “типа-интерактив”, но я себе в два счёта могу представить разумную игру для планшета на тему отработки этих самых тем, которая одновременно и обучение и тест. Прошёл — сдал экзамен.

Единственный вопрос — как доказать, что игра не менее эффективна, чем классический экзамен? Разумеется, это можно сделать только одним способом — “клиническими” испытаниями. В медицине (кстати, совсем недавно, на самом деле) утвердились наконец разумные протоколы испытаний и вообще подход, называемый “доказательной медициной”. А вот в педагогике и тестировании, мне кажется, как-то слабо с этим. И это явный прокол.

Аналогично, обучение навыкам первой помощи на права в Германии в большинстве случаев чистейшая профанация, и в первую очередь именно потому что там просто быстро рассказывают, в то время как по уму надо это перемежать многократной проработкой кейсов в игровой форме, чтобы навык запоминался всеми системами восприятия и закреплялся многократным повторением. Что, опять же, неплохо бы доказать “клиническими” испытаниями. Когда что-то такое навязывают десятку миллионов людей в год, неплохо бы иметь данные об эффективности методов.

Интуитивно мне кажется, что игра и learning-by-doing (т.е. обучение через прикладные проекты) — самые эффективные способы наработки навыков. Кстати, у всех высших приматов, кроме человека, обучение происходит, насколько я понимаю, именно только так. Но если честно, это кто-то измерял качественно?

TouchBar

Nov. 26th, 2016 09:49 am
akuklev: (ДР Цертуса 2011)
Вообще идея рисовать/писать на функциональных клавишах, какое у них будет действие в данном конкретном случае — очень хорошая идея, она напрашивается с конца восьмидесятых, когда хотелось вот эту нижнюю полоску в Нортоне расположить прямо на клавишах. И TouchId в углу для подтверждения умеренно серьёзных и неотменябельных действий — тоже вещь, о которой даже лично я говорил уже году в 2004'ом, а так люди наверное об этом и намного раньше думали.

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

<чисто-поныть>
А ещё нельзя ли всё-таки взять и сделать где-нибудь нормальный блок классических клавиш навигации (Ins/Del, Home/End, PgUp/PgDn)?...
</чисто-поныть>
akuklev: (ДР Цертуса 2011)
А что вы думаете про свежепоявившийся семиместный Škoda Kodiaq? Выглядит как очень занятная машина, которая в варианте со сложенными сиденьями является близка по вместимости к Škoda Yeti, только ездит получше, и при необходимости можно разложить ещё два сиденья с Isofix'ами.

Денег у меня, конечно, как всегда нет, но на сайте Шкоды описываются симпатичные варианты лизинга, о которых можно было бы думать в долгосрочной перспективе, когда мне удастся наконец долги раздать.
akuklev: (ДР Цертуса 2011)
Вот у обычных ручных пылесосов кусок с мотором и ёмкостью для мусора расположен отдельно от щётки, чтобы щётку можно было сделать максимально компактной и плоской и она везде пролезла. Почему создатели робопылесосов не пошли таким путём и пытаются запихать всё в моноблок?

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

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

* * *

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



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

Полба

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

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

JoinadFix

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

Вот я, кажется, и понял каким образом соотносятся эффекты и многопоточность.Read more... )
akuklev: (ДР Цертуса 2011)
Как выясняется, есть глубокая аналогия между монадическими эффектами и индуктивными типами. А что соответствует с эффектной стороны высшим индуктивным типам? Мне кажется, у меня есть ответ на этот вопрос для важного частного случая.Read more... )
akuklev: (ДР Цертуса 2011)
То, что правые популисты приходят во власть, — ничтожная проблема по сравнению с тем, что они приходят во власть демократическим путём именно благодаря право-популистской риторике.

* * *

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

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

ICQ

Nov. 10th, 2016 02:57 am
akuklev: (ДР Цертуса 2011)
Решил тут зайти в аську, посмотреть кто онлайн. Последний раз я там был лет пять назад. Из трёх сотен контактов трое онлайн. Мъртвэ.
akuklev: (ДР Цертуса 2011)
На днях снилось, что я работаю водителем гибридного троллейбуса. Не спрашивайте.
Однако (!) четыре педали и около 20 передач. %-)
akuklev: (ДР Цертуса 2011)
У меня с детства идеосинкразия на имена Вахтанг и Ядвига, с одной стороны я знаю живых людей, которых так зовут. Однако когда я слышу или произношу эти имена, у меня в голове ассоциации не с людьми, а с предметами, причём чисто визуальные. Вахтанг, например — причудливое античное устройство, сочетающее черты бумеранга, штангенциркуля и плоской пружины. Ядвига — древнее причудливое змеевидное сучковато-коленчатое деревянное сельскохозяйственное устройство, где-то между мотыгой и сохой.
akuklev: (ДР Цертуса 2011)
Кто не знает, сейчас уже продаются SD-карточки на 1 TiB. Говорят к концу года должна выйти такого же размера MicroSD, ага.

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

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

Read more... )
akuklev: (ДР Цертуса 2011)
Не знаю, чего на него ругаются. По мне так тринадцатидюймовая версия — это просто проапгрейженный Air, всё отлично (в рамках традиции Apple).

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

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... )
akuklev: (ДР Цертуса 2011)
Как до жирафа. Всего-то лет десять прошло. В общем я о том, что 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 из/в указанной границы. И всё работает.
akuklev: (ДР Цертуса 2011)
В магазине C&A в центре Гёттингена нередко случаются магазинные кражи и иногда орудуют карманники (жертвой каковых вчера и стала моя дорогая жена), в связи с этим в магазине установлено восемь дорогих и качественных всенаправленных потолочных камер. Кроме камер в специальной комнате безопасности, она же кабинет заведующей, установлено 16 мониторов, на которые транслируется изображение с камер, полноценная CCTV-система, видимо совсем недешёвая.

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

Okmij

Oct. 25th, 2016 07:47 am
akuklev: (ДР Цертуса 2011)
Вчера у меня наконец дошли руки посмотреть на статью 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 коммутировали), я вообще пока не встречал удовлетворительного подхода к этому вопросу, если работать в терминах монад/комонад, а не в терминах стрелок. Но по идее оно должно быть, собственно монадами описываются эффекты, у которых контракты накладываются на интерпретатор (если он есть), а процедуры могут полагаться на их выполнение, а комонадами эффекты, налагающие на использующую их процедуру обязательства по выполнению контрактов (например, использовать вызов команды только один раз).
akuklev: (ДР Цертуса 2011)
Предлагается трактовать обозначения [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... )

Ыыы

Oct. 24th, 2016 08:08 am
akuklev: (ДР Цертуса 2011)
Боже, как я сразу не узнал?
Высшие ℧-модули, которые у меня вырисовываются в мемо про линейные типы из идеи про квантовые трансдьюсеры — это же просто геометрии Зарисского*. Как же я сразу не сообразил-то?.. Теперь я понимаю откуда у Зильбера квантовый гармонический осциллятор из теории моделей всплывает.


____
(* У геометрий вылезающих из теорий на первом уровне “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-категорию? Было бы красиво.)
Page generated Jul. 28th, 2017 04:47 pm
Powered by Dreamwidth Studios