дыбр

[juan_gandhi]

 Хотя бы рано не надо было идти. В 10 первый доклад, про батчинг реквестов HTTP в контексте хаскеля. Ну это. В ZIO это как-то легче читается... да и пишется наверно. Но в целом хороший доклад, ладно. Просто мне еще и стиль не нравится, шрифтом курьер, серые буквы на черном (вообще в текстовой моде), да еще без нужды буквы все мелкие. Зато сорсы сверкают, как будто тут у нас 1993-й год, ярко-зеленые keywords, серые собственно идентификаторы, и еще что-то там синее, что ли.

Ладно, херня.

В 11 Тони Моррис задвигал про зиперы. Прикольно так, не спеша, для народа, с производными. Но как-то чуток кондовато - но контент миленький.

В 11 что, обед; сел с Шарлин и с каким-то горячим восточным парнем, то ли Абрахам его зовут, то ли чо. Шарлин, красивая молодая негритяночка, показывала какие-то фотки на телефоне; я показал фотку радуги (не могу закинуть, тут интернета нету в гостинице), она попросила поделиться, дал ей телефон, послала себе. А этот горячий восточный парень такой заревновал, что красавица поделилась со мной своим мейлом, а с ним не поделилась. Ха. Потому что надо не выпрашивать, а делиться, да. И будто мне это зачем-то нужно. Шарлин на тему криптокойнов ходит слушать, а этот как раз что-то криптовое задвигал. Кабы он не гнал так агрессивно, я б его с Майком познакомил.

Шарлин сказала, что постарается проникнуть на ужин спикеров.  И она таки проникла, пришла с Франсуа; но потом ушла, ну типа спикеров же в лицо знают, так чо - Кортни ее и выперла, думаю. Не знаю, не видел.

В час опять Тони Моррис, про "growing trees", но рассказывал ужасно нудно, и контент некачественный. Такое ощущение, что расчитывает на тупую публику, и типа просто отбарабанил, как для студентов.

В два опять про HTTP, какой красивый пакет guardrail люди сделали, чтобы обеспечить документирование и чуть ли не типизацию API. Ну там все сложно, в реале. А, и еще генерируют код - через свагер. В конце спикер признался, что один интерн, "не понимая, что делает", удалил "ненужный код" (тесты ничего не заметили), и разрушил всю апликацию на продакшене, пока не откатили назад. Достаточно, да? Кстати, понятия не имею, на каком языке все это дело было. На джейсоне, наверно.

А затем пошел, типа для попсы и отдохнуть, на "introduction to natural deduction". Ну которое я студентам преподаю. Лайл раздал распечатки, со списком рулесов, через слак запостил линк, откуда взять stack и хаскель, и откуда склонировать его проект, git clone https://github.com/lylek/proof-verifier.git - ну чо, тесты идут, чо.

Стал впаривать эту дедакшен, но срезал углы. Правила, как строить доказательство, не рассказал, и все его простые домашки выглядели загадкой. Кстати, я понял, каково моим студентам. Буду полегче.

Потом он показал страничку с Карри-Хауардом, и что чему соответствует. Кое-где срезая углы. Кстати об углах. Мы сели в таком "углу гуру" - я, Майк Стей, Стивен Пиментель. Майк там пытался перевести на человеческий, как это Лайл перегнал negation elimination на Карри-Хауарда, но я не согласился. А как вообще в хаскеле двойное отрицание записывается? (Я не местный, не в курсе.)

Ну и это, надо уже на ужин; а у меня телефон разрядился. Днем я пытался было выйти на рабочий слак, посмотреть, чо там ваще, и как мой пулреквест поживает - но оказалось, что и рабочий телефон разряжен. А блин, проводочек для зарядки я не брал чота. Ну пошел в гостиницу, скинул из рюкзака все лишнее. Жарища стояла, кстати, дикая. Но я куртку таки взял в рюкзаке, знаю я этот Боулдер, сейчас жара, через полчаса снегопад.

Ну фигня, хоть прогулялся 3 мили. В пивной наши сидели уже, но мало. Я подсел к паре спикеров, познакомился, пошел подключать телефон заряжать. Вернулся - а у них там уже Франсуа с Шарлин сидят. Ну хорошо, хорошо, пошел дальше сел. К двум голландцам и одному местному. Голландцы сначала поняли, что они оба голландцы, потом оказалось, что они в одной конторе работают, ну и т.д. Обсуждали с ними Европу, Россию, Америку. Но главное я узнал от эпистемологического философа Марко - что главная проблема в скальной комьюнити - это Мартин. Это он погнал Пола, когда тот требовал "больше ФП"; и т.п. А до нас уже волны доходят, как будто все это политика между восточным берегом и западным (то и нету на этой концеренции никого из лайтбенда, например, и никого из cats). А, хер с ним. Потом голландец Марко стал байки рассказывать. Как один его знакомый был студентом у Дайкстры (все так произносят), и как Дайкстра разговаривал очень медленно, сначала взвесив в голове целое длинное предложение, и произнося его слово за словом.

Тут я взвился. Извините, в отличие от вас, я-то Дайкстру видел, и разговаривал он совершенно нормальным веселым голосом, и говорил вполне нормальные умные вещи. Что за херня. Сменили тему разговора.

Да потом мне эти нудные надоели, я пошел встретил Павла Шульца (кстати, спросил его про Сергея Щ. - не помнит такого); Павел с Майком работал, да и сейчас как бы работает; и еще там был прикольнейший ABC из Миссури, который типа два года жил в Сингапуре (и жена у него развеселая сингапурка), но главное, этот Hsu рассекает на APL, написал на нем компилятор APL, на 17 строк кода, и этот компилятор и на GPU работает, да и вообще Apl самое то для GPU, ну и все такое. А мечтает он поехать в отпуск на Алясочку, месяца на два-три, в декабре, чтобы 24-часовую ночь застать, потому что он любит ночью работать. Любит ли он откапывать машину от снега, утеплять окна на зиму, и всякое такое - типа тоже любит. И хорошую теплую зимнюю одежду любит. Комаров только не любит. Ну я ему такой - да какие уж там на Аляске комары, это просто американцы народ балованный, им покажи три комара, они в панике. Вот так вот мы чесали языками и разговаривали о всякой херне. Как Майк с Джоном Баэзом работал, диссертацию у него написал. Джон-то классный же тоже.

Но пиво мне уже не лезло; я сидел пил воду, и постепенно оклямывался. А к десяти понял, что дальше не могу, и пешком идти тоже полторы мили не то чтобы лень, но поздно, и поехал на лифте. Водила Роллин, такой седой, толстый, бывший электронщик, ругал языки программирования, кроме питона, на котором его сын пишет; а мама у Роллина с перфокартами работала. Чувствую я, что этот дедок Роллин мне ну хотя бы в племянники годится. Вот же ж блин, да.

Притащился, и быстро в душ, и сейчас дыбр допишу, и все, спать, завтра рано вставать, в 9 Майк будет что-то впаривать. CDelta Cryptocurrency Platform, вот.

Пока.

 

 

Comments

[sassa_nf]

"negation elimination на Карри-Хауарда, но я не согласился. А как вообще в хаскеле двойное отрицание записывается?"

Double negation or negation elimination?

Double negation is: dn : (a -> b) -> b

Polymorphism on b means it includes (a->⊥)->⊥.

[juan_gandhi]

I meant double negation, yes.

[aucubagold]

насыщенно)

[juan_gandhi]

Да; много такого не выдержать, а несколько дней норм.

[66george]

Выходит Тони Моррис, расстёгивает зиппер и мочится на публику.

[juan_gandhi]

Ну он не настолько отвязный.

[thedeemon]

Смотря что именно под отрицанием понимать. А то, например, показывали, что двойное отрицание суть ленивость, хаскель на нем весь стоит.
https://www.microsoft.com/en-us/research/wp-content/uploads/2006/01/not-not-ml.pdf (Mycroft и SPJ в авторах)

[juan_gandhi]

О, забавно.
У Лайла отрицание было определено как импликация в ложь.

[sassa_nf]

Sure. Laziness is Thunks, Thunks are Continuations. CPT turns any A into (A->b)->b.

[gracheeha]

>> Любит ли он откапывать машину от снега, утеплять окна на зиму, и всякое такое - типа тоже любит.

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

Я вообще люблю физическую работу на свежем воздухе, но когда мне жарко, то моё давление падает, а оно у меня и так пониженное, и мне становится нехорошо. Зимой же я могла пахать, как вол, и получать от этого удовольствие без побочных неприятностей. И лыжи (cross-country) я по той же причине любила. Коньки - нет, не люблю крутиться на пятачке. До замужества я жила рядом с Голосеевским лесом и, как только появлялась возможность, хватала лыжи и мчалась, куда глаза глядят, по лесу.

[juan_gandhi]

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

[vital_sol]

А я жил до 8 класса рядом с голосеевским лесом :)
И тоже все время на лыжах, ну вот и до сих пор.

[gracheeha]

Привет земляку! На какой улице Вы жили?

[vital_sol]

На Потехина. Она с одной стороны упиралась в лес, а с другой выходила на 40 лет октября, тоже мимо леса. То есть лес был как бы с двух сторон.
А Вы где?

[gracheeha]

Я жила сначала на ул. Голосеевской, а потом на Проспекте 40-летия 90, прямо напротив парка. А Потехина где-то возле ВДНХ, как мне кажется. Я ещё работала в Ин-те Теор. Физики в Феофании, так у меня на работе тоже пара лыж стояла. :)

[vital_sol]

Да, Потехина между Голосеевским парком и ВДНХ, примерно посредине.
А у меня мать работала в Феофании, в интернате для детей с нарушениями речи. Который был напротив математического интерната.

[gracheeha]

В мою бытность студенткой мех-мата я волонтёрила в математическом интернате. :)

[zyxman]

На руби, очень вероятно:
https://www.guardrails.io/blog